The interaction of linear span and tensor product for mixed scalars.

def Submodule.tensorToSpan {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (p : Submodule R M) : TensorProduct R A ↥p →ₗ[A] ↥(span A ↑p)

If A is an R-algebra and p is an R-submodule of an A-module M, this is the natural surjection A ⊗[R] p → span A p.

See also Submodule.tensorEquivSpan.

Equations

• Submodule.tensorToSpan A p = TensorProduct.AlgebraTensorModule.lift { toFun := fun (a : A) => a • Submodule.inclusionSpan A p, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Submodule.tensorToSpan_apply_tmul {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (p : Submodule R M) (a : A) (x : ↥p) : ↑((tensorToSpan A p) (a ⊗ₜ[R] x)) = a • ↑x

theorem Submodule.surjective_tensorToSpan {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (p : Submodule R M) : Function.Surjective ⇑(tensorToSpan A p)

theorem Submodule.injective_tensorToSpan {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (p : Submodule R M) [Algebra.IsEpi R A] [Module.Flat R A] : Function.Injective ⇑(tensorToSpan A p)

noncomputable def Submodule.tensorEquivSpan {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (p : Submodule R M) [Algebra.IsEpi R A] [Module.Flat R A] : TensorProduct R A ↥p ≃ₗ[A] ↥(span A ↑p)

If A is a flat epi R-algebra and p is an R-submodule of an A-module M then the natural surjection from A ⊗[R] p to span A p is an equivalence.

Equations

• Submodule.tensorEquivSpan A p = LinearEquiv.ofBijective (Submodule.tensorToSpan A p) ⋯

@[simp]

theorem Submodule.tensorEquivSpan_apply_tmul {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (p : Submodule R M) [Algebra.IsEpi R A] [Module.Flat R A] (a : A) (x : ↥p) : ↑((tensorEquivSpan A p) (a ⊗ₜ[R] x)) = a • ↑x

noncomputable def Submodule.tensorSpanEquivSpan (R : Type u_1) (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [Algebra.IsEpi R A] [Module.Flat R A] (s : Set M) : TensorProduct R A ↥(span R s) ≃ₗ[A] ↥(span A s)

If A is a flat epi R-algebra and s is a subset of an A-module M then the natural surjection from A ⊗[R] span R s to span A s is an equivalence.

Equations

• Submodule.tensorSpanEquivSpan R A s = (Submodule.tensorEquivSpan A (Submodule.span R s)).trans (LinearEquiv.ofEq (Submodule.span A ↑(Submodule.span R s)) (Submodule.span A s) ⋯)

@[simp]

theorem Submodule.coe_tensorSpanEquivSpan_apply_tmul {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [Algebra.IsEpi R A] [Module.Flat R A] {s : Set M} (a : A) (x : ↥(span R s)) : ↑((tensorSpanEquivSpan R A s) (a ⊗ₜ[R] x)) = a • ↑x

@[simp]

theorem Submodule.finrank_span_eq_finrank {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Nontrivial A] [Algebra R A] [Algebra.IsEpi R A] [Module.Flat R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] (p : Submodule R M) [Module.Free R ↥p] [Module.Finite R ↥p] : Module.finrank A ↥(span A ↑p) = Module.finrank R ↥p

theorem Submodule.finrank_span_eq_finrank_span (R : Type u_1) (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Nontrivial A] [Algebra R A] [Algebra.IsEpi R A] [Module.Flat R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [IsPrincipalIdealRing R] [IsDomain R] [Module.IsTorsionFree R M] (s : Set M) [Module.Finite R ↥(span R s)] : Module.finrank A ↥(span A s) = Module.finrank R ↥(span R s)