Module

ActualFiniteResidueAction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteResidueAction

3 declarations indexed from sourceView source ↗

Module documentation

The actual finite restricted decomposition residue action

This is the existing intrinsic stabilizer residue morphism evaluated on the actual finite restriction, with its literal coefficient formula.

Imports3

Imported by3

theorem

actualFiniteNormalizationPrime_isMaximal

L33 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationPrime_isMaximal

Documentation

The literal finite prime is maximal because it is a nonzero Dedekind prime.

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] [IsDomain A] [IsDiscreteValuationRing 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) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteNormalizationPrime_isMaximal (E : FiniteGaloisIntermediateField K L) :
    (finiteAbsoluteNormalizationPrime A K L Q E).IsMaximal

def

actualFiniteDecompositionResidueFieldMap

L41 ↗

EtaleFundamentalGroups.Inertia.actualFiniteDecompositionResidueFieldMap

Documentation

The actual finite stabilizer acts on its residue field through the SAME native morphism.

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] [IsDomain A] [IsDiscreteValuationRing 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) [Q.IsMaximal]

Lean source · full declaration

def actualFiniteDecompositionResidueFieldMap (E : FiniteGaloisIntermediateField K L)
    (d : (normalizationDecompositionGroup A K L Q).carrier) :
    let : (finiteAbsoluteNormalizationPrime A K L Q E).IsPrime :=
      finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    (finiteAbsoluteNormalizationPrime A K L Q E).ResidueField →+*
      (finiteAbsoluteNormalizationPrime A K L Q E).ResidueField := by
  intro finitePrime
  have : (finiteAbsoluteNormalizationPrime A K L Q E).IsMaximal :=
    actualFiniteNormalizationPrime_isMaximal A K L Q E
  exact commAlgDecompositionResidueRingHom A (finiteAbsoluteNormalizationAlgebra A K L E)
    (finiteAbsoluteNormalizationPrime A K L Q E)
    ((actualFiniteDecompositionRestriction A K L Q E).hom'.toFun d)

theorem

actualFiniteDecompositionResidueFieldMap_coefficient

L54 ↗

EtaleFundamentalGroups.Inertia.actualFiniteDecompositionResidueFieldMap_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] [IsDomain A] [IsDiscreteValuationRing 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) [Q.IsMaximal]

Lean source · full declaration

theorem actualFiniteDecompositionResidueFieldMap_coefficient
    (E : FiniteGaloisIntermediateField K L)
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (b : (finiteAbsoluteNormalizationAlgebra A K L E).carrier) :
    let : (finiteAbsoluteNormalizationPrime A K L Q E).IsPrime :=
      finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    (actualFiniteDecompositionResidueFieldMap A K L Q E d).toFun
        ((algebraMap (finiteAbsoluteNormalizationAlgebra A K L E).carrier
          (finiteAbsoluteNormalizationPrime A K L Q E).ResidueField).toFun b) =
      (algebraMap (finiteAbsoluteNormalizationAlgebra A K L E).carrier
        (finiteAbsoluteNormalizationPrime A K L Q E).ResidueField).toFun
        ((actualFiniteNormalizationRestrictionRingHom A K L E d.val).toFun b) := by
  intro finitePrime
  have : (finiteAbsoluteNormalizationPrime A K L Q E).IsMaximal :=
    actualFiniteNormalizationPrime_isMaximal A K L Q E
  exact commAlgStabilizerResidueRingHom_coefficient A
    (finiteAbsoluteNormalizationAlgebra A K L E)
    (finiteAbsoluteNormalizationPrime A K L Q E)
    ((actualFiniteDecompositionRestriction A K L Q E).hom'.toFun d) b

Module documentation

The actual finite restricted decomposition residue action

Declarations

actualFiniteNormalizationPrime_isMaximal

actualFiniteDecompositionResidueFieldMap

actualFiniteDecompositionResidueFieldMap_coefficient