NYLL
Module

ResidueFieldHullSocle.lean

Nyll.EtaleFundamentalGroups.Purity.ResidueFieldHullSocle
7 declarations indexed from sourceView source ↗

Module documentation

The socle of an essential extension of the residue field

In an essential extension of the residue field, the elements killed by the maximal ideal form precisely the given residue-field image. Indeed, the cyclic submodule of any such element meets that image; a coefficient outside the maximal ideal is a unit and recovers the original element.

Evaluation at one identifies maps from a quotient ring with the elements annihilated by its defining ideal. Consequently maps from the residue field into its essential extension form a copy of the residue field. The arguments use the existing R-module structures throughout.

Imports9
  • Nyll.EtaleFundamentalGroups.Purity.EssentialModuleExtension
  • Mathlib.Algebra.Group.Units.Defs
  • Mathlib.Algebra.Module.Submodule.Equiv
  • Mathlib.Algebra.Module.Submodule.Range
  • Mathlib.Algebra.Module.Torsion.Basic
  • Mathlib.LinearAlgebra.Quotient.Basic
  • Mathlib.LinearAlgebra.Span.Basic
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Imported by5

Declarations

theorem

quotient_linearMap_range_le_torsionBySet

L40 ↗
EtaleFundamentalGroups.Purity.quotient_linearMap_range_le_torsionBySet
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {E : Type v} [AddCommGroup E] [Module R E]
Lean source · statement
theorem quotient_linearMap_range_le_torsionBySet
    (I : Ideal R) (f : (R ⧸ I) →ₗ[R] E) :
    LinearMap.range f ≤ Submodule.torsionBySet R E I
def

quotientHomEquivTorsionBySet

L56 ↗
EtaleFundamentalGroups.Purity.quotientHomEquivTorsionBySet
Documentation

Evaluation at one identifies quotient-module homomorphisms with vectors annihilated by the quotient ideal.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {E : Type v} [AddCommGroup E] [Module R E]
Lean source · full declaration
def quotientHomEquivTorsionBySet (I : Ideal R) :
    ((R ⧸ I) →ₗ[R] E) ≃ₗ[R] Submodule.torsionBySet R E I where
  toFun f := ⟨f (Ideal.Quotient.mk I 1),
    quotient_linearMap_range_le_torsionBySet I f ⟨Ideal.Quotient.mk I 1, rfl⟩⟩
  invFun z := I.liftQ (LinearMap.toSpanSingleton R E (z : E)) (by
    intro a ha
    change a • (z : E) = 0
    exact (Submodule.mem_torsionBySet_iff (I : Set R) (z : E)).mp z.property ⟨a, ha⟩)
  left_inv f := by
    apply LinearMap.ext
    intro q
    obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective q
    change a • f (Ideal.Quotient.mk I 1) = f (Ideal.Quotient.mk I a)
    rw [← f.map_smul]
    congr 1
    change Ideal.Quotient.mk I (a * 1) = Ideal.Quotient.mk I a
    rw [mul_one]
  right_inv z := by
    apply Subtype.ext
    change (1 : R) • (z : E) = (z : E)
    exact one_smul R (z : E)
  map_add' f g := Subtype.ext rfl
  map_smul' a f := Subtype.ext rfl
theorem

quotientHomEquivTorsionBySet_apply

L81 ↗
EtaleFundamentalGroups.Purity.quotientHomEquivTorsionBySet_apply
Documentation

The quotient-Hom equivalence evaluates a linear map at the class of one.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {E : Type v} [AddCommGroup E] [Module R E]
Lean source · statement
theorem quotientHomEquivTorsionBySet_apply
    (I : Ideal R) (f : (R ⧸ I) →ₗ[R] E) :
    (quotientHomEquivTorsionBySet (R := R) (E := E) I f : E) =
      f (Ideal.Quotient.mk I 1)
theorem

quotientHomEquivTorsionBySet_symm_apply_mk

L87 ↗
EtaleFundamentalGroups.Purity.quotientHomEquivTorsionBySet_symm_apply_mk
Documentation

The inverse quotient-Hom equivalence sends the class of a to a • z.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {E : Type v} [AddCommGroup E] [Module R E]
Lean source · statement
theorem quotientHomEquivTorsionBySet_symm_apply_mk
    (I : Ideal R) (z : Submodule.torsionBySet R E I) (a : R) :
    (quotientHomEquivTorsionBySet (R := R) (E := E) I).symm z
        (Ideal.Quotient.mk I a) = a • (z : E)
theorem

torsionBySet_maximalIdeal_eq_range

L96 ↗
EtaleFundamentalGroups.Purity.torsionBySet_maximalIdeal_eq_range
Documentation

In an essential extension of a residue-field image, that image is exactly the submodule annihilated by the maximal ideal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {E : Type v} [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
theorem torsionBySet_maximalIdeal_eq_range
    (i : (R ⧸ IsLocalRing.maximalIdeal R) →ₗ[R] E)
    (hess : IsEssentialSubmodule (LinearMap.range i)) :
    Submodule.torsionBySet R E (IsLocalRing.maximalIdeal R) =
      LinearMap.range i
def

residueFieldHullSocleEquiv

L135 ↗
EtaleFundamentalGroups.Purity.residueFieldHullSocleEquiv
Documentation

The socle of an essential extension of an embedded residue field is linearly equivalent to that residue field.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {E : Type v} [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
def residueFieldHullSocleEquiv
    (i : (R ⧸ IsLocalRing.maximalIdeal R) →ₗ[R] E)
    (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i)) :
    Submodule.torsionBySet R E (IsLocalRing.maximalIdeal R) ≃ₗ[R]
      (R ⧸ IsLocalRing.maximalIdeal R)
def

residueFieldHullHomEquiv

L148 ↗
EtaleFundamentalGroups.Purity.residueFieldHullHomEquiv
Documentation

Homomorphisms from the residue field into its essential extension form a copy of the residue field.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {E : Type v} [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
def residueFieldHullHomEquiv
    (i : (R ⧸ IsLocalRing.maximalIdeal R) →ₗ[R] E)
    (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i)) :
    ((R ⧸ IsLocalRing.maximalIdeal R) →ₗ[R] E) ≃ₗ[R]
      (R ⧸ IsLocalRing.maximalIdeal R)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.