Module

ActualFiniteTameContinuity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameContinuity

2 declarations indexed from sourceView source ↗

Module documentation

Continuity of the existing canonical tame coordinates

The SAME constructed canonical coordinate is the composite of the locally constant actual finite inertia restriction with its finite character and residue-root inclusion. Its source keeps the original Krull subgroup topology.

Imports8

Imported by2

theorem

actualFiniteTameCoordinate_isLocallyConstant

L38 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_isLocallyConstant

Documentation

The existing canonical finite tame coordinate is locally constant for the original Krull subgroup topology.

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)) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteTameCoordinate_isLocallyConstant
    (E : FiniteGaloisIntermediateField K L) :
    IsLocallyConstant (actualFiniteTameCoordinate A K L Q E).hom'.toFun

theorem

actualFiniteTameCoordinate_continuous

L47 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_continuous