NYLL
Module

ActualAbsoluteTameQuotient.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualAbsoluteTameQuotient
5 declarations indexed from sourceView source ↗

Module documentation

The SAME tame quotient is the full separable roots limit

Compose the existing continuous quotient equivalence with the actual separable-roots equivalence. The representative law retains the original quotient projection and the literal postcomposed character.

Imports5
Imported by2

Declarations

def

actualAbsoluteTameQuotient_apply

L36 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameQuotient_apply
Documentation

The quotient's actual function, before joining its quotient topology.

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 actualAbsoluteTameQuotient_apply
    (x : (actualTameQuotientGroup A K Ω Q).carrier) :
    (normalizationSeparableRootsGroup A Ω Q).carrier
theorem

actualAbsoluteTameQuotient_apply_projection

L43 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameQuotient_apply_projection
Documentation

The actual function retains the SAME representative computation.

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 actualAbsoluteTameQuotient_apply_projection
    (σ : (actualNormalizationInertiaGroup A K Ω Q).carrier) :
    actualAbsoluteTameQuotient_apply A K Ω Q
        ((actualTameQuotientProjection A K Ω Q).hom'.toFun σ) =
      (actualAbsoluteTameCharacterMorphism A K Ω Q).hom'.toFun σ
def

actualAbsoluteTameQuotientEquiv

L52 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameQuotientEquiv
Documentation

The original I/P with its quotient topology is the full separable roots limit.

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 actualAbsoluteTameQuotientEquiv :
    (actualTameQuotientGroup A K Ω Q).carrier ≃ₜ*
      (normalizationSeparableRootsGroup A Ω Q).carrier
theorem

actualAbsoluteTameQuotientEquiv_toFun

L58 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameQuotientEquiv_toFun
Documentation

The continuous equivalence retains the previously computed actual function.

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 actualAbsoluteTameQuotientEquiv_toFun :
    (actualAbsoluteTameQuotientEquiv A K Ω Q).toMulEquiv.toFun =
      actualAbsoluteTameQuotient_apply A K Ω Q
theorem

actualAbsoluteTameQuotientEquiv_projection

L63 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteTameQuotientEquiv_projection
Documentation

A representative maps to the SAME canonical absolute tame character.

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 actualAbsoluteTameQuotientEquiv_projection
    (σ : (actualNormalizationInertiaGroup A K Ω Q).carrier) :
    (actualAbsoluteTameQuotientEquiv A K Ω Q).toMulEquiv.toFun
        ((actualTameQuotientProjection A K Ω Q).hom'.toFun σ) =
      (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.