Module

ActualTameCharacterContinuity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacterContinuity

3 declarations indexed from sourceView source ↗

Module documentation

Continuity of the actual tame character

The original finite coordinates are locally constant in the original Krull subgroup topology. Their quotient-valued, degree-indexed coordinates retain local constancy, so the constructed map into the literal root limit is continuous.

Imports3

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacter
Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteQuotientTameProperties
Mathlib.Topology.LocallyConstant.Basic

Imported by3

theorem

actualTameCoordinate_isLocallyConstant

L35 ↗

EtaleFundamentalGroups.Inertia.actualTameCoordinate_isLocallyConstant

Documentation

The actual-degree coordinate retains local constancy for the SAME original inertia topology.

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_isLocallyConstant
    (n : Subtype (actualFiniteTameDegreeSet A K L Q)) :
    IsLocallyConstant (actualTameCoordinate A K L Q n).toFun

theorem

actualTameCoordinate_continuous

L44 ↗

EtaleFundamentalGroups.Inertia.actualTameCoordinate_continuous

Documentation

Every actual-degree coordinate is continuous for the topology of its literal stage in the existing root system.

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 · full declaration

theorem actualTameCoordinate_continuous
    (n : Subtype (actualFiniteTameDegreeSet A K L Q)) :
    Continuous (show (actualNormalizationInertiaGroup A K L Q).carrier →
      (actualFiniteTameRootsSystem A K L Q).X n from
        (actualTameCoordinate A K L Q n).toFun) :=
  IsLocallyConstant.continuous
    (Y := (actualFiniteTameRootsSystem A K L Q).X n)
    (actualTameCoordinate_isLocallyConstant A K L Q n)

theorem

actualTameCharacter_continuous

L55 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacter_continuous

Documentation

The actual canonical character is continuous from original inertia with its Krull subgroup topology into the literal quotient-root limit.

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 actualTameCharacter_continuous :
    Continuous (actualTameCharacter A K L Q).toFun

Module documentation

Continuity of the actual tame character

Declarations

actualTameCoordinate_isLocallyConstant

actualTameCoordinate_continuous

actualTameCharacter_continuous