Documentation

TauCeti.Algebra.Module.Lattice

Full submodule lattices #

This file provides generic results about full submodules over fraction fields. It relates bases and ranks of full submodules to their ambient spaces. It also extends integral linear equivalences between full submodules to rational linear equivalences of their ambient spaces, and proves that rational linear equivalences preserve fullness. Finally, a free full lattice over an integral domain rationalizes to its ambient vector space over the fraction field.

Main declarations #

Module.Basis.span_range_extendOfIsLattice: the span of an extended lattice basis is the lattice.
TauCeti.Submodule.IsLattice.toAddSubgroup_eq_closure_range_extendOfIsLattice: the additive closure of an extended lattice basis is the lattice's underlying additive subgroup.
Submodule.toAddSubgroup_submoduleOf: taking the underlying additive subgroup commutes with restricting a submodule to another submodule.
TauCeti.Submodule.IsLattice.finrank_eq_finrank: a full lattice and its ambient space have the same finrank.
LinearEquiv.extendOfIsLattice: extension of an R-linear equivalence between full submodules to their ambient K-vector spaces.
TauCeti.Submodule.IsLattice.isBaseChange_subtype: the inclusion of a free full lattice submodule into its ambient vector space over the fraction field is a base change.
TauCeti.Submodule.rationalizationEquiv: the canonical equivalence from the scalar extension of a free full lattice submodule to its ambient vector space.
TauCeti.TensorProduct.unitTmulEquiv: a finite free module is the full lattice of unit pure tensors in its scalar extension.
TauCeti.TensorProduct.rationalizationEquiv_baseChange_unitTmulEquiv: rationalizing that unit-tensor lattice returns the scalar extension one started from.

References #

See N. Bourbaki, Commutative Algebra, Chapter VII, §4 for lattice theory over Dedekind domains.

theorem Module.Basis.span_range_extendOfIsLattice {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] {κ : Type u_4} {N : Submodule R V} [Submodule.IsLattice K N] (b : Basis κ R ↥N) :

Submodule.span R (Set.range ⇑(extendOfIsLattice K b)) = N

The R-span of the ambient K-basis obtained from an R-basis of a lattice is the lattice itself.

theorem TauCeti.Submodule.IsLattice.finrank_eq_finrank {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (N : Submodule R V) [Submodule.IsLattice K N] [Module.Free R ↥N] :

Module.finrank R ↥N = Module.finrank K V

The R-finrank of a free full lattice in V equals the K-finrank of the ambient space.

theorem Submodule.toAddSubgroup_submoduleOf {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] (p q : Submodule R V) :

(p.submoduleOf q).toAddSubgroup = p.toAddSubgroup.addSubgroupOf q.toAddSubgroup

Taking the underlying additive subgroup commutes with restricting a submodule to another submodule.

theorem TauCeti.Submodule.IsLattice.toAddSubgroup_eq_closure_range_extendOfIsLattice {V : Type u_1} [AddCommGroup V] [Module ℚ V] {N : Submodule ℤ V} [Submodule.IsLattice ℚ N] {κ : Type u_2} (b : Module.Basis κ ℤ ↥N) :

N.toAddSubgroup = AddSubgroup.closure (Set.range ⇑(Module.Basis.extendOfIsLattice ℚ b))

The additive subgroup generated by an extended basis of a full ℤ-submodule is the submodule's underlying additive subgroup.

noncomputable def LinearEquiv.extendOfIsLattice {R : Type u_1} {K : Type u_2} {V : Type u} {W : Type v} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] [AddCommGroup W] [Module R W] [Module K W] [IsScalarTower R K W] {S : Submodule R V} {T : Submodule R W} [Submodule.IsLattice K S] [Submodule.IsLattice K T] [Module.Free R ↥S] (e : ↥S ≃ₗ[R] ↥T) :

