Module

ActualFiniteQuotientTameValue.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteQuotientTameValue

3 declarations indexed from sourceView source ↗

Module documentation

Scalar values of the actual finite quotient coordinate

The scalar is the projection of the SAME constructed quotient coordinate. Its canonical normalized-raw evaluation closes the root group at one stage; subsequent tower comparisons can work entirely with scalars.

Imports3

Imported by3

def

actualFiniteQuotientTameValue

L36 ↗

EtaleFundamentalGroups.Inertia.actualFiniteQuotientTameValue

Documentation

The scalar projection of the actual finite quotient coordinate.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
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

def actualFiniteQuotientTameValue (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (normalizationCommAlgCat A L).carrier ⧸ Q

theorem

actualFiniteQuotientTameValue_eq_residue

L43 ↗

EtaleFundamentalGroups.Inertia.actualFiniteQuotientTameValue_eq_residue

Documentation

The quotient scalar is the canonical quotient comparison of the original finite root scalar. The comparison involves only one finite stage.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
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 actualFiniteQuotientTameValue_eq_residue
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    actualFiniteQuotientTameValue A K L Q E σ =
      (normalizationMaximalQuotientResidueEquiv A L Q).symm.toFun
        ((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ).val.val

theorem

actualFiniteQuotientTameValue_eq_normalizationMap

L52 ↗

EtaleFundamentalGroups.Inertia.actualFiniteQuotientTameValue_eq_normalizationMap

Documentation

The actual quotient scalar agrees with the independently constructed raw value and its actual e/n normalization.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
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 actualFiniteQuotientTameValue_eq_normalizationMap
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    actualFiniteQuotientTameValue A K L Q E σ =
      (normalizationMaximalQuotientResidueEquiv A L Q).symm.toFun
        ((actualFiniteTameNormalizationMap A K L Q E).toFun
          (actualFiniteRawTameValue A K L Q E σ))

Module documentation

Scalar values of the actual finite quotient coordinate

Declarations

actualFiniteQuotientTameValue

actualFiniteQuotientTameValue_eq_residue

actualFiniteQuotientTameValue_eq_normalizationMap