Module

IntegralClosureAutomorphisms.lean

Nyll.SchemeTheory.Normalization.IntegralClosureAutomorphisms

1 declaration indexed from sourceView source ↗

Module documentation

Automorphisms of finite Galois integral closures

Proves that the algebra automorphism group of the integral closure in a finite Galois extension forms a Galois group over the integrally closed base domain.

Imports3

Mathlib.RingTheory.Invariant.Galois
Mathlib.RingTheory.IsGaloisGroup.Defs
Mathlib.RingTheory.DedekindDomain.IntegralClosure

Imported by6

theorem

integralClosure_automorphisms_isGaloisGroup

L25 ↗

SchemeTheory.integralClosure_automorphisms_isGaloisGroup

Documentation

The intrinsic automorphisms of an actual finite Galois normalization are its Galois group. The invariant-ring assertion is the native theorem proved through actual fraction-field restriction.

Source context 2 commands

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

namespace SchemeTheory
universe u v w

Lean source · statement

theorem integralClosure_automorphisms_isGaloisGroup
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [IsGalois K L] :
    IsGaloisGroup (integralClosure A L ≃ₐ[A] integralClosure A L) A (integralClosure A L)

Module documentation

Automorphisms of finite Galois integral closures

Declarations

integralClosure_automorphisms_isGaloisGroup