Module

ActualTameRootsSeparableEquiv.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsSeparableEquiv

10 declarations indexed from sourceView source ↗

Module documentation

The actual equivariant separable tame-roots comparison

The coefficient inclusion is restricted along the proved cofinality of the SAME actual finite tame-degree range. Its inverse is the requested continuous group equivalence from the SAME actual roots group to the full separable roots limit. The coordinate square identifies both original decomposition actions, rather than defining one by transport.

Imports3

Imported by4

def

actualSeparableRootsComparisonHomeomorph

L36 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparisonHomeomorph

Documentation

The actual cofinal comparison as a homeomorphism, before group structures are joined.

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 actualSeparableRootsComparisonHomeomorph :
    (normalizationSeparableRootsGroup A Ω Q).carrier ≃ₜ
      (actualTameRootsGroup A K Ω Q).carrier

def

actualSeparableRootsComparisonMulEquiv

L43 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparisonMulEquiv

Documentation

The same actual cofinal comparison as a multiplicative equivalence.

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 actualSeparableRootsComparisonMulEquiv :
    (normalizationSeparableRootsGroup A Ω Q).carrier ≃*
      (actualTameRootsGroup A K Ω Q).carrier

theorem

actualSeparableRootsComparisonMulEquiv_toFun

L50 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparisonMulEquiv_toFun

Documentation

Both constructed comparisons have the exact same forward 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 actualSeparableRootsComparisonMulEquiv_toFun :
    (actualSeparableRootsComparisonMulEquiv A K Ω Q).toFun =
      (actualSeparableRootsComparisonHomeomorph A K Ω Q).toFun

def

actualSeparableRootsComparison

L55 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparison

Documentation

Assemble continuity and multiplication after the actual degree interface has closed.

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

def

actualSeparableRootsComparison_apply

L63 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparison_apply

Documentation

Plain application closes the comparison's topology and group dictionaries.

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 actualSeparableRootsComparison_apply
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    (actualTameRootsGroup A K Ω Q).carrier

theorem

actualSeparableRootsComparison_toFun

L70 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparison_toFun

Documentation

The assembled continuous group equivalence retains the literal comparison 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 actualSeparableRootsComparison_toFun :
    (actualSeparableRootsComparison A K Ω Q).toFun =
      actualSeparableRootsComparison_apply A K Ω Q

theorem

actualSeparableRootsComparison_scalar

L75 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparison_scalar

Documentation

The characteristic retained-coordinate law of the actual 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 actualSeparableRootsComparison_scalar
    (n : Subtype (actualFiniteTameDegreeSet A K Ω Q))
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    actualTameRootsScalar A K Ω Q n (actualSeparableRootsComparison_apply A K Ω Q x) =
      normalizationSeparableRootsScalar A Ω Q n.val x

theorem

actualSeparableRootsComparison_equivariant

L84 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsComparison_equivariant

Documentation

Root inclusion and cofinal restriction intertwine the SAME original D 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 actualSeparableRootsComparison_equivariant
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    actualSeparableRootsComparison_apply A K Ω Q (actualSeparableRootsAction_apply A K Ω Q d x) =
      actualTameRootsAction_apply A K Ω Q d (actualSeparableRootsComparison_apply A K Ω Q x)

def