NYLL
Module

ActualTameCoordinateSurjectivity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCoordinateSurjectivity
2 declarations indexed from sourceView source ↗

Module documentation

Surjective actual-degree coordinates and primitive roots

The proved original finite-coordinate surjection is transported by the SAME canonical quotient comparison. Actual finite primitive roots are transported by that comparison as well. No root-existence or surjectivity is assumed.

Imports4
Imported by3

Declarations

theorem

actualTameCoordinate_surjective

L36 ↗
EtaleFundamentalGroups.Inertia.actualTameCoordinate_surjective
Documentation

Every actual-degree coordinate is onto the full root group in the literal normalization quotient.

Source context 5 commands

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

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 actualTameCoordinate_surjective
    (n : Subtype (actualFiniteTameDegreeSet A K L Q)) :
    Function.Surjective (actualTameCoordinate A K L Q n).toFun
theorem

actualFiniteTameDegreeSet_exists_primitiveRoot

L45 ↗
EtaleFundamentalGroups.Inertia.actualFiniteTameDegreeSet_exists_primitiveRoot
Documentation

Each degree in the literal actual range has a primitive root in the SAME literal normalization quotient.

Source context 5 commands

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

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 actualFiniteTameDegreeSet_exists_primitiveRoot
    (n : Subtype (actualFiniteTameDegreeSet A K L Q)) :
    ∃ ζ : (normalizationCommAlgCat A L).carrier ⧸ Q, IsPrimitiveRoot ζ n.val.val

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.