NYLL
Module

FiniteGaloisInvariantNeighborhood.lean

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

Module documentation

The finite-Galois normalization neighborhood in Stacks tag 0BSU

For a finite Galois extension of the fraction field of a normal domain, the canonical Galois action on its actual integral closure has the original normal domain as its full invariants. The literal invariant-base map is proved bijective; its algebra equivalence transports the original 0BST étale neighborhood to that original base.

This supplies the finite-Galois principal-neighborhood prerequisite of 0BSU. The arbitrary infinite inertia restriction and localized filtered-colimit comparisons are separate statements.

Imports8
  • Nyll.EtaleFundamentalGroups.Inertia.InvariantEtaleNeighborhood
  • Mathlib.Algebra.Algebra.Subalgebra.Basic
  • Mathlib.Algebra.Algebra.Subalgebra.Operations
  • Mathlib.Algebra.Algebra.Tower
  • Mathlib.RingTheory.Etale.Basic
  • Mathlib.RingTheory.Invariant.Galois
  • Mathlib.RingTheory.Localization.FractionRing
  • Mathlib.RingTheory.Localization.Integral
Imported by3

Declarations

theorem

exists_etale_away_of_invariant_base

L37 ↗
EtaleFundamentalGroups.Inertia.exists_etale_away_of_invariant_base
Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem exists_etale_away_of_invariant_base
    (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    (hinj : Function.Injective (algebraMap A B)) (q : Ideal B) [q.IsPrime] :
    ∃ f : FixedPoints.subalgebra A B (q.inertia G),
      (f : B) ∉ q ∧ Algebra.Etale A (Localization.Away f)
theorem

finiteGalois_integralClosure_inertia_exists_etale_away

L70 ↗
EtaleFundamentalGroups.Inertia.finiteGalois_integralClosure_inertia_exists_etale_away
Documentation

In a finite Galois normalization, every inertia-invariant localization at an original normalization prime has an actual principal neighborhood étale over the original normal domain. The full-invariant base comparison is proved from canonical Galois invariance and injectivity.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · full declaration
theorem finiteGalois_integralClosure_inertia_exists_etale_away
    (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]
    (q : Ideal (integralClosure A L)) [q.IsPrime] :
    let : MulSemiringAction Gal(L/K) (integralClosure A L) :=
      IsIntegralClosure.MulSemiringAction A K L (integralClosure A L)
    let : SMulCommClass Gal(L/K) A (integralClosure A L) := by
      constructor
      intro σ a b
      change (galRestrict A K L (integralClosure A L) σ) (a • b) =
        a • (galRestrict A K L (integralClosure A L) σ) b
      exact (galRestrict A K L (integralClosure A L) σ).toLinearMap.map_smul a b
    ∃ f : FixedPoints.subalgebra A (integralClosure A L) (q.inertia Gal(L/K)),
      (f : integralClosure A L) ∉ q ∧ Algebra.Etale A (Localization.Away f) := by
  intro actualAction actualComm
  have : IsFractionRing (integralClosure A L) L :=
    integralClosure.isFractionRing_of_finite_extension (A := A) K L
  have : Algebra.IsInvariant A (integralClosure A L) Gal(L/K) :=
    Algebra.isInvariant_of_isGalois A K L (integralClosure A L)
  exact exists_etale_away_of_invariant_base A (integralClosure A L) Gal(L/K)
    (algebraMap_injective_of_field_isFractionRing (R := A) (S := integralClosure A L) K L) q

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