Extend an R-linear equivalence between full submodules uniquely to their ambient K-vector spaces.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem LinearEquiv.extendOfIsLattice_apply {R : Type u_1} {K : Type u_2} {V : Type u} {W : Type v} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] [AddCommGroup W] [Module R W] [Module K W] [IsScalarTower R K W] {S : Submodule R V} {T : Submodule R W} [Submodule.IsLattice K S] [Submodule.IsLattice K T] [Module.Free R ↥S] (e : ↥S ≃ₗ[R] ↥T) (x : ↥S) :

e.extendOfIsLattice ↑x = ↑(e x)

The ambient extension of a full-submodule equivalence agrees with it on the submodule.

theorem LinearEquiv.eq_extendOfIsLattice {R : Type u_1} {K : Type u_2} {V : Type u} {W : Type v} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] [AddCommGroup W] [Module R W] [Module K W] [IsScalarTower R K W] {S : Submodule R V} {T : Submodule R W} [Submodule.IsLattice K S] [Submodule.IsLattice K T] [Module.Free R ↥S] (e : ↥S ≃ₗ[R] ↥T) (f : V ≃ₗ[K] W) (h : ∀ (x : ↥S), f ↑x = ↑(e x)) :

f = e.extendOfIsLattice

A K-linear equivalence extending a given equivalence of full submodules is the canonical extension.

theorem LinearEquiv.extendOfIsLattice_map {R : Type u_1} {K : Type u_2} {V : Type u} {W : Type v} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] [AddCommGroup W] [Module R W] [Module K W] [IsScalarTower R K W] {S : Submodule R V} {T : Submodule R W} [Submodule.IsLattice K S] [Submodule.IsLattice K T] [Module.Free R ↥S] (e : ↥S ≃ₗ[R] ↥T) :

Submodule.map (↑(restrictScalars R e.extendOfIsLattice)) S = T

The ambient extension maps the source full submodule onto the target full submodule.

theorem TauCeti.Submodule.IsLattice.isBaseChange_subtype {R : Type u} {K : Type v} {V' : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V'] [Module R V'] [Module K V'] [IsScalarTower R K V'] (S : Submodule R V') [Module.Free R ↥S] [Submodule.IsLattice K S] :

IsBaseChange K S.subtype

The inclusion of a free full lattice submodule over an integral domain into its ambient vector space over the fraction field exhibits that space as base change from R to K.

noncomputable def TauCeti.Submodule.rationalizationEquiv {R : Type u} {K : Type v} {V' : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V'] [Module R V'] [Module K V'] [IsScalarTower R K V'] (S : Submodule R V') [Module.Free R ↥S] [Submodule.IsLattice K S] :

TensorProduct R K ↥S ≃ₗ[K] V'

The canonical equivalence from the scalar extension of a free full lattice submodule to its ambient vector space.

Equations

TauCeti.Submodule.rationalizationEquiv S = ⋯.equiv

Instances For

@[simp]

theorem TauCeti.Submodule.rationalizationEquiv_tmul {R : Type u} {K : Type v} {V' : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V'] [Module R V'] [Module K V'] [IsScalarTower R K V'] (S : Submodule R V') [Module.Free R ↥S] [Submodule.IsLattice K S] (k : K) (x : ↥S) :

(rationalizationEquiv S) (k ⊗ₜ[R] x) = k • ↑x

The rationalization equivalence sends a pure tensor to scalar multiplication of the embedded lattice vector. This equation characterizes the equivalence.

@[simp]

theorem TauCeti.Submodule.rationalizationEquiv_symm_coe {R : Type u} {K : Type v} {V' : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V'] [Module R V'] [Module K V'] [IsScalarTower R K V'] (S : Submodule R V') [Module.Free R ↥S] [Submodule.IsLattice K S] (x : ↥S) :

(rationalizationEquiv S).symm ↑x = 1 ⊗ₜ[R] x

The inverse rationalization equivalence sends an embedded lattice vector to the corresponding unit pure tensor.

