Loogle!

Result

Found 63 declarations mentioning Algebra.TensorProduct.map.

Algebra.TensorProduct.map 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : TensorProduct R A B →ₐ[S] TensorProduct R C D
Algebra.TensorProduct.map_id 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] : Algebra.TensorProduct.map (AlgHom.id S A) (AlgHom.id R B) = AlgHom.id S (TensorProduct R A B)
Algebra.TensorProduct.productMap_eq_comp_map 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) : Algebra.TensorProduct.productMap f g = (Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f g)
Algebra.TensorProduct.map_comp_includeLeft 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : (Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft = Algebra.TensorProduct.includeLeft.comp f
Algebra.TensorProduct.map_id_comp 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {D : Type uD} {F : Type uF} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring D] [Algebra R D] [Semiring F] [Algebra R F] (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) : Algebra.TensorProduct.map (AlgHom.id S A) (g₂.comp g₁) = (Algebra.TensorProduct.map (AlgHom.id S A) g₂).comp (Algebra.TensorProduct.map (AlgHom.id S A) g₁)
Algebra.TensorProduct.map_comp_includeRight 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) : (Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeRight.comp g
Algebra.TensorProduct.map_comp_id 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {C : Type uC} {E : Type uE} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring E] [Algebra R E] [Algebra S E] [IsScalarTower R S E] (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C) : Algebra.TensorProduct.map (f₂.comp f₁) (AlgHom.id R E) = (Algebra.TensorProduct.map f₂ (AlgHom.id R E)).comp (Algebra.TensorProduct.map f₁ (AlgHom.id R E))
Algebra.TensorProduct.map_comp 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE} {F : Type uF} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] [Semiring E] [Algebra R E] [Algebra S E] [IsScalarTower R S E] [Semiring F] [Algebra R F] (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C) (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) : Algebra.TensorProduct.map (f₂.comp f₁) (g₂.comp g₁) = (Algebra.TensorProduct.map f₂ g₂).comp (Algebra.TensorProduct.map f₁ g₁)
Algebra.TensorProduct.map_tmul 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) (a : A) (b : B) : (Algebra.TensorProduct.map f g) (a ⊗ₜ[R] b) = f a ⊗ₜ[R] g b
Algebra.TensorProduct.lmul'_comp_map 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [CommSemiring S] [Algebra R A] [Algebra R B] [Algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) : (Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f g) = Algebra.TensorProduct.lift f g ⋯
Algebra.TensorProduct.map_restrictScalars_comp_includeRight 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeRight.comp g
Algebra.TensorProduct.toLinearMap_map 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D) : (Algebra.TensorProduct.map f g).toLinearMap = TensorProduct.AlgebraTensorModule.map f.toLinearMap g.toLinearMap
Algebra.TensorProduct.map_bijective 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] {f : A →ₐ[R] B} {g : C →ₐ[R] D} (hf : Function.Bijective ⇑f) (hg : Function.Bijective ⇑g) : Function.Bijective ⇑(Algebra.TensorProduct.map f g)
Algebra.TensorProduct.congr_apply 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x : TensorProduct R A B) : (Algebra.TensorProduct.congr f g) x = (Algebra.TensorProduct.map ↑f ↑g) x
Algebra.TensorProduct.map_range 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) : (Algebra.TensorProduct.map f g).range = (Algebra.TensorProduct.includeLeft.comp f).range ⊔ (Algebra.TensorProduct.includeRight.comp g).range
Algebra.TensorProduct.congr_symm_apply 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Semiring D] [Algebra R D] (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x : TensorProduct R C D) : (Algebra.TensorProduct.congr f g).symm x = (Algebra.TensorProduct.map ↑f.symm ↑g.symm) x
Algebra.TensorProduct.comm_comp_map 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) : (↑(Algebra.TensorProduct.comm R C D)).comp (Algebra.TensorProduct.map f g) = (Algebra.TensorProduct.map g f).comp ↑(Algebra.TensorProduct.comm R A B)
Algebra.TensorProduct.comm_comp_map_apply 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D) (x : TensorProduct R A B) : (Algebra.TensorProduct.comm R C D) ((Algebra.TensorProduct.map f g) x) = (Algebra.TensorProduct.map g f) ((Algebra.TensorProduct.comm R A B) x)
Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R A] : Subalgebra.centralizer R ↑Algebra.TensorProduct.includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.center R B).val).range
Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] (S : Set B) [Module.Free R A] : Subalgebra.centralizer R (⇑Algebra.TensorProduct.includeRight '' S) = (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.centralizer R S).val).range
Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] (S : Subalgebra R B) [Module.Free R A] : Subalgebra.centralizer R ↑(Subalgebra.map Algebra.TensorProduct.includeRight S) = (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.centralizer R ↑S).val).range
Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R B] : Subalgebra.centralizer R ↑Algebra.TensorProduct.includeLeft.range = (Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range
Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] (S : Set A) [Module.Free R B] : Subalgebra.centralizer R (⇑Algebra.TensorProduct.includeLeft '' S) = (Algebra.TensorProduct.map (Subalgebra.centralizer R S).val (AlgHom.id R B)).range
Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R A] : Subalgebra.centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range = (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.center R B).val).range
Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] [Module.Free R B] : Subalgebra.centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range = (Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range
Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct 📋 Mathlib.Algebra.Algebra.Subalgebra.Centralizer
(R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] (S : Subalgebra R A) [Module.Free R B] : Subalgebra.centralizer R ↑(Subalgebra.map Algebra.TensorProduct.includeLeft S) = (Algebra.TensorProduct.map (Subalgebra.centralizer R ↑S).val (AlgHom.id R B)).range
Algebra.TensorProduct.lTensor_ker 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
{R : Type u_4} [CommRing R] {A : Type u_5} {C : Type u_7} {D : Type u_8} [Ring A] [Ring C] [Ring D] [Algebra R A] [Algebra R C] [Algebra R D] (g : C →ₐ[R] D) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) g) = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
Algebra.TensorProduct.rTensor_ker 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
{R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) : RingHom.ker (Algebra.TensorProduct.map f (AlgHom.id R C)) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f)
Algebra.TensorProduct.map_ker 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
{R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} {D : Type u_8} [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map f g) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔ Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
RingHom.Finite.tensorProductMap 📋 Mathlib.RingTheory.TensorProduct.Finite
{R : Type u_1} {S : Type u_2} {S' : Type u_3} {T : Type u_4} {T' : Type u_5} [CommRing R] [CommRing S] [CommRing T] [CommRing S'] [CommRing T'] [Algebra R S] [Algebra R T] [Algebra R S'] [Algebra R T'] {f : S →ₐ[R] S'} (Hf : f.Finite) {g : T →ₐ[R] T'} (Hg : g.Finite) : (Algebra.TensorProduct.map f g).Finite
AlgCat.hom_whiskerLeft 📋 Mathlib.Algebra.Category.AlgCat.Monoidal
{R : Type u} [CommRing R] (L : AlgCat R) {M N : AlgCat R} (f : M ⟶ N) : AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) = Algebra.TensorProduct.map (AlgHom.id R ↑L) (AlgCat.Hom.hom f)
AlgCat.hom_whiskerRight 📋 Mathlib.Algebra.Category.AlgCat.Monoidal
{R : Type u} [CommRing R] {L M : AlgCat R} (f : L ⟶ M) (N : AlgCat R) : AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) = Algebra.TensorProduct.map (AlgCat.Hom.hom f) (AlgHom.id R ↑N)
AlgCat.hom_tensorHom 📋 Mathlib.Algebra.Category.AlgCat.Monoidal
{R : Type u} [CommRing R] {K L M N : AlgCat R} (f : K ⟶ L) (g : M ⟶ N) : AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = Algebra.TensorProduct.map (AlgCat.Hom.hom f) (AlgCat.Hom.hom g)
Bialgebra.ofAlgHom 📋 Mathlib.RingTheory.Bialgebra.Basic
{R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (comul : A →ₐ[R] TensorProduct R A A) (counit : A →ₐ[R] R) (h_coassoc : (↑(Algebra.TensorProduct.assoc R R A A A)).comp ((Algebra.TensorProduct.map comul (AlgHom.id R A)).comp comul) = (Algebra.TensorProduct.map (AlgHom.id R A) comul).comp comul) (h_rTensor : (Algebra.TensorProduct.map counit (AlgHom.id R A)).comp comul = ↑(Algebra.TensorProduct.lid R A).symm) (h_lTensor : (Algebra.TensorProduct.map (AlgHom.id R A) counit).comp comul = ↑(Algebra.TensorProduct.rid R R A).symm) : Bialgebra R A
BialgHom.ofAlgHom 📋 Mathlib.RingTheory.Bialgebra.Hom
{R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A →ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map f f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp f) : A →ₐc[R] B
BialgHom.ofAlgHom_apply 📋 Mathlib.RingTheory.Bialgebra.Hom
{R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A →ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map f f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp f) (a✝ : A) : (BialgHom.ofAlgHom f counit_comp map_comp_comul) a✝ = f a✝
BialgHomClass.map_comp_comulAlgHom 📋 Mathlib.RingTheory.Bialgebra.Hom
{R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] [FunLike F A B] [BialgHomClass F R A B] (f : F) : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f
BialgEquiv.ofAlgEquiv 📋 Mathlib.RingTheory.Bialgebra.Equiv
{R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A ≃ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f) : A ≃ₐc[R] B
BialgEquiv.ofAlgEquiv_apply 📋 Mathlib.RingTheory.Bialgebra.Equiv
{R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A ≃ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f) (a✝ : A) : (BialgEquiv.ofAlgEquiv f counit_comp map_comp_comul) a✝ = f.toFun a✝
BialgEquiv.toLinearMap_ofAlgEquiv 📋 Mathlib.RingTheory.Bialgebra.Equiv
{R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A ≃ₐ[R] B) (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A) (map_comp_comul : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f) : ↑↑(BialgEquiv.ofAlgEquiv f counit_comp map_comp_comul) = ↑↑f
Bialgebra.TensorProduct.counitAlgHom_def 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
(R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : Bialgebra.counitAlgHom S (TensorProduct R A B) = (↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (Bialgebra.counitAlgHom S A) (Bialgebra.counitAlgHom R B))
Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
(R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : CoalgebraStruct.counit = ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (Bialgebra.counitAlgHom S A) (Bialgebra.counitAlgHom R B))).toLinearMap
Bialgebra.TensorProduct.map_toAlgHom 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
{R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D) : ↑(Bialgebra.TensorProduct.map f g) = Algebra.TensorProduct.map ↑f ↑g
Bialgebra.TensorProduct.comulAlgHom_def 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
(R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : Bialgebra.comulAlgHom S (TensorProduct R A B) = (↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp (Algebra.TensorProduct.map (Bialgebra.comulAlgHom S A) (Bialgebra.comulAlgHom R B))
Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
(R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : CoalgebraStruct.comul = ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp (Algebra.TensorProduct.map (Bialgebra.comulAlgHom S A) (Bialgebra.comulAlgHom R B))).toLinearMap
CommRingCat.tensorProd_map_right 📋 Mathlib.Algebra.Category.Ring.Under.Basic
(R S : CommRingCat) [Algebra ↑R ↑S] {X✝ Y✝ : CategoryTheory.Under R} (f : X✝ ⟶ Y✝) : ((R.tensorProd S).map f).right = CommRingCat.ofHom ↑(Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom f))
CommAlgCat.whiskerLeft_hom 📋 Mathlib.Algebra.Category.CommAlgCat.Monoidal
{R : Type u} [CommRing R] {A B : CommAlgCat R} (C : CommAlgCat R) (f : A ⟶ B) : CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f) = Algebra.TensorProduct.map (AlgHom.id R ↑C) (CommAlgCat.Hom.hom f)
CommAlgCat.whiskerRight_hom 📋 Mathlib.Algebra.Category.CommAlgCat.Monoidal
{R : Type u} [CommRing R] {A B : CommAlgCat R} (C : CommAlgCat R) (f : A ⟶ B) : CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f C) = Algebra.TensorProduct.map (CommAlgCat.Hom.hom f) (AlgHom.id R ↑C)
CommAlgCat.tensorHom_hom 📋 Mathlib.Algebra.Category.CommAlgCat.Monoidal
{R : Type u} [CommRing R] {A B C D : CommAlgCat R} (f : A ⟶ C) (g : B ⟶ D) : CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = Algebra.TensorProduct.map (CommAlgCat.Hom.hom f) (CommAlgCat.Hom.hom g)
RingHom.SurjectiveOnStalks.tensorProductMap 📋 Mathlib.RingTheory.SurjectiveOnStalks
{R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {T : Type u_3} [CommRing T] {S' : Type u_4} {T' : Type u_5} [CommRing S'] [CommRing T'] [Algebra R S] [Algebra R T] [Algebra R S'] [Algebra R T'] {f : S →ₐ[R] S'} (Hf : f.SurjectiveOnStalks) {g : T →ₐ[R] T'} (Hg : g.SurjectiveOnStalks) : (Algebra.TensorProduct.map f g).SurjectiveOnStalks
AlgHom.tensorEqualizer 📋 Mathlib.RingTheory.Flat.Equalizer
{R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f g : A →ₐ[R] B) : TensorProduct R T ↥(AlgHom.equalizer f g) →ₐ[S] ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g))
AlgHom.tensorEqualizerEquiv 📋 Mathlib.RingTheory.Flat.Equalizer
{R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f g : A →ₐ[R] B) [Module.Flat R T] : TensorProduct R T ↥(AlgHom.equalizer f g) ≃ₐ[S] ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g))
AlgHom.coe_tensorEqualizer 📋 Mathlib.RingTheory.Flat.Equalizer
{R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f g : A →ₐ[R] B) (x : TensorProduct R T ↥(AlgHom.equalizer f g)) : ↑((AlgHom.tensorEqualizer S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (AlgHom.equalizer f g).val) x
AlgHom.tensorEqualizerEquiv_apply 📋 Mathlib.RingTheory.Flat.Equalizer
{R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f g : A →ₐ[R] B) [Module.Flat R T] (x : TensorProduct R T ↥(AlgHom.equalizer f g)) : (AlgHom.tensorEqualizerEquiv S T f g) x = (AlgHom.tensorEqualizer S T f g) x
CommRingCat.Under.equalizerForkTensorProdIso 📋 Mathlib.Algebra.Category.Ring.Under.Limits
{R S : CommRingCat} [Algebra ↑R ↑S] [Module.Flat ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CommRingCat.Under.tensorProdEqualizer f g ≅ CommRingCat.Under.equalizerFork' (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom f)) (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom g))
Algebra.FiniteType.baseChangeAux_surj 📋 Mathlib.RingTheory.FiniteStability
{R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] {σ : Type u_1} {f : MvPolynomial σ R →ₐ[R] A} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(Algebra.TensorProduct.map (AlgHom.id B B) f)
Subalgebra.mulMap_map_comp_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Subalgebra
{R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] (A B : Subalgebra R S) (f : S →ₐ[R] T) : ((Subalgebra.map f A).mulMap (Subalgebra.map f B)).comp (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) = f.comp (A.mulMap B)
Algebra.TensorProduct.algEquivIncludeRange_toAlgHom 📋 Mathlib.LinearAlgebra.TensorProduct.Subalgebra
(R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] : ↑(Algebra.TensorProduct.algEquivIncludeRange R S T) = Algebra.TensorProduct.map Algebra.TensorProduct.includeLeft.rangeRestrict Algebra.TensorProduct.includeRight.rangeRestrict
CliffordAlgebra.toBaseChange_comp_involute 📋 Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
{R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : (CliffordAlgebra.toBaseChange A Q).comp CliffordAlgebra.involute = (Algebra.TensorProduct.map (AlgHom.id A A) CliffordAlgebra.involute).comp (CliffordAlgebra.toBaseChange A Q)
CliffordAlgebra.toBaseChange_comp_reverseOp 📋 Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
{R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : (AlgHom.op (CliffordAlgebra.toBaseChange A Q)).comp CliffordAlgebra.reverseOp = (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) CliffordAlgebra.reverseOp).comp (CliffordAlgebra.toBaseChange A Q))
Algebra.Presentation.tensorModelOfHasCoeffsInv.eq_1 📋 Mathlib.RingTheory.Extension.Presentation.Core
{R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Presentation R S ι σ) (R₀ : Type u_5) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [P.HasCoeffs R₀] : P.tensorModelOfHasCoeffsInv R₀ = (Ideal.Quotient.liftₐ P.ker ((Algebra.TensorProduct.map (AlgHom.id R R) (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀))))).comp ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm) ⋯).comp ↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm
PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable 📋 Mathlib.RingTheory.Spectrum.Prime.Homeomorph
(K : Type u_2) (R : Type u_3) (S : Type u_4) [Field K] [CommRing R] [CommRing S] [Algebra R K] [Algebra R S] (L : Type u_5) [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L] [IsPurelyInseparable K L] : IsHomeomorph (PrimeSpectrum.comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)
MonoidAlgebra.tensorEquiv.eq_1 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
(R : Type u_1) {M : Type u_2} (A : Type u_4) (B : Type u_5) [CommSemiring R] [CommMonoid M] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] : MonoidAlgebra.tensorEquiv R A B = AlgEquiv.ofAlgHom (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (TensorProduct R A B) (MonoidAlgebra (TensorProduct R A B) M)).comp Algebra.TensorProduct.includeLeft) (MonoidAlgebra.mapRangeAlgHom M Algebra.TensorProduct.includeRight) ⋯) (MonoidAlgebra.liftNCAlgHom (Algebra.TensorProduct.map (AlgHom.id A A) MonoidAlgebra.singleOneAlgHom) ((↑Algebra.TensorProduct.includeRight.toRingHom).comp (MonoidAlgebra.of B M)) ⋯) ⋯ ⋯

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision edaf32c