Module

PrimeToRootsSeparableClosure.lean

Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsSeparableClosure

5 declarations indexed from sourceView source ↗

Module documentation

The actual prime-to-characteristic limit is unchanged by separable closure

The stage maps are the canonical field inclusions on roots of unity. Their bijectivity was proved from polynomial separability, and the actual power transition theorem proves the required compatibility. The native stagewise inverse-system theorem supplies the continuous multiplicative limit equivalence without any assumed inverse-limit comparison.

Imports4

Imported by2

def

primeToRootsSeparableClosureSystemIso

L32 ↗

EtaleFundamentalGroups.Inertia.primeToRootsSeparableClosureSystemIso

Documentation

The actual inclusion of the relative separable closure is a compatible isomorphism at every prime-to-characteristic roots stage.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v

Lean source · statement

def primeToRootsSeparableClosureSystemIso
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] :
    InverseSystem.InverseSystemIso
      (primeToRootsSystem k (separableClosure k E)) (primeToRootsSystem k E)

def

primeToRootsSeparableClosureLimitMap

L41 ↗

EtaleFundamentalGroups.Inertia.primeToRootsSeparableClosureLimitMap

Documentation

Plain inclusion of compatible root families, before group/topology comparison.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v

Lean source · statement

def primeToRootsSeparableClosureLimitMap
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] :
    (primeToRootsSystem k (separableClosure k E)).inverseLimit →
      (primeToRootsSystem k E).inverseLimit

theorem

primeToRootsSeparableClosureLimitMap_scalar

L49 ↗

EtaleFundamentalGroups.Inertia.primeToRootsSeparableClosureLimitMap_scalar

Documentation

The plain inclusion has the actual subtype scalar at each full exponent.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v

Lean source · statement

theorem primeToRootsSeparableClosureLimitMap_scalar
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E]
    (n : InvertibleExponent k)
    (x : (primeToRootsSystem k (separableClosure k E)).inverseLimit) :
    ((primeToRootsSystem k E).projection n
      (primeToRootsSeparableClosureLimitMap k E x)).val.val =
      (((primeToRootsSystem k (separableClosure k E)).projection n x).val.val).val

def

primeToRootsSeparableClosureLimitEquiv

L59 ↗

EtaleFundamentalGroups.Inertia.primeToRootsSeparableClosureLimitEquiv

Documentation

The full prime-to-characteristic roots limit over an extension is canonically the same as the one over its relative separable closure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v

Lean source · statement

def primeToRootsSeparableClosureLimitEquiv
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] :
    (primeToRootsSystem k (separableClosure k E)).inverseLimit ≃ₜ*
      (primeToRootsSystem k E).inverseLimit

theorem

primeToRootsSeparableClosureLimitEquiv_toFun

L66 ↗

EtaleFundamentalGroups.Inertia.primeToRootsSeparableClosureLimitEquiv_toFun

Documentation

The continuous group equivalence retains the already constructed plain inclusion.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u v

Lean source · statement

theorem primeToRootsSeparableClosureLimitEquiv_toFun
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] :
    (primeToRootsSeparableClosureLimitEquiv k E).toFun =
      primeToRootsSeparableClosureLimitMap k E

Module documentation

The actual prime-to-characteristic limit is unchanged by separable closure

Declarations

primeToRootsSeparableClosureSystemIso

primeToRootsSeparableClosureLimitMap

primeToRootsSeparableClosureLimitMap_scalar

primeToRootsSeparableClosureLimitEquiv

primeToRootsSeparableClosureLimitEquiv_toFun