Module

ActualFiniteTameSurjectivity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameSurjectivity

3 declarations indexed from sourceView source ↗

Module documentation

Surjectivity of the actual finite tame coordinates

The finite canonical character is onto its full native root group. The finite residue embedding preserves that full root group, and the actual original inertia restriction is onto. Their SAME existing composite is therefore surjective. The same finite primitive root also gives a primitive root in the original ambient residue field.

Imports11

Imported by3

theorem

actualFiniteCanonicalTameMorphism_surjective

L44 ↗

EtaleFundamentalGroups.Inertia.actualFiniteCanonicalTameMorphism_surjective

Documentation

Exactness of the native finite normalization supplies surjectivity of the SAME actual finite canonical morphism.

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) [hQ : Q.IsMaximal]
  (E : FiniteGaloisIntermediateField K L)

Lean source · statement

theorem actualFiniteCanonicalTameMorphism_surjective :
    Function.Surjective (actualFiniteCanonicalTameMorphism A K L Q E).hom'.toFun

theorem

actualFiniteRootsGroupMap_surjective

L65 ↗

EtaleFundamentalGroups.Inertia.actualFiniteRootsGroupMap_surjective

Documentation

The SAME actual finite residue-root embedding is onto the full root group of the ambient residue field.

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) [hQ : Q.IsMaximal]
  (E : FiniteGaloisIntermediateField K L)

Lean source · statement

theorem actualFiniteRootsGroupMap_surjective :
    Function.Surjective (actualFiniteRootsGroupMap A K L Q E).hom'.toFun

theorem

actualFiniteTameCoordinate_surjective

L77 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_surjective

Documentation

Every ambient tame root is the value of the SAME actual finite coordinate on an original inertia element.

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) [hQ : Q.IsMaximal]
  (E : FiniteGaloisIntermediateField K L)

Lean source · statement

theorem actualFiniteTameCoordinate_surjective :
    Function.Surjective (actualFiniteTameCoordinate A K L Q E).hom'.toFun

Module documentation

Surjectivity of the actual finite tame coordinates

Declarations

actualFiniteCanonicalTameMorphism_surjective

actualFiniteRootsGroupMap_surjective

actualFiniteTameCoordinate_surjective