Module

IntegralClosureGaloisAction.lean

Nyll.EtaleFundamentalGroups.Inertia.IntegralClosureGaloisAction

2 declarations indexed from sourceView source ↗

Module documentation

The two actual Galois actions on an integral closure

The fraction-ring restriction used by ramification theory and the literal restriction used by normalization geometry agree on the embedded integral closure. The comparison follows by applying its injective inclusion into the common field, where both automorphisms are the original field automorphism.

Imports2

Nyll.EtaleFundamentalGroups.Inertia.AffineNormalizationGeometricPoint
Mathlib.RingTheory.Invariant.Galois

Imported by2

theorem

galRestrict_integralClosure_eq

L31 ↗

EtaleFundamentalGroups.Inertia.galRestrict_integralClosure_eq

Documentation

Fraction-ring restriction and literal restriction define the same homomorphism into the automorphisms of the integral closure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R K L : Type u) [CommRing R] [Field K] [Field L]
  [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L]
  [IsFractionRing R K] [Algebra.IsAlgebraic K L]

Lean source · statement

theorem galRestrict_integralClosure_eq :
    (galRestrict R K L (integralClosure R L)).toMonoidHom =
      (integralClosureAutHom R L).comp (AlgEquiv.restrictScalarsHom R)

theorem

integralClosureGaloisAction_eq

L43 ↗

EtaleFundamentalGroups.Inertia.integralClosureGaloisAction_eq