Loogle!

Result

Found 25 declarations mentioning TensorProduct.AlgebraTensorModule.map.

TensorProduct.AlgebraTensorModule.map_id 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : TensorProduct.AlgebraTensorModule.map LinearMap.id LinearMap.id = LinearMap.id
TensorProduct.AlgebraTensorModule.map 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct R M N →ₗ[A] TensorProduct R P Q
TensorProduct.AlgebraTensorModule.map_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f g = TensorProduct.map f g
TensorProduct.AlgebraTensorModule.map_one 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : TensorProduct.AlgebraTensorModule.map 1 1 = 1
TensorProduct.AlgebraTensorModule.map_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : (TensorProduct.AlgebraTensorModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
TensorProduct.AlgebraTensorModule.map_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.AlgebraTensorModule.map f₂ g₂ ∘ₗ TensorProduct.AlgebraTensorModule.map f₁ g₁
TensorProduct.AlgebraTensorModule.map_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (f₁ f₂ : M →ₗ[A] M) (g₁ g₂ : N →ₗ[R] N) : TensorProduct.AlgebraTensorModule.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.AlgebraTensorModule.map f₁ g₁ * TensorProduct.AlgebraTensorModule.map f₂ g₂
TensorProduct.AlgebraTensorModule.map_add_left 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (f₁ + f₂) g = TensorProduct.AlgebraTensorModule.map f₁ g + TensorProduct.AlgebraTensorModule.map f₂ g
TensorProduct.AlgebraTensorModule.map_smul_right 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f (r • g) = r • TensorProduct.AlgebraTensorModule.map f g
TensorProduct.AlgebraTensorModule.map_add_right 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f (g₁ + g₂) = TensorProduct.AlgebraTensorModule.map f g₁ + TensorProduct.AlgebraTensorModule.map f g₂
TensorProduct.AlgebraTensorModule.map_smul_left 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (b • f) g = b • TensorProduct.AlgebraTensorModule.map f g
TensorProduct.AlgebraTensorModule.homTensorHomMap_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : (TensorProduct.AlgebraTensorModule.homTensorHomMap R A B M N P Q) (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
TensorProduct.AlgebraTensorModule.rTensor_tensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
(R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} (P' : Type uP') [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid P'] [Module A P'] [Module R P] [IsScalarTower R A P] [Module R P'] [IsScalarTower R A P'] (g : P →ₗ[A] P') : LinearMap.rTensor (TensorProduct R M N) g = ↑(TensorProduct.AlgebraTensorModule.assoc R A A P' M N) ∘ₗ TensorProduct.AlgebraTensorModule.map (LinearMap.rTensor M g) LinearMap.id ∘ₗ ↑(TensorProduct.AlgebraTensorModule.assoc R A A P M N).symm
TensorProduct.AlgebraTensorModule.mapBilinear_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : ((TensorProduct.AlgebraTensorModule.mapBilinear R A B M N P Q) f) g = TensorProduct.AlgebraTensorModule.map f g
TensorProduct.directSum.eq_1 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
(R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂) [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] : TensorProduct.directSum R S M₁ M₂ = LinearEquiv.ofLinear (TensorProduct.AlgebraTensorModule.lift (DirectSum.toModule S ι₁ ((DirectSum ι₂ fun i₂ => M₂ i₂) →ₗ[R] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) fun i₁ => (DirectSum.toModule R ι₂ (M₁ i₁ →ₗ[S] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) fun i₂ => (TensorProduct.AlgebraTensorModule.curry (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂))).flip).flip)) (DirectSum.toModule S (ι₁ × ι₂) (TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) (DirectSum ι₂ fun i₂ => M₂ i₂)) fun i => TensorProduct.AlgebraTensorModule.map (DirectSum.lof S ι₁ M₁ i.1) (DirectSum.lof R ι₂ M₂ i.2)) ⋯ ⋯
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
Module.endTensorEndAlgHom_apply 📋 Mathlib.RingTheory.TensorProduct.Maps
{R : Type u_1} {S : Type u_2} {A : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Algebra S A] [Algebra R A] [Module R M] [Module S M] [Module A M] [Module R N] [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S M] (f : Module.End A M) (g : Module.End R N) : Module.endTensorEndAlgHom (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
isBaseChange_tensorProduct_map 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {P : Type u_2} [AddCommMonoid P] [Module R P] (A : Type u_4) [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Module S M] [IsScalarTower R S M] [Module A N] [IsScalarTower S A N] [IsScalarTower R A N] {f : M →ₗ[S] N} (hf : IsBaseChange A f) : IsBaseChange A (TensorProduct.AlgebraTensorModule.map f LinearMap.id)
TensorProduct.counit_def 📋 Mathlib.RingTheory.Coalgebra.TensorProduct
{R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [CoalgebraStruct R B] [CoalgebraStruct S A] : CoalgebraStruct.counit = ↑(TensorProduct.AlgebraTensorModule.rid R S S) ∘ₗ TensorProduct.AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit
Coalgebra.TensorProduct.map_toLinearMap 📋 Mathlib.RingTheory.Coalgebra.TensorProduct
{R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[S] N) (g : P →ₗc[R] Q) : ↑(Coalgebra.TensorProduct.map f g) = TensorProduct.AlgebraTensorModule.map ↑f ↑g
TensorProduct.comul_def 📋 Mathlib.RingTheory.Coalgebra.TensorProduct
{R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [CoalgebraStruct R B] [CoalgebraStruct S A] : CoalgebraStruct.comul = ↑(TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) ∘ₗ TensorProduct.AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul
TensorProduct.antipode_def 📋 Mathlib.RingTheory.HopfAlgebra.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] [Algebra R S] [HopfAlgebra R A] [HopfAlgebra S B] [Algebra R B] [IsScalarTower R S B] : HopfAlgebraStruct.antipode S = TensorProduct.AlgebraTensorModule.map (HopfAlgebraStruct.antipode S) (HopfAlgebraStruct.antipode R)
AdicCompletion.ofTensorProduct_naturality 📋 Mathlib.RingTheory.AdicCompletion.AsTensorProduct
{R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : AdicCompletion.map I f ∘ₗ AdicCompletion.ofTensorProduct I M = AdicCompletion.ofTensorProduct I N ∘ₗ TensorProduct.AlgebraTensorModule.map LinearMap.id f
AdicCompletion.tensor_map_id_left_injective_of_injective 📋 Mathlib.RingTheory.AdicCompletion.AsTensorProduct
{R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} [Module.Finite R M] [Module.Finite R N] (hf : Function.Injective ⇑f) : Function.Injective ⇑(TensorProduct.AlgebraTensorModule.map LinearMap.id f)
AdicCompletion.tensor_map_id_left_eq_map 📋 Mathlib.RingTheory.AdicCompletion.AsTensorProduct
{R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) [Module.Finite R M] [Module.Finite R N] : TensorProduct.AlgebraTensorModule.map LinearMap.id f = ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ AdicCompletion.map I f ∘ₗ ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I 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