theorem TauCeti.Submodule.IsLattice.map {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (S : Submodule ℤ V) [Submodule.IsLattice ℚ S] (e : V ≃ₗ[ℚ ] W) :

Submodule.IsLattice ℚ (Submodule.map (↑(LinearEquiv.restrictScalars ℤ e)) S)

A rational linear equivalence maps a full integral submodule to a full integral submodule.

theorem TauCeti.TensorProduct.range_mk_one_eq_span {R : Type u} {K : Type v} {M : Type w} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] {ι : Type u_1} (b : Module.Basis ι R M) :

((TensorProduct.mk R K M) 1).range = Submodule.span R (Set.range ⇑(Module.Basis.baseChange K b))

The unit pure tensors are the R-span of the base change of any basis.

instance TauCeti.TensorProduct.isLattice_range_mk_one {R : Type u} {K : Type v} {M : Type w} [CommRing R] [CommRing K] [Algebra R K] [AddCommMonoid M] [Module R M] [Module.Finite R M] :

Submodule.IsLattice K ((TensorProduct.mk R K M) 1).range

The unit pure tensors form a full lattice in the scalar extension of a finite module.

noncomputable def TauCeti.TensorProduct.unitTmulEquiv (R : Type u) (K : Type v) (M : Type w) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup M] [Module R M] [Module.Free R M] :

M ≃ₗ[R] ↥((TensorProduct.mk R K M) 1).range

A finite free module is canonically isomorphic to the lattice of unit pure tensors in its scalar extension.

Equations

TauCeti.TensorProduct.unitTmulEquiv R K M = LinearEquiv.ofInjective ((TensorProduct.mk R K M) 1) ⋯

Instances For

instance TauCeti.TensorProduct.free_range_mk_one {R : Type u} {K : Type v} {M : Type w} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup M] [Module R M] [Module.Free R M] :

Module.Free R ↥((TensorProduct.mk R K M) 1).range

The lattice of unit pure tensors is free, being a copy of the module it comes from.

@[simp]

theorem TauCeti.TensorProduct.coe_unitTmulEquiv_apply {R : Type u} {K : Type v} {M : Type w} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup M] [Module R M] [Module.Free R M] (m : M) :

↑((unitTmulEquiv R K M) m) = 1 ⊗ₜ[R] m

The unit-tensor equivalence sends a vector to its unit pure tensor. This equation characterizes the equivalence.

@[simp]

theorem TauCeti.TensorProduct.unitTmulEquiv_symm_tmul {R : Type u} {K : Type v} {M : Type w} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup M] [Module R M] [Module.Free R M] (m : M) (h : 1 ⊗ₜ[R] m ∈ ((TensorProduct.mk R K M) 1).range) :

(unitTmulEquiv R K M).symm ⟨1 ⊗ₜ[R] m, h⟩ = m

The inverse unit-tensor equivalence recovers a vector from its unit pure tensor.

@[simp]

theorem TauCeti.TensorProduct.rationalizationEquiv_baseChange_unitTmulEquiv {R : Type u} {K : Type v} {M : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (x : TensorProduct R K M) :

(Submodule.rationalizationEquiv ((TensorProduct.mk R K M) 1).range) ((LinearEquiv.baseChange R K M (↥((TensorProduct.mk R K M) 1).range) (unitTmulEquiv R K M)) x) = x

Rationalizing the unit-tensor lattice recovers the scalar extension it sits in: base-changing the unit-tensor equivalence and then rationalizing is the identity.

theorem TauCeti.TensorProduct.unitTmulEquiv_baseChange_trans_rationalizationEquiv {R : Type u} {K : Type v} {M : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] :

LinearEquiv.baseChange R K M (↥((TensorProduct.mk R K M) 1).range) (unitTmulEquiv R K M) ≪≫ₗ Submodule.rationalizationEquiv ((TensorProduct.mk R K M) 1).range = LinearEquiv.refl K (TensorProduct R K M)

The bundled form of rationalizationEquiv_baseChange_unitTmulEquiv.