Module

ActualFiniteNormalizationCoefficientSquare.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationCoefficientSquare

3 declarations indexed from sourceView source ↗

Module documentation

Coefficient squares for finite normalization restriction

Defines the ring maps underlying finite normalization restriction and ambient inclusion, and proves that their Galois action square commutes.

Imports3

Imported by9

def

actualFiniteNormalizationRestrictionRingHom

L33 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationRestrictionRingHom

Documentation

The individual actual restriction on the finite normalization, retained as a ring map before any coefficient square is compared.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]

Lean source · statement

def actualFiniteNormalizationRestrictionRingHom (E : FiniteGaloisIntermediateField K L)
    (σ : Gal(L/K)) :
    finiteAbsoluteNormalizationAlgebra A K L E →+* finiteAbsoluteNormalizationAlgebra A K L E

def

actualFiniteNormalizationAmbientRingHom

L40 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationAmbientRingHom

Documentation

The literal inclusion of the actual finite normalization into L.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]

Lean source · statement

def actualFiniteNormalizationAmbientRingHom (E : FiniteGaloisIntermediateField K L) :
    finiteAbsoluteNormalizationAlgebra A K L E →+* L

theorem

actualFiniteNormalizationRestrictionRingHom_commutes

L48 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationRestrictionRingHom_commutes

Documentation

The actual restricted coefficient action agrees with the original ambient automorphism on the literal normalization inclusion.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
omit [IsFractionRing A K] [IsGalois K L] in

Lean source · statement

theorem actualFiniteNormalizationRestrictionRingHom_commutes
    (E : FiniteGaloisIntermediateField K L) (σ : Gal(L/K)) :
    (actualFiniteNormalizationAmbientRingHom A K L E).comp
        (actualFiniteNormalizationRestrictionRingHom A K L E σ) =
      (galoisAutomorphismRingHom K L σ).comp
        (actualFiniteNormalizationAmbientRingHom A K L E)

Module documentation

Coefficient squares for finite normalization restriction

Declarations

actualFiniteNormalizationRestrictionRingHom

actualFiniteNormalizationAmbientRingHom

actualFiniteNormalizationRestrictionRingHom_commutes