NYLL
Module

FiniteGaloisRestrictionGroupMap.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteGaloisRestrictionGroupMap
2 declarations indexed from sourceView source ↗

Module documentation

Restriction to finite Galois group objects

Defines the Galois group object of a finite intermediate field and the restriction homomorphism from the ambient Galois group.

Imports4
Imported by7

Declarations

def

finiteGaloisGroupObject

L30 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisGroupObject
Documentation

The native Galois group 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 finiteGaloisGroupObject (E : FiniteGaloisIntermediateField K L) : GrpCat.{v}
def

finiteGaloisRestrictionGroupMap

L34 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisRestrictionGroupMap
Documentation

Actual restriction from the original ambient Galois group.

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 · full declaration
def finiteGaloisRestrictionGroupMap (E : FiniteGaloisIntermediateField K L) :
    GrpCat.Hom (galoisGroupObject K L) (finiteGaloisGroupObject K L E) where
  hom' := AlgEquiv.restrictNormalHom E

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.