Module

FiniteRestrictionCoefficientSquare.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteRestrictionCoefficientSquare

5 declarations indexed from sourceView source ↗

Module documentation

Coefficient squares for finite field restriction

Defines the finite intermediate field ring object, its ambient inclusion, and individual Galois restriction maps, and proves their commuting square.

Imports3

Nyll.EtaleFundamentalGroups.Inertia.FiniteGaloisRestrictionGroupMap
Mathlib.Algebra.Category.Ring.Basic
Mathlib.FieldTheory.Normal.Defs

Imported by2

def

finiteIntermediateRingObject

L29 ↗

EtaleFundamentalGroups.Inertia.finiteIntermediateRingObject

Documentation

The actual finite field as a native coefficient ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]

Lean source · statement

def finiteIntermediateRingObject (E : FiniteGaloisIntermediateField K L) : CommRingCat.{v}

def

finiteIntermediateAmbientRingHom

L33 ↗

EtaleFundamentalGroups.Inertia.finiteIntermediateAmbientRingHom

Documentation

The literal inclusion of the actual finite intermediate field.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]

Lean source · statement

def finiteIntermediateAmbientRingHom (E : FiniteGaloisIntermediateField K L) :
    finiteIntermediateRingObject K L E →+* L

def

finiteGaloisRestrictionRingHom

L37 ↗

EtaleFundamentalGroups.Inertia.finiteGaloisRestrictionRingHom

Documentation

The individual actual finite field restriction, before any A-normalization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]

Lean source · statement

def finiteGaloisRestrictionRingHom (E : FiniteGaloisIntermediateField K L)
    (σ : Gal(L/K)) :
    finiteIntermediateRingObject K L E →+* finiteIntermediateRingObject K L E

theorem

finiteGaloisRestriction_native_square

L43 ↗

EtaleFundamentalGroups.Inertia.finiteGaloisRestriction_native_square

Documentation

Native field restriction before any categorical ring coercion occurs.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem finiteGaloisRestriction_native_square (E : FiniteGaloisIntermediateField K L)
    (σ : Gal(L/K)) :
    E.val.toRingHom.comp (AlgEquiv.restrictNormalHom E σ).toRingHom =
      σ.toRingHom.comp E.val.toRingHom

theorem

finiteGaloisRestrictionRingHom_commutes

L53 ↗

EtaleFundamentalGroups.Inertia.finiteGaloisRestrictionRingHom_commutes

Documentation

Actual finite restriction commutes with the actual field inclusion.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem finiteGaloisRestrictionRingHom_commutes (E : FiniteGaloisIntermediateField K L)
    (σ : Gal(L/K)) :
    (finiteIntermediateAmbientRingHom K L E).comp (finiteGaloisRestrictionRingHom K L E σ) =
      σ.toRingHom.comp (finiteIntermediateAmbientRingHom K L E)

Module documentation

Coefficient squares for finite field restriction

Declarations

finiteIntermediateRingObject

finiteIntermediateAmbientRingHom

finiteGaloisRestrictionRingHom

finiteGaloisRestriction_native_square

finiteGaloisRestrictionRingHom_commutes