Module

NormalizationAbsoluteResidueGroup.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationAbsoluteResidueGroup

8 declarations indexed from sourceView source ↗

Module documentation

Absolute normalization residue Galois groups

Identifies the literal normalization residue as an algebraic closure of the base residue field and constructs the restriction isomorphism to its separable residue Galois group.

Imports3

Imported by5

theorem

normalizationResidueAutomorphisms_eq_fieldObject

L28 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueAutomorphisms_eq_fieldObject

Documentation

The existing residue target is precisely the automorphism group of the two stored literal fields with their constructed coefficient action.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

theorem normalizationResidueAutomorphisms_eq_fieldObject
    (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
    [Field Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] :
    normalizationResidueAutomorphisms A Ω Q =
      nativeFieldAutomorphisms (IsLocalRing.ResidueField A) (normalizationResidueFieldObject A Ω Q)
        (normalizationResidueFieldAlgebra A Ω Q)

theorem

normalizationResidueAutomorphisms_fieldObject_apply

L39 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueAutomorphisms_fieldObject_apply

Documentation

The proved field-object identification retains the literal quotient automorphism, including its value on every coefficient.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

theorem normalizationResidueAutomorphisms_fieldObject_apply
    (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
    [Field Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
    (σ : (normalizationResidueAutomorphisms A Ω Q).carrier)
    (z : (normalizationResidueFieldObject A Ω Q).α) :
    nativeFieldResidueActionScalar (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)
        ((eqToIso (normalizationResidueAutomorphisms_eq_fieldObject A Ω Q)).hom.hom'.toFun σ)
        z =
      normalizationResidueActionScalar A Ω Q σ z

def

normalizationResidueSeparableGroup

L69 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueSeparableGroup

Documentation

The actual Galois group of the relative separable closure of the base residue field inside the literal normalization quotient.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def normalizationResidueSeparableGroup
    (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
    [CommRing Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] : GrpCat.{w}

def

normalizationResidueSeparableIso_of_isAlgClosed

L79 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueSeparableIso_of_isAlgClosed

Documentation

Once algebraic closedness of the literal quotient is supplied, the actual integral residue extension and actual restriction equivalence give the comparison of residue automorphism groups.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def normalizationResidueSeparableIso_of_isAlgClosed
    (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
    [Field Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
    [IsAlgClosed (normalizationResidueFieldObject A Ω Q)] :
    normalizationResidueAutomorphisms A Ω Q ≅ normalizationResidueSeparableGroup A Ω Q

theorem

normalizationResidueSeparableIso_of_isAlgClosed_commutes

L95 ↗

EtaleFundamentalGroups.Inertia.normalizationResidueSeparableIso_of_isAlgClosed_commutes

Documentation

The private closed-residue construction computes the original quotient action through its actual separable coefficient inclusion.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

theorem normalizationResidueSeparableIso_of_isAlgClosed_commutes
    (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
    [Field Ω] [Algebra A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
    [IsAlgClosed (normalizationResidueFieldObject A Ω Q).α]
    (σ : (normalizationResidueAutomorphisms A Ω Q).carrier)
    (z : (nativeSeparableResidueField (IsLocalRing.ResidueField A)
      (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)).α) :
    nativeSeparableResidueActionScalar (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)
        ((normalizationResidueSeparableIso_of_isAlgClosed A Ω Q).hom.hom'.toFun σ) z =
      normalizationResidueActionScalar A Ω Q σ
        (nativeSeparableResidueScalar (IsLocalRing.ResidueField A)
          (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q) z)

theorem

normalizationAbsoluteResidue_isAlgClosure

L122 ↗

EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidue_isAlgClosure

Documentation

The literal quotient residue is an algebraic closure of the actual base residue field, derived solely from the original absolute DVR data.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · full declaration

theorem normalizationAbsoluteResidue_isAlgClosure
    (A : Type u) (K : Type v) (Ω : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
    [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] :
    letI := normalizationResidueFieldAlgebra A Ω Q
    IsAlgClosure (IsLocalRing.ResidueField A) (normalizationResidueFieldObject A Ω Q) := by
  let := normalizationResidueFieldAlgebra A Ω Q
  exact ⟨normalizationAbsoluteResidue_isAlgClosed A K Ω Q,
    normalizationResidueFieldAlgebra_isAlgebraic A Ω Q⟩

def

normalizationAbsoluteResidueIso

L136 ↗

EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueIso

Documentation

Original-input restriction from the actual residue automorphisms to the actual separable residue Galois group. No residue comparison is assumed.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def normalizationAbsoluteResidueIso
    (A : Type u) (K : Type v) (Ω : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
    [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] :
    normalizationResidueAutomorphisms A Ω Q ≅ normalizationResidueSeparableGroup A Ω Q

theorem

normalizationAbsoluteResidueIso_commutes

L149 ↗

EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidueIso_commutes

Documentation

The public absolute isomorphism has the actual quotient coefficient square. The separable-field dictionaries remain inside the lower coefficient maps.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

theorem normalizationAbsoluteResidueIso_commutes
    (A : Type u) (K : Type v) (Ω : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
    [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
    (σ : (normalizationResidueAutomorphisms A Ω Q).carrier)
    (z : (nativeSeparableResidueField (IsLocalRing.ResidueField A)
      (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)).α) :
    nativeSeparableResidueActionScalar (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)
        ((normalizationAbsoluteResidueIso A K Ω Q).hom.hom'.toFun σ) z =
      normalizationResidueActionScalar A Ω Q σ
        (nativeSeparableResidueScalar (IsLocalRing.ResidueField A)
          (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q) z)

Module documentation

Absolute normalization residue Galois groups

Declarations