Module

NativeSeparableRootsRestriction.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeSeparableRootsRestriction

7 declarations indexed from sourceView source ↗

Module documentation

Separable roots compared with a cofinal set of actual degrees

The two constructed equivalences are composed only after the coefficient field and cofinal restriction owners have proved their own coordinate laws.

Imports2

Imported by2

def

nativeRestrictedRootsGroup

L29 ↗

EtaleFundamentalGroups.Inertia.nativeRestrictedRootsGroup

Documentation

The native group of the literal restricted roots system, with its existing operations.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory ProCGroups.InverseSystems
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
  (T : Set (InvertibleExponent k))

Lean source · statement

def nativeRestrictedRootsGroup : GrpCat.{v}

instance

nativeRestrictedRootsGroup_topology

L32 ↗

EtaleFundamentalGroups.Inertia.nativeRestrictedRootsGroup_topology

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory ProCGroups.InverseSystems
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
  (T : Set (InvertibleExponent k))

Lean source · statement

instance nativeRestrictedRootsGroup_topology :
    TopologicalSpace (nativeRestrictedRootsGroup k E T).carrier

def

nativeRestrictedRootsScalar

L37 ↗

EtaleFundamentalGroups.Inertia.nativeRestrictedRootsScalar

Documentation

The retained scalar coordinate, closing the restricted stage owner.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory ProCGroups.InverseSystems
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
  (T : Set (InvertibleExponent k))

Lean source · statement

def nativeRestrictedRootsScalar (t : T)
    (x : (nativeRestrictedRootsGroup k E T).carrier) : E.α

def

nativeFullRootsRestrictionEquiv

L45 ↗

EtaleFundamentalGroups.Inertia.nativeFullRootsRestrictionEquiv

Documentation

The native full roots group restricts to the original cofinal subsystem.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory ProCGroups.InverseSystems
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
  (T : Set (InvertibleExponent k))
variable
  (hT : ∀ n : InvertibleExponent k, ∃ t : T, n ≤ t.val)

Lean source · statement

def nativeFullRootsRestrictionEquiv :
    (nativeFullRootsGroup k E).carrier ≃ₜ*
      (nativeRestrictedRootsGroup k E T).carrier

theorem

nativeFullRootsRestrictionEquiv_scalar

L52 ↗

EtaleFundamentalGroups.Inertia.nativeFullRootsRestrictionEquiv_scalar

Documentation

The native cofinal equivalence is the original retained-coordinate map.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory ProCGroups.InverseSystems
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
  (T : Set (InvertibleExponent k))
variable
  (hT : ∀ n : InvertibleExponent k, ∃ t : T, n ≤ t.val)

Lean source · statement

theorem nativeFullRootsRestrictionEquiv_scalar
    (t : T) (x : (nativeFullRootsGroup k E).carrier) :
    nativeRestrictedRootsScalar k E T t
      ((nativeFullRootsRestrictionEquiv k E T hT).toFun x) =
      nativeFullRootsScalar k E t.val x

def

nativeSeparableRootsRestrictionEquiv

L64 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableRootsRestrictionEquiv

Documentation

The actual root inclusion followed by the proved cofinal restriction.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory ProCGroups.InverseSystems
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
  (T : Set (InvertibleExponent k))
variable
  (hT : ∀ n : InvertibleExponent k, ∃ t : T, n ≤ t.val)
variable (a : Algebra k E.α)

Lean source · statement

def nativeSeparableRootsRestrictionEquiv :
    (nativeSeparableRootsGroup k E a).carrier ≃ₜ*
      (nativeRestrictedRootsGroup k E T).carrier

theorem

nativeSeparableRootsRestrictionEquiv_scalar

L71 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableRootsRestrictionEquiv_scalar

Documentation

Every retained scalar is inclusion of the same separable-root coordinate.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory ProCGroups.InverseSystems
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
  (T : Set (InvertibleExponent k))
variable
  (hT : ∀ n : InvertibleExponent k, ∃ t : T, n ≤ t.val)
variable (a : Algebra k E.α)

Lean source · statement

theorem nativeSeparableRootsRestrictionEquiv_scalar
    (t : T) (x : (nativeSeparableRootsGroup k E a).carrier) :
    nativeRestrictedRootsScalar k E T t
      ((nativeSeparableRootsRestrictionEquiv k E T hT a).toFun x) =
      nativeSeparableRootsScalar k E a t.val x

Module documentation

Separable roots compared with a cofinal set of actual degrees

Declarations

nativeRestrictedRootsGroup

nativeRestrictedRootsGroup_topology

nativeRestrictedRootsScalar

nativeFullRootsRestrictionEquiv

nativeFullRootsRestrictionEquiv_scalar

nativeSeparableRootsRestrictionEquiv

nativeSeparableRootsRestrictionEquiv_scalar