Module

ActualTameQuotientEquiv.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameQuotientEquiv

4 declarations indexed from sourceView source ↗

Module documentation

The SAME canonical tame character identifies I/P with the actual root limit

Surjectivity and the proved independent wild kernel give the first isomorphism theorem. The actual quotient projection descends continuity, and compactness upgrades this SAME map to a continuous group equivalence.

Imports9

Nyll.EtaleFundamentalGroups.Inertia.ActualTameQuotientGroup
Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacterKernel
Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacterSurjectivity
Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsGroup
Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationWildSubgroup
Nyll.EtaleFundamentalGroups.Inertia.OriginalNormalizationInertiaAction
Nyll.ProCGroups.Topologies.ContinuousMulEquiv
Mathlib.GroupTheory.QuotientGroup.Defs
Mathlib.Topology.Algebra.Group.Quotient

Imported by3

def

actualTameQuotientMulEquiv

L40 ↗

EtaleFundamentalGroups.Inertia.actualTameQuotientMulEquiv

Documentation

The first isomorphism theorem for the SAME theta and independent P.

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) (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

def actualTameQuotientMulEquiv :
    (actualTameQuotientGroup A K L Q).carrier ≃*
      (actualTameRootsGroup A K L Q).carrier

theorem

actualTameQuotientMulEquiv_projection

L50 ↗

EtaleFundamentalGroups.Inertia.actualTameQuotientMulEquiv_projection

Documentation

A representative is mapped to its SAME canonical character value.

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) (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 actualTameQuotientMulEquiv_projection
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (actualTameQuotientMulEquiv A K L Q).toFun
        ((actualTameQuotientProjection A K L Q).hom'.toFun σ) =
      (actualTameCharacterMorphism A K L Q).hom'.toFun σ

theorem

actualTameQuotientMulEquiv_continuous

L62 ↗

EtaleFundamentalGroups.Inertia.actualTameQuotientMulEquiv_continuous

Documentation

The SAME isomorphism is continuous for the original 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) (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 actualTameQuotientMulEquiv_continuous :
    Continuous (actualTameQuotientMulEquiv A K L Q).toFun

def