NYLL
Module

HenselianIntegralFiberAction.lean

Nyll.EtaleFundamentalGroups.Inertia.HenselianIntegralFiberAction
6 declarations indexed from sourceView source ↗

Module documentation

Stabilizers of the actual integral-fiber idempotents

The unique idempotent isolating a closed-fiber prime has exactly that prime's stabilizer. Over a local base with separably closed residue field, integrality makes the residue quotient purely inseparable, so the prime stabilizer is its inertia group. These are the group-action inputs for the invariant-factor projection in Stacks tag 0BST.

Imports11
  • Nyll.EtaleFundamentalGroups.Inertia.HenselianIntegralFiber
  • Mathlib.Algebra.Group.Idempotent
  • Mathlib.Algebra.Group.Subgroup.Map
  • Mathlib.Algebra.Ring.Action.Basic
  • Mathlib.FieldTheory.PurelyInseparable.Basic
  • Mathlib.RingTheory.Ideal.GoingUp
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.Ideal.Pointwise
  • Mathlib.RingTheory.Ideal.Quotient.Basic
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
Imported by3

Declarations

def

primeFiberPermutation

L43 ↗
EtaleFundamentalGroups.Inertia.primeFiberPermutation
Documentation

The original ring action induces its canonical permutation action on all actual primes over a fixed base ideal. No choice of orbit representatives or new action on the original ring is involved.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v w
variable (A : Type u) (R : Type v) (G : Type w)
  [CommRing A] [CommRing R] [Algebra A R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G A R]
Lean source · full declaration
def primeFiberPermutation (p : Ideal A) : G →* Equiv.Perm (p.primesOver R) where
  toFun g :=
    { toFun := fun q => Ideal.primesOver.mk p (g • q.val)
      invFun := fun q => Ideal.primesOver.mk p (g⁻¹ • q.val)
      left_inv := fun q => Subtype.ext (inv_smul_smul g q.val)
      right_inv := fun q => Subtype.ext (smul_inv_smul g q.val) }
  map_one' := by
    apply Equiv.ext
    intro q
    exact Subtype.ext (one_smul G q.val)
  map_mul' g h := by
    apply Equiv.ext
    intro q
    exact Subtype.ext (mul_smul g h q.val)
theorem

smul_isolating_support

L58 ↗
EtaleFundamentalGroups.Inertia.smul_isolating_support
Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v w
variable (A : Type u) (R : Type v) (G : Type w)
  [CommRing A] [CommRing R] [Algebra A R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G A R]
Lean source · statement
theorem smul_isolating_support (p : Ideal A) (q : Ideal R) (e : R)
    (hsupp : ∀ Q : Ideal R, Q.IsPrime → Q.LiesOver p → (e ∉ Q ↔ Q = q)) (g : G) :
    ∀ Q : Ideal R, Q.IsPrime → Q.LiesOver p → (g • e ∉ Q ↔ Q = g • q)
theorem

isolatingIdempotent_stabilizer_eq

L76 ↗
EtaleFundamentalGroups.Inertia.isolatingIdempotent_stabilizer_eq
Documentation

An actual isolating idempotent has precisely the stabilizer of its prescribed closed-fiber prime. The support hypotheses are supplied by existsUnique_idempotent_of_finite_integral_fiber.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v w
variable (A : Type u) (R : Type v) (G : Type w)
  [CommRing A] [CommRing R] [Algebra A R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G A R]
Lean source · statement
theorem isolatingIdempotent_stabilizer_eq [HenselianLocalRing A]
    [Algebra.IsIntegral A R]
    (hfinite : ((IsLocalRing.maximalIdeal A).primesOver R).Finite)
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)]
    (e : R) (he : IsIdempotentElem e)
    (hsupp : ∀ Q : Ideal R, Q.IsPrime → Q.LiesOver (IsLocalRing.maximalIdeal A) →
      (e ∉ Q ↔ Q = q)) :
    MulAction.stabilizer G e = MulAction.stabilizer G q
theorem

isolatingIdempotents_equivariant

L107 ↗
EtaleFundamentalGroups.Inertia.isolatingIdempotents_equivariant
Documentation

The actual prime-indexed isolating family is equivariant for the canonical permutations of its prime indices. Every equation follows from the uniqueness of the already constructed idempotents.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v w
variable (A : Type u) (R : Type v) (G : Type w)
  [CommRing A] [CommRing R] [Algebra A R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G A R]
Lean source · statement
theorem isolatingIdempotents_equivariant [HenselianLocalRing A]
    [Algebra.IsIntegral A R]
    (hfinite : ((IsLocalRing.maximalIdeal A).primesOver R).Finite)
    (e : ((IsLocalRing.maximalIdeal A).primesOver R) → R)
    (he : ∀ q, IsIdempotentElem (e q))
    (hsupp : ∀ (q : (IsLocalRing.maximalIdeal A).primesOver R) (Q : Ideal R),
      Q.IsPrime → Q.LiesOver (IsLocalRing.maximalIdeal A) → (e q ∉ Q ↔ Q = q.val))
    (g : G) (q : (IsLocalRing.maximalIdeal A).primesOver R) :
    g • e q = e (primeFiberPermutation A R G (IsLocalRing.maximalIdeal A) g q)
theorem

inertia_eq_stabilizer_of_integral_of_residue_isSepClosed

L128 ↗
EtaleFundamentalGroups.Inertia.inertia_eq_stabilizer_of_integral_of_residue_isSepClosed
Documentation

Over a local base with separably closed residue field, every element of the prime stabilizer acts trivially on the integral residue quotient. Thus the actual inertia subgroup equals the prime stabilizer, without a finite type or finite-group hypothesis.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v w
variable (A : Type u) (R : Type v) (G : Type w)
  [CommRing A] [CommRing R] [Algebra A R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G A R]
Lean source · statement
theorem inertia_eq_stabilizer_of_integral_of_residue_isSepClosed
    [IsLocalRing A] [IsSepClosed (IsLocalRing.ResidueField A)]
    [Algebra.IsIntegral A R]
    (q : Ideal R) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)] :
    q.inertia G = MulAction.stabilizer G q
theorem

isolatingIdempotent_stabilizer_eq_inertia_of_map

L161 ↗
EtaleFundamentalGroups.Inertia.isolatingIdempotent_stabilizer_eq_inertia_of_map
Documentation

An equivariant family mapping to an actual isolating idempotent has precisely the original prime's inertia as its selected stabilizer. The map need not be injective: one direction uses the literal image, and the other uses the prescribed permutation of the actual prime indices.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v w
variable (A : Type u) (R : Type v) (G : Type w)
  [CommRing A] [CommRing R] [Algebra A R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G A R]
Lean source · statement
theorem isolatingIdempotent_stabilizer_eq_inertia_of_map
    [HenselianLocalRing A] [IsSepClosed (IsLocalRing.ResidueField A)]
    [Algebra.IsIntegral A R]
    (hfinite : ((IsLocalRing.maximalIdeal A).primesOver R).Finite)
    {S : Type*} [CommRing S] [MulSemiringAction G S]
    (f : S →+* R) (hf : ∀ (g : G) (s : S), f (g • s) = g • f s)
    (q : (IsLocalRing.maximalIdeal A).primesOver R)
    (eS : ((IsLocalRing.maximalIdeal A).primesOver R) → S)
    (hσ : ∀ g : G, g • eS q =
      eS (primeFiberPermutation A R G (IsLocalRing.maximalIdeal A) g q))
    (e : R) (he : IsIdempotentElem e)
    (hsupp : ∀ Q : Ideal R, Q.IsPrime → Q.LiesOver (IsLocalRing.maximalIdeal A) →
      (e ∉ Q ↔ Q = q.val))
    (hmap : f (eS q) = e) :
    MulAction.stabilizer G (eS q) = q.val.inertia G

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