Module

NormalizationSeparableRoots.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationSeparableRoots

13 declarations indexed from sourceView source ↗

Module documentation

The full separable roots target of the original normalization

The residue field, its algebra, and the relative separable closure are constructed once in the existing field owner. This layer contains no fraction-field or original decomposition-group data.

Imports2

Imported by3

def

normalizationSeparableRootsGroup

L31 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsGroup

Documentation

The full invertible-exponent roots limit in the actual relative separable closure.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsGroup : GrpCat.{w}

instance

normalizationSeparableRootsGroup_topology

L35 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsGroup_topology

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

instance normalizationSeparableRootsGroup_topology :
    TopologicalSpace (normalizationSeparableRootsGroup A Ω Q).carrier

def

normalizationSeparableRootsScalar

L41 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsScalar

Documentation

A full separable-root coordinate viewed in the literal normalization quotient.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsScalar
    (n : InvertibleExponent (IsLocalRing.ResidueField A))
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    (normalizationCommAlgCat A Ω).carrier ⧸ Q

def

normalizationSeparableRootsAction

L49 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsAction

Documentation

The same separable residue group acts through its actual coefficient action.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsAction :
    (normalizationResidueSeparableGroup A Ω Q).carrier →*
      Equiv.Perm (normalizationSeparableRootsGroup A Ω Q).carrier

def

normalizationSeparableRootsAction_apply

L56 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsAction_apply

Documentation

Plain application closes the action's permutation data in this owner.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsAction_apply
    (σ : (normalizationResidueSeparableGroup A Ω Q).carrier)
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    (normalizationSeparableRootsGroup A Ω Q).carrier

def

normalizationSeparableRootsRestrictionEquiv

L63 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionEquiv

Documentation

Comparison with any cofinal subsystem of the literal quotient roots.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsRestrictionEquiv
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) :
    (normalizationSeparableRootsGroup A Ω Q).carrier ≃ₜ*
      (nativeRestrictedRootsGroup (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) T).carrier

theorem

normalizationSeparableRootsRestrictionEquiv_scalar

L74 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionEquiv_scalar

Documentation

The comparison is specified by the actual inclusion on retained scalar coordinates.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableRootsRestrictionEquiv_scalar
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) (t : T)
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    nativeRestrictedRootsScalar (IsLocalRing.ResidueField A)
      (normalizationResidueFieldObject A Ω Q) T t
        ((normalizationSeparableRootsRestrictionEquiv A Ω Q T hT).toFun x) =
      normalizationSeparableRootsScalar A Ω Q t.val x

def

normalizationSeparableRootsRestrictionMap

L87 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionMap

Documentation

The literal forward comparison, with group and topology dictionaries closed in this owner.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsRestrictionMap
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) :
    (normalizationSeparableRootsGroup A Ω Q).carrier →
      (nativeRestrictedRootsGroup (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) T).carrier

theorem

normalizationSeparableRootsRestrictionMap_scalar

L97 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionMap_scalar

Documentation

Scalar computation for the plain forward map requires no topology at the consumer.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableRootsRestrictionMap_scalar
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) (t : T)
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    nativeRestrictedRootsScalar (IsLocalRing.ResidueField A)
      (normalizationResidueFieldObject A Ω Q) T t
        (normalizationSeparableRootsRestrictionMap A Ω Q T hT x) =
      normalizationSeparableRootsScalar A Ω Q t.val x

def

normalizationSeparableRootsRestrictionHomeomorph

L109 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionHomeomorph

Documentation

The actual comparison's homeomorphism, before the original degree data is supplied.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsRestrictionHomeomorph
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) :
    (normalizationSeparableRootsGroup A Ω Q).carrier ≃ₜ
      (nativeRestrictedRootsGroup (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) T).carrier

theorem

normalizationSeparableRootsRestrictionHomeomorph_toFun

L119 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionHomeomorph_toFun

Documentation

The homeomorphism and plain compatible-family comparison share the exact forward function.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableRootsRestrictionHomeomorph_toFun
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) :
    (normalizationSeparableRootsRestrictionHomeomorph A Ω Q T hT).toFun =
      normalizationSeparableRootsRestrictionMap A Ω Q T hT

def

normalizationSeparableRootsRestrictionMulEquiv

L127 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionMulEquiv

Documentation

The actual comparison's multiplicative equivalence, independently of its topology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def normalizationSeparableRootsRestrictionMulEquiv
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) :
    (normalizationSeparableRootsGroup A Ω Q).carrier ≃*
      (nativeRestrictedRootsGroup (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) T).carrier

theorem

normalizationSeparableRootsRestrictionHomeomorph_scalar

L137 ↗

EtaleFundamentalGroups.Inertia.normalizationSeparableRootsRestrictionHomeomorph_scalar

Documentation

The topology-only comparison still retains precisely the same included scalar.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory ProCGroups.InverseSystems
universe u w
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

theorem normalizationSeparableRootsRestrictionHomeomorph_scalar
    (T : Set (InvertibleExponent (IsLocalRing.ResidueField A)))
    (hT : ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : T, n ≤ t.val) (t : T)
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    nativeRestrictedRootsScalar (IsLocalRing.ResidueField A)
      (normalizationResidueFieldObject A Ω Q) T t
        ((normalizationSeparableRootsRestrictionHomeomorph A Ω Q T hT).toFun x) =
      normalizationSeparableRootsScalar A Ω Q t.val x

Module documentation

The full separable roots target of the original normalization

Declarations