Module

ActualFiniteQuotientTameProperties.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteQuotientTameProperties

2 declarations indexed from sourceView source ↗

Module documentation

Surjectivity and local constancy of the finite quotient coordinate

The proved original finite-coordinate properties are preserved by the SAME canonical quotient comparison. Its root carriers and coefficient dictionaries remain inside their existing single-stage owners.

Imports3

Imported by3

theorem

actualFiniteQuotientTameCoordinate_surjective

L33 ↗

EtaleFundamentalGroups.Inertia.actualFiniteQuotientTameCoordinate_surjective

Documentation

The actual finite quotient coordinate is onto.

Source context 4 commands

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

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]
  (E : FiniteGaloisIntermediateField K L)

Lean source · statement

theorem actualFiniteQuotientTameCoordinate_surjective :
    Function.Surjective (actualFiniteQuotientTameCoordinate A K L Q E).toFun

theorem

actualFiniteQuotientTameCoordinate_isLocallyConstant

L41 ↗

EtaleFundamentalGroups.Inertia.actualFiniteQuotientTameCoordinate_isLocallyConstant