Module

ActualFiniteInertiaContinuity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaContinuity

4 declarations indexed from sourceView source ↗

Module documentation

Local constancy of actual finite inertia restriction

The coefficient automorphism underlying the SAME intrinsic finite inertia restriction factors through the locally constant finite Galois restriction. Injectivity of the intrinsic subgroup inclusion then proves local constancy without installing any replacement topology on the original inertia group.

Imports9

Imported by3

theorem

actualFiniteInertiaRestriction_coefficient

L37 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaRestriction_coefficient

Documentation

The constructor for actual intrinsic restriction has the prescribed coefficient automorphism.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
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]

Lean source · statement

theorem actualFiniteInertiaRestriction_coefficient
    (Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    ((actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ).val =
      (actualFiniteInertiaCoefficientMap A K L Q E).hom'.toFun σ

theorem

actualFiniteInertiaCoefficientMap_isLocallyConstant

L46 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaCoefficientMap_isLocallyConstant

Documentation

The existing coefficient restriction is locally constant on original inertia by restriction of the ambient coefficient map to its subgroup.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
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]

Lean source · statement

theorem actualFiniteInertiaCoefficientMap_isLocallyConstant
    (Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L) :
    IsLocallyConstant (actualFiniteInertiaCoefficientMap A K L Q E).hom'.toFun

theorem

actualFiniteInertiaRestriction_isLocallyConstant

L55 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaRestriction_isLocallyConstant

Documentation

Restricting actual original inertia to its intrinsic finite normalization inertia is locally constant for the original subgroup topology.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
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]

Lean source · statement

theorem actualFiniteInertiaRestriction_isLocallyConstant
    (Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L) :
    IsLocallyConstant (actualFiniteInertiaRestriction A K L Q E).hom'.toFun

theorem

actualFiniteInertiaRestriction_continuous

L76 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaRestriction_continuous

Documentation

The actual restriction is continuous into the discrete intrinsic finite group; more generally, it is continuous for any topology on that target.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
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]

Lean source · statement

theorem actualFiniteInertiaRestriction_continuous
    (Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L)
    [TopologicalSpace (commAlgIdealInertiaGroup A (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)).carrier] :
    Continuous (actualFiniteInertiaRestriction A K L Q E).hom'.toFun

Module documentation

Local constancy of actual finite inertia restriction

Declarations

actualFiniteInertiaRestriction_coefficient

actualFiniteInertiaCoefficientMap_isLocallyConstant

actualFiniteInertiaRestriction_isLocallyConstant

actualFiniteInertiaRestriction_continuous