NYLL
Module

ActualTameRootsSeparableMap.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsSeparableMap
6 declarations indexed from sourceView source ↗

Module documentation

The actual separable roots comparison as a shared group morphism

The algebraic inverse comparison supplies the literal group map. Its function is the SAME continuous comparison; injectivity and surjectivity are proved before introducing topologies. The character consumes this actual map, so its kernel calculation does not reopen root topologies.

Imports4
Imported by3

Declarations

def

actualTameRootsSeparableMap

L36 ↗
EtaleFundamentalGroups.Inertia.actualTameRootsSeparableMap
Documentation

The SAME inverse comparison, with its group structure retained independently.

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 actualTameRootsSeparableMap :
    GrpCat.Hom (actualTameRootsGroup A K Ω Q) (normalizationSeparableRootsGroup A Ω Q)
theorem

actualTameRootsSeparableMap_toFun

L41 ↗
EtaleFundamentalGroups.Inertia.actualTameRootsSeparableMap_toFun
Documentation

The stored group map is exactly the proved continuous comparison's 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 actualTameRootsSeparableMap_toFun :
    (actualTameRootsSeparableMap A K Ω Q).hom'.toFun =
      (actualTameRootsSeparableEquiv A K Ω Q).toFun
theorem

actualTameRootsSeparableMap_injective

L46 ↗
EtaleFundamentalGroups.Inertia.actualTameRootsSeparableMap_injective
Documentation

Injectivity belongs to the actual algebraic inverse 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
theorem actualTameRootsSeparableMap_injective :
    Function.Injective (actualTameRootsSeparableMap A K Ω Q).hom'.toFun
theorem

actualTameRootsSeparableMap_surjective

L51 ↗
EtaleFundamentalGroups.Inertia.actualTameRootsSeparableMap_surjective
Documentation

Surjectivity belongs to that same algebraic inverse 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
theorem actualTameRootsSeparableMap_surjective :
    Function.Surjective (actualTameRootsSeparableMap A K Ω Q).hom'.toFun
theorem

actualTameRootsSeparableMap_continuous

L56 ↗
EtaleFundamentalGroups.Inertia.actualTameRootsSeparableMap_continuous
Documentation

The existing comparison topology makes the SAME stored group map 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 actualTameRootsSeparableMap_continuous :
    Continuous (actualTameRootsSeparableMap A K Ω Q).hom'.toFun
theorem

actualTameRootsSeparableMap_equivariant

L61 ↗
EtaleFundamentalGroups.Inertia.actualTameRootsSeparableMap_equivariant
Documentation

The stored map retains the two original decomposition actions.

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 actualTameRootsSeparableMap_equivariant
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (x : (actualTameRootsGroup A K Ω Q).carrier) :
    (actualTameRootsSeparableMap A K Ω Q).hom'.toFun
        (actualTameRootsAction_apply A K Ω Q d x) =
      actualSeparableRootsAction_apply A K Ω Q d
        ((actualTameRootsSeparableMap A K Ω Q).hom'.toFun x)

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