NYLL
Module

NormalizationGaloisInvariant.lean

Nyll.SchemeTheory.RingTheory.Ramification.NormalizationGaloisInvariant
14 declarations indexed from sourceView source ↗

Module documentation

Native Galois invariance of the actual integral closure

The prescribed normalization action is invariant over the original normal base. Field fixedness gives a fraction-field preimage. The integral-closure subtype supplies its integrality, and normality descends it to the base. The final proof uses the literal inclusion and the existing coefficient square, without opening an algebra from the integral closure to the field.

The descent specializes the proof of Algebra.isInvariant_of_isGalois: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/RingTheory/Invariant/Galois.lean Its field-fixedness, integrality, and normality facts are reused below.

Imports9
Imported by4

Declarations

def

normalizationInclusionRingHom

L41 ↗
EtaleFundamentalGroups.Inertia.normalizationInclusionRingHom
Documentation

The already constructed native inclusion, retained with its literal carrier.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
def normalizationInclusionRingHom
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F] :
    integralClosure A F →+* F
def

normalizationCoefficientRingHom

L47 ↗
EtaleFundamentalGroups.Inertia.normalizationCoefficientRingHom
Documentation

The already constructed native coefficient map on the same carrier.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
def normalizationCoefficientRingHom
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F] :
    A →+* integralClosure A F
theorem

normalizationInclusionRingHom_injective

L52 ↗
EtaleFundamentalGroups.Inertia.normalizationInclusionRingHom_injective
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem normalizationInclusionRingHom_injective
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F] :
    Function.Injective (normalizationInclusionRingHom A F).toFun
theorem

normalizationInclusionRingHom_comp_coefficient

L58 ↗
EtaleFundamentalGroups.Inertia.normalizationInclusionRingHom_comp_coefficient
Documentation

The existing subtype coefficient square, before Galois data occur.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem normalizationInclusionRingHom_comp_coefficient
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F] :
    (normalizationInclusionRingHom A F).comp (normalizationCoefficientRingHom A F) =
      algebraMap A F
theorem

galois_fixed_exists_field_coefficient

L65 ↗
EtaleFundamentalGroups.Inertia.galois_fixed_exists_field_coefficient
Documentation

A field fixed by its full Galois group is the original base field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem galois_fixed_exists_field_coefficient
    (K : Type v) (F : Type w) [Field K] [Field F] [Algebra K F]
    [IsGalois K F] (x : F)
    (hx : ∀ σ : Gal(F/K), σ.toRingHom.toFun x = x) :
    ∃ k : K, (algebraMap K F).toFun k = x
theorem

integral_field_preimage_exists_coefficient

L73 ↗
EtaleFundamentalGroups.Inertia.integral_field_preimage_exists_coefficient
Documentation

An integral image of a fraction-field element comes from the normal base.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem integral_field_preimage_exists_coefficient
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsIntegrallyClosed A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] (k : K)
    (hk : IsIntegral A ((algebraMap K F).toFun k)) :
    ∃ a : A, (algebraMap A F).toFun a = (algebraMap K F).toFun k
theorem

normalization_fixed_exists_coefficient

L92 ↗
EtaleFundamentalGroups.Inertia.normalization_fixed_exists_coefficient
Documentation

Fixed normalization elements descend using their literal subtype integrality.

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
section RawNormalizationAction
attribute [local instance] normalizationInertiaImageAction
Lean source · statement
theorem normalization_fixed_exists_coefficient
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsIntegrallyClosed A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [IsGalois K F]
    (b : integralClosure A F) (hb : ∀ σ : Gal(F/K), σ • b = b) :
    ∃ a : A, (normalizationCoefficientRingHom A F).toFun a = b
theorem

coefficientDescent_isInvariant

L121 ↗
EtaleFundamentalGroups.Inertia.coefficientDescent_isInvariant
Documentation

Construct the native invariant property only after coefficient descent is proved.

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
section RawNormalizationAction
attribute [local instance] normalizationInertiaImageAction
Lean source · statement
theorem coefficientDescent_isInvariant
    (A : Type u) (B G : Type w) [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B]
    (h : ∀ b : B, (∀ g : G, g • b = b) →
      ∃ a : A, (algebraMap A B).toFun a = b) : Algebra.IsInvariant A B G
theorem

integralClosure_isInvariant_of_isGalois

L134 ↗
EtaleFundamentalGroups.Inertia.integralClosure_isInvariant_of_isGalois
Documentation

The original possibly infinite Galois action on the literal integral closure is invariant over the original normal base. The proof uses the native subtype inclusion and does not instantiate the general integral-closure-to-field algebra interface of Algebra.isInvariant_of_isGalois.

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
section RawNormalizationAction
attribute [local instance] normalizationInertiaImageAction
Lean source · statement
theorem integralClosure_isInvariant_of_isGalois
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsIntegrallyClosed A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [IsGalois K F] :
    Algebra.IsInvariant A (integralClosure A F) Gal(F/K)
theorem

normalizationCommAlgInclusion_injective

L145 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlgInclusion_injective
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem normalizationCommAlgInclusion_injective
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F] :
    Function.Injective (normalizationCommAlgInclusion A F).toFun
theorem

normalizationCommAlgInclusion_comp_coefficient

L150 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlgInclusion_comp_coefficient
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem normalizationCommAlgInclusion_comp_coefficient
    (A : Type u) (F : Type w) [CommRing A] [CommRing F] [Algebra A F] :
    (normalizationCommAlgInclusion A F).comp
        (commAlgCoefficientMap (normalizationCommAlgCat A F)) = algebraMap A F
theorem

normalizationCommAlg_fixed_exists_coefficient

L160 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlg_fixed_exists_coefficient
Documentation

Fixed native normalization elements descend by the existing literal integrality and normality proof, along the stored coefficient map.

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
attribute [local instance] normalizationCommAlgGaloisAction
Lean source · statement
theorem normalizationCommAlg_fixed_exists_coefficient
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsIntegrallyClosed A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [IsGalois K F]
    (b : normalizationCommAlgCat A F) (hb : ∀ σ : Gal(F/K), σ • b = b) :
    ∃ a : A, (commAlgCoefficientMap (normalizationCommAlgCat A F)).toFun a = b
theorem

normalizationCommAlg_fixedSet_isOpen_krull

L170 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlg_fixedSet_isOpen_krull
Documentation

The actual native normalization stabilizers are open in the Krull topology.

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
attribute [local instance] normalizationCommAlgGaloisAction
Lean source · full declaration
theorem normalizationCommAlg_fixedSet_isOpen_krull
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [Algebra.IsAlgebraic K F]
    (b : normalizationCommAlgCat A F) : IsOpen (fun σ : Gal(F/K) => σ • b = b) :=
  integralClosure_fixedSet_isOpen_krull A K F b
theorem

normalizationCommAlg_action_comp_coefficient

L180 ↗
EtaleFundamentalGroups.Inertia.normalizationCommAlg_action_comp_coefficient
Documentation

The prescribed normalization action fixes the actual coefficient map. The proof cancels the literal inclusion and uses the native field square.

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
attribute [local instance] normalizationCommAlgGaloisAction
Lean source · statement
theorem normalizationCommAlg_action_comp_coefficient
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [IsGalois K F] (σ : Gal(F/K)) :
    (MulSemiringAction.toRingHom Gal(F/K) (normalizationCommAlgCat A F) σ).comp
        (commAlgCoefficientMap (normalizationCommAlgCat A F)) =
      commAlgCoefficientMap (normalizationCommAlgCat A F)

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