Module

ActualTameCoordinateIdentity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCoordinateIdentity

2 declarations indexed from sourceView source ↗

Module documentation

Identity detection at one actual tame degree

The SAME canonical quotient-root equivalence preserves and reflects identity. This comparison is proved before the global inverse-limit group is introduced.

Imports1

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCoordinate

Imported by2

theorem

actualTameCoordinate_at_stage

L32 ↗

EtaleFundamentalGroups.Inertia.actualTameCoordinate_at_stage

Documentation

Evaluation at the degree of any finite stage recovers its canonical coordinate, through the SAME canonical quotient comparison.

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_at_stage
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (actualTameCoordinate A K L Q
        ⟨actualFiniteStageTameIndex A K L Q E, E, rfl⟩).toFun σ =
      (normalizationQuotientRootsEquiv A L Q
        (actualFiniteStageTameOrder A K L Q E)).toFun
        ((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ)

theorem

actualTameCoordinate_eq_one_iff

L47 ↗

EtaleFundamentalGroups.Inertia.actualTameCoordinate_eq_one_iff