Module

ActualNormalizationResidueAction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationResidueAction

6 declarations indexed from sourceView source ↗

Module documentation

The actual original decomposition action on residue coefficients

The quotient automorphism is the SAME original normalization residue morphism. Its localization presentation retains the already proved coefficient equation.

Imports3

Imported by8

def

actualNormalizationQuotientAction

L33 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationQuotientAction

Documentation

The original decomposition group acts by its literal quotient automorphism.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier)

Lean source · statement

def actualNormalizationQuotientAction :
    (normalizationDecompositionGroup A K L Q).carrier →*
      (((normalizationCommAlgCat A L).carrier ⧸ Q) ≃+*
        ((normalizationCommAlgCat A L).carrier ⧸ Q))

def

actualNormalizationQuotientActionScalar

L42 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationQuotientActionScalar

Documentation

Evaluate the SAME literal quotient action on a coefficient. Its ring automorphism group remains inside this original action owner.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier)

Lean source · statement

def actualNormalizationQuotientActionScalar [Q.IsMaximal]
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (z : (normalizationResidueFieldObject A L Q).α) :
    (normalizationResidueFieldObject A L Q).α

theorem

actualNormalizationQuotientActionScalar_apply

L50 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationQuotientActionScalar_apply

Documentation

The stored scalar evaluation is exactly the existing quotient action, with no alternative action or coefficient identification.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier)

Lean source · statement

theorem actualNormalizationQuotientActionScalar_apply [Q.IsMaximal]
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (z : (normalizationResidueFieldObject A L Q).α) :
    actualNormalizationQuotientActionScalar A K L Q d z =
      ((actualNormalizationQuotientAction A K L Q).toFun d).toRingHom.toFun z

theorem

actualNormalizationQuotientActionScalar_eq_residueAction

L58 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationQuotientActionScalar_eq_residueAction

Documentation

The original quotient action evaluates the original residue morphism on the same stored coefficient, before any separable-field comparison.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier)

Lean source · statement

theorem actualNormalizationQuotientActionScalar_eq_residueAction [Q.IsMaximal]
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (z : (normalizationResidueFieldObject A L Q).α) :
    actualNormalizationQuotientActionScalar A K L Q d z =
      normalizationResidueActionScalar A L Q
        ((normalizationResidueMorphism A K L Q).hom'.toFun d) z

def

actualNormalizationResidueFieldMap

L66 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationResidueFieldMap

Documentation

The SAME action transported to the fixed localization residue field.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier)

Lean source · statement

def actualNormalizationResidueFieldMap [Q.IsMaximal]
    (d : (normalizationDecompositionGroup A K L Q).carrier) :
    Q.ResidueField →+* Q.ResidueField

theorem

actualNormalizationResidueFieldMap_coefficient

L72 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationResidueFieldMap_coefficient

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier)

Lean source · statement

theorem actualNormalizationResidueFieldMap_coefficient [Q.IsMaximal]
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (b : (normalizationCommAlgCat A L).carrier) :
    (actualNormalizationResidueFieldMap A K L Q d).toFun
        ((algebraMap (normalizationCommAlgCat A L).carrier Q.ResidueField).toFun b) =
      (algebraMap (normalizationCommAlgCat A L).carrier Q.ResidueField).toFun
        ((normalizationGaloisRingHom A K L d.val).toFun b)

Module documentation

The actual original decomposition action on residue coefficients

Declarations

actualNormalizationQuotientAction

actualNormalizationQuotientActionScalar

actualNormalizationQuotientActionScalar_apply

actualNormalizationQuotientActionScalar_eq_residueAction

actualNormalizationResidueFieldMap

actualNormalizationResidueFieldMap_coefficient