NYLL
Module

ActualAbsoluteTameCharacter.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualAbsoluteTameCharacter
7 declarations indexed from sourceView source ↗

Module documentation

The original tame character into the full separable roots limit

Postcompose the SAME actual character with the proved full separable-roots comparison. Continuity, surjectivity, the SAME independent wild kernel and the original decomposition equivariance follow from their actual suppliers. No new character coordinates, subgroup or transported action are introduced.

Imports10
Imported by4

Declarations

def

actualAbsoluteTameCharacterMorphism

L42 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameCharacterMorphism
Documentation

The SAME character, followed by the actual full separable-roots comparison.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
def actualAbsoluteTameCharacterMorphism :
    GrpCat.Hom (actualNormalizationInertiaGroup A K Ω Q)
      (normalizationSeparableRootsGroup A Ω Q)
theorem

actualAbsoluteTameCharacterMorphism_map_apply

L49 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameCharacterMorphism_map_apply
Documentation

The group-map computation closes the comparison topology before later proofs.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteTameCharacterMorphism_map_apply
    (σ : (actualNormalizationInertiaGroup A K Ω Q).carrier) :
    (actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.toFun σ =
      (actualTameRootsSeparableMap A K Ω Q).hom'.toFun
        ((actualTameCharacterMorphism A K Ω Q).hom'.toFun σ)
theorem

actualAbsoluteTameCharacterMorphism_apply

L56 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameCharacterMorphism_apply
Documentation

The absolute character is literally the prescribed postcomposition.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteTameCharacterMorphism_apply
    (σ : (actualNormalizationInertiaGroup A K Ω Q).carrier) :
    (actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.toFun σ =
      (actualTameRootsSeparableEquiv A K Ω Q).toFun
        ((actualTameCharacterMorphism A K Ω Q).hom'.toFun σ)
theorem

actualAbsoluteTameCharacter_continuous

L63 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameCharacter_continuous
Documentation

The canonical character into the full separable roots limit is continuous.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteTameCharacter_continuous :
    Continuous (actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.toFun
theorem

actualAbsoluteTameCharacter_surjective

L69 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameCharacter_surjective
Documentation

The canonical character reaches every compatible family at every invertible exponent.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteTameCharacter_surjective :
    Function.Surjective (actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.toFun
theorem

actualAbsoluteTameCharacter_ker

L75 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameCharacter_ker
Documentation

Postcomposition retains precisely the independently defined original wild subgroup.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteTameCharacter_ker :
    (actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.ker =
      actualNormalizationWildSubgroup A K Ω Q
theorem

actualAbsoluteTameCharacter_conjugate

L84 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameCharacter_conjugate
Documentation

Original conjugation agrees with the SAME actual absolute residue action.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteTameCharacter_conjugate
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (σ : (actualNormalizationInertiaGroup A K Ω Q).carrier) :
    (actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.toFun
        (originalFiniteNormalizationInertiaConjugate A K Ω Q d σ) =
      actualSeparableRootsAction_apply A K Ω Q d
        ((actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.toFun σ)

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