Module

NativeSeparableResidueGroup.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeSeparableResidueGroup

10 declarations indexed from sourceView source ↗

Module documentation

Separable residue Galois group objects

Constructs the automorphism-group comparison between a stored algebraic closure and its relative separable closure. Records preservation of surjectivity and kernels under target group isomorphisms.

Imports5

Nyll.EtaleFundamentalGroups.Inertia.NativeAbsoluteResidueFields
Nyll.EtaleFundamentalGroups.Inertia.SeparableClosureAutomorphisms
Mathlib.Algebra.Category.Grp.Basic
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Mathlib.Algebra.Group.Subgroup.Ker

Imported by7

def

nativeFieldAutomorphisms

L30 ↗

EtaleFundamentalGroups.Inertia.nativeFieldAutomorphisms

Documentation

Automorphisms of the actual stored field extension.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

def nativeFieldAutomorphisms (k : Type u) [Field k] (E : Bundled Field.{v})
    (a : Algebra k E) : GrpCat.{v}

def

nativeSeparableResidueGroup

L36 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableResidueGroup

Documentation

The actual relative separable-closure Galois group.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

def nativeSeparableResidueGroup (k : Type u) [Field k] (E : Bundled Field.{v})
    (a : Algebra k E) : GrpCat.{v}

def

nativeSeparableResidueIso

L43 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableResidueIso

Documentation

Restriction on the stored algebraic residue closure is the already proved actual separable-closure automorphism equivalence.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · full declaration

def nativeSeparableResidueIso (k : Type u) [Field k] (E : Bundled Field.{v})
    (a : Algebra k E) (h : letI := a; IsAlgClosure k E) :
    nativeFieldAutomorphisms k E a ≅ nativeSeparableResidueGroup k E a := by
  letI := a
  have : IsAlgClosure k E := h
  exact (separableClosureAutEquiv k E).toGrpIso

def

nativeSeparableResidueField

L53 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableResidueField

Documentation

The actual relative separable closure with its one stored field structure. This carrier owner keeps its coefficient algebra and subtype coercion out of original normalization statements.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

def nativeSeparableResidueField
    (k : Type u) [Field k] (E : Bundled Field.{v}) (a : Algebra k E.α) :
    Bundled Field.{v}

def

nativeSeparableResidueScalar

L60 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableResidueScalar

Documentation

The actual coefficient inclusion of the stored relative separable closure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

def nativeSeparableResidueScalar
    (k : Type u) [Field k] (E : Bundled Field.{v}) (a : Algebra k E.α)
    (z : (nativeSeparableResidueField k E a).α) : E.α

def

nativeFieldResidueActionScalar

L66 ↗

EtaleFundamentalGroups.Inertia.nativeFieldResidueActionScalar

Documentation

The stored field automorphism evaluated on a coefficient.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

def nativeFieldResidueActionScalar
    (k : Type u) [Field k] (E : Bundled Field.{v}) (a : Algebra k E.α)
    (σ : (nativeFieldAutomorphisms k E a).carrier) (z : E.α) : E.α

def

nativeSeparableResidueActionScalar

L74 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableResidueActionScalar

Documentation

The actual separable residue automorphism evaluated in the ambient field. Only the stored coefficient action is installed, inside this field owner.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

def nativeSeparableResidueActionScalar
    (k : Type u) [Field k] (E : Bundled Field.{v}) (a : Algebra k E.α)
    (τ : (nativeSeparableResidueGroup k E a).carrier)
    (z : (nativeSeparableResidueField k E a).α) : E.α

theorem

nativeSeparableResidueIso_commutes

L84 ↗

EtaleFundamentalGroups.Inertia.nativeSeparableResidueIso_commutes

Documentation

Restriction through the actual stored isomorphism preserves its ambient coefficient map. This is the defining restrictNormal square.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · full declaration

theorem nativeSeparableResidueIso_commutes
    (k : Type u) [Field k] (E : Bundled Field.{v}) (a : Algebra k E.α)
    (h : let := a; IsAlgClosure k E.α)
    (σ : (nativeFieldAutomorphisms k E a).carrier)
    (z : (nativeSeparableResidueField k E a).α) :
    nativeSeparableResidueActionScalar k E a
        ((nativeSeparableResidueIso k E a h).hom.hom'.toFun σ) z =
      nativeFieldResidueActionScalar k E a σ (nativeSeparableResidueScalar k E a z) := by
  let := a
  have : IsAlgClosure k E.α := h
  exact separableClosure_restrictNormal_coefficient k E.α (show E.α ≃ₐ[k] E.α from σ) z

theorem

nativeGroupMorphism_comp_iso_surjective

L97 ↗

EtaleFundamentalGroups.Inertia.nativeGroupMorphism_comp_iso_surjective

Documentation

Target transport by a genuine group isomorphism preserves surjectivity.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

theorem nativeGroupMorphism_comp_iso_surjective
    {D G H : GrpCat.{v}} (f : D ⟶ G) (e : G ≅ H)
    (hf : Function.Surjective f.hom'.toFun) :
    Function.Surjective (f ≫ e.hom).hom'.toFun

theorem

nativeGroupMorphism_comp_iso_ker

L104 ↗

EtaleFundamentalGroups.Inertia.nativeGroupMorphism_comp_iso_ker

Documentation

Target transport by that same isomorphism preserves the literal kernel.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v

Lean source · statement

theorem nativeGroupMorphism_comp_iso_ker
    {D G H : GrpCat.{v}} (f : D ⟶ G) (e : G ≅ H) :
    (f ≫ e.hom).hom'.ker = f.hom'.ker

Module documentation

Separable residue Galois group objects

Declarations