ModuleFiniteTorsionFreeNonzeroFunctional.lean
Nyll.EtaleFundamentalGroups.Purity.FiniteTorsionFreeNonzeroFunctional
2 declarations indexed from sourceView source ↗ Module documentation
Nonzero functionals on finite torsion-free modules
Localizing a torsion-free module in the fraction field preserves its nonzero vectors. A vector-space functional separates such a vector; clearing the denominators of finitely many generators gives a functional with values in the original domain.
Imports12
- Mathlib.Algebra.Algebra.Tower
- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
- Mathlib.Algebra.Module.LocalizedModule.Basic
- Mathlib.Algebra.Module.Submodule.Equiv
- Mathlib.Algebra.Module.Submodule.LinearMap
- Mathlib.Algebra.Module.Submodule.Range
- Mathlib.Algebra.Module.Torsion.Free
- Mathlib.LinearAlgebra.Basis.VectorSpace
- Mathlib.LinearAlgebra.Span.Defs
- Mathlib.RingTheory.Finiteness.Defs
- Mathlib.RingTheory.Localization.FractionRing
- Mathlib.RingTheory.Localization.Integer
Imported by2
Declarations
EtaleFundamentalGroups.Purity.exists_linearMap_apply_ne_zero_of_finite_torsionFree
DocumentationA nonzero vector in a finite torsion-free module is detected by an R-valued linear functional.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
open nonZeroDivisors
universe u v
variable {R : Type u} [CommRing R] [IsDomain R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable [Module.Finite R M] [Module.IsTorsionFree R M]
EtaleFundamentalGroups.Purity.exists_ne_zero_linearMap_of_finite_torsionFree
DocumentationA finite nonzero torsion-free module over a domain has a nonzero linear functional into the domain.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
open nonZeroDivisors
universe u v
variable {R : Type u} [CommRing R] [IsDomain R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable [Module.Finite R M] [Module.IsTorsionFree R M]