Module

ProfiniteInertiaMap.lean

Nyll.SchemeTheory.RingTheory.Ramification.ProfiniteInertiaMap

4 declarations indexed from sourceView source ↗

Module documentation

Inertia images through a profinite invariant kernel

The finite invariant-kernel argument extends to a compact totally disconnected kernel acting continuously on the discrete ring. The two substantial inputs are the existing profinite prime-orbit theorem and the existing surjectivity of the quotient stabilizer action. The ring and group maps remain literal.

Imports7

Mathlib.RingTheory.Invariant.Basic
Mathlib.RingTheory.Invariant.Profinite
Mathlib.RingTheory.Ideal.Defs
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Pointwise
Mathlib.RingTheory.Ideal.Quotient.Basic
Mathlib.Topology.Algebra.MulAction

Imported by3

theorem

kernel_smulCommClass

L38 ↗

SchemeTheory.kernel_smulCommClass

Source context 4 commands

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

noncomputable section
open MulAction
open scoped Pointwise
namespace SchemeTheory

Lean source · statement

theorem kernel_smulCommClass
    {R S G G' : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Group G] [Group G'] [MulSemiringAction G S] [MulSemiringAction G' R]
    (f : G →* G') (H : Subgroup G) (hH : H ≤ f.ker)
    (hf : ∀ g x, algebraMap R S (f g • x) = g • algebraMap R S x) :
    SMulCommClass H R S

theorem

exists_inertia_correction_of_profinite

L54 ↗

SchemeTheory.exists_inertia_correction_of_profinite

Documentation

A profinite invariant kernel corrects a quotient action without changing its original base residues. Quotient rings and their one canonical scalar action occur only in this separate proof scope.

Source context 4 commands

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

noncomputable section
open MulAction
open scoped Pointwise
namespace SchemeTheory

Lean source · statement

theorem exists_inertia_correction_of_profinite
    {R S G : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Group G] [MulSemiringAction G S]
    (H : Subgroup G) [SMulCommClass H R S] [Algebra.IsInvariant R S H]
    [TopologicalSpace H] [CompactSpace H] [TotallyDisconnectedSpace H]
    [IsTopologicalGroup H] [TopologicalSpace S] [DiscreteTopology S] [ContinuousSMul H S]
    (p : Ideal R) (q : Ideal S) [q.LiesOver p] [q.IsPrime]
    (g : stabilizer G q)
    (hg : ∀ x : R, (g : G) • algebraMap R S x - algebraMap R S x ∈ q) :
    ∃ h : H, (h : G)⁻¹ * (g : G) ∈ q.inertia G

theorem

map_stabilizer_of_surjective_of_profinite

L96 ↗

SchemeTheory.map_stabilizer_of_surjective_of_profinite

Documentation

A surjective equivariant group map with profinite invariant kernel surjects on the stabilizers of the actual prime and its contraction.

Source context 6 commands

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

noncomputable section
open MulAction
open scoped Pointwise
namespace SchemeTheory
section Maps
variable {R S G G' : Type*} [CommRing R] [CommRing S] [Algebra R S]
  [Group G] [Group G'] [MulSemiringAction G S] [MulSemiringAction G' R]
  (f : G →* G') (H : Subgroup G) [Algebra.IsInvariant R S H]
  [TopologicalSpace H] [CompactSpace H] [TotallyDisconnectedSpace H]
  [IsTopologicalGroup H] [TopologicalSpace S] [DiscreteTopology S] [ContinuousSMul H S]
  (p : Ideal R) (q : Ideal S) [q.LiesOver p] [q.IsPrime]

Lean source · statement

theorem map_stabilizer_of_surjective_of_profinite
    (hf_surj : Function.Surjective f) (hf_ker : H ≤ f.ker)
    (hf : ∀ g x, algebraMap R S (f g • x) = g • algebraMap R S x) :
    (stabilizer G q).map f = stabilizer G' p

theorem

map_inertia_of_surjective_of_profinite

L125 ↗

SchemeTheory.map_inertia_of_surjective_of_profinite

Documentation

The original finite invariant-kernel inertia-image theorem with a profinite kernel. Every residue correction is supplied by the existing profinite quotient-action surjectivity theorem; no image equality is assumed.

Source context 6 commands

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

noncomputable section
open MulAction
open scoped Pointwise
namespace SchemeTheory
section Maps
variable {R S G G' : Type*} [CommRing R] [CommRing S] [Algebra R S]
  [Group G] [Group G'] [MulSemiringAction G S] [MulSemiringAction G' R]
  (f : G →* G') (H : Subgroup G) [Algebra.IsInvariant R S H]
  [TopologicalSpace H] [CompactSpace H] [TotallyDisconnectedSpace H]
  [IsTopologicalGroup H] [TopologicalSpace S] [DiscreteTopology S] [ContinuousSMul H S]
  (p : Ideal R) (q : Ideal S) [q.LiesOver p] [q.IsPrime]

Lean source · statement

theorem map_inertia_of_surjective_of_profinite
    (hf_surj : Function.Surjective f) (hf_ker : H ≤ f.ker)
    (hf : ∀ g x, algebraMap R S (f g • x) = g • algebraMap R S x) :
    (q.inertia G).map f = p.inertia G'

Module documentation

Inertia images through a profinite invariant kernel

Declarations

kernel_smulCommClass

exists_inertia_correction_of_profinite

map_stabilizer_of_surjective_of_profinite

map_inertia_of_surjective_of_profinite