Module

ActualTameCharacterSurjectivity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacterSurjectivity

1 declaration indexed from sourceView source ↗

Module documentation

Surjectivity of the actual tame character

Compactness of the SAME original inertia, local constancy of the actual coordinates, their proved surjectivity, and directedness of the literal actual degree range supply the existing compact-limit theorem.

Imports5

Imported by4

theorem

actualTameCharacter_surjective

L32 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacter_surjective

Documentation

Every compatible family of actual-degree roots is the canonical tame character of an original inertia element. No compactness, continuity, comparison, coordinate-surjectivity or directedness premise is supplied.

Source context 4 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

Lean source · statement

theorem actualTameCharacter_surjective
    (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] :
    Function.Surjective (actualTameCharacter A K L Q).toFun

Module documentation

Surjectivity of the actual tame character

Declarations

actualTameCharacter_surjective