NYLL
Module

FiniteGaloisInertiaCriterion.lean

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

Module documentation

Finite Galois quotients killing every original normalization inertia

The original inertia image theorem and lying over show that a finite Galois restriction kills all inertia in an arbitrary Galois normalization exactly when every inertia group in the finite normalization is trivial. Neither normalization is assumed module finite over the base.

Imports3
Imported by2

Declarations

theorem

exists_prime_comap_mapIntegralClosure

L24 ↗
EtaleFundamentalGroups.Inertia.exists_prime_comap_mapIntegralClosure
Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem exists_prime_comap_mapIntegralClosure
    {A : Type u} {R : Type v} {S : Type w}
    [CommRing A] [CommRing R] [CommRing S] [IsDomain S]
    [Algebra A R] [Algebra A S]
    (f : R →ₐ[A] S) (hf : Function.Injective f)
    (q : Ideal (integralClosure A R)) [q.IsPrime] :
    ∃ Q : Ideal (integralClosure A S), Q.IsPrime ∧
      Q.comap f.mapIntegralClosure = q
theorem

all_normalization_inertia_le_fixingSubgroup_iff

L59 ↗
EtaleFundamentalGroups.Inertia.all_normalization_inertia_le_fixingSubgroup_iff
Documentation

All original inertia in the possibly infinite normalization fixes a finite Galois subfield exactly when every original inertia in that finite normalization is trivial. Every finite prime is reached by lying over.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction
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
theorem all_normalization_inertia_le_fixingSubgroup_iff
    (E : FiniteGaloisIntermediateField K L) :
    (∀ (Q : Ideal (integralClosure A L)) [Q.IsPrime],
      Q.inertia Gal(L/K) ≤ E.toIntermediateField.fixingSubgroup) ↔
    ∀ (q : Ideal (integralClosure A E)) [q.IsPrime], q.inertia Gal(E/K) = ⊥

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