NYLL
Module

ProfiniteRingActionRestriction.lean

Nyll.SchemeTheory.RingTheory.Ramification.ProfiniteRingActionRestriction
12 declarations indexed from sourceView source ↗

Module documentation

A data-only boundary for profinite ring-action restrictions

The diagram stores ordinary ring/group/action/map/topology data only. In particular it stores no equivariance, invariance, surjectivity, contraction, stabilizer-image, or inertia-image proof. These facts must be proved for a concrete diagram before the ordinary image theorem can be applied.

Imports4
Imported by3

Declarations

structure

RingActionRestriction

L31 ↗
SchemeTheory.RingActionRestriction
Documentation

Ordinary data for a restriction of ring actions. No comparison or image theorem is part of this structure.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
Lean source · full declaration
structure RingActionRestriction where
  /-- The lower ring. -/
  lowerRing : CommRingCat.{u}
  /-- The upper ring. -/
  upperRing : CommRingCat.{v}
  /-- The upper acting group. -/
  upperGroup : GrpCat.{w}
  /-- The lower acting group. -/
  lowerGroup : GrpCat.{x}
  /-- The prescribed action on the upper ring. -/
  upperAction : MulSemiringAction upperGroup.carrier upperRing.carrier
  /-- The prescribed action on the lower ring. -/
  lowerAction : MulSemiringAction lowerGroup.carrier lowerRing.carrier
  /-- The literal coefficient inclusion. -/
  ringMap : lowerRing.carrier →+* upperRing.carrier
  /-- The prescribed group restriction. -/
  groupMap : upperGroup.carrier →* lowerGroup.carrier
  /-- The subgroup that will correct lifts. -/
  kernelGroup : Subgroup upperGroup.carrier
  /-- Its prescribed topology. -/
  kernelTopology : TopologicalSpace kernelGroup
def

upperInertia

L56 ↗
SchemeTheory.RingActionRestriction.upperInertia
Documentation

Upper inertia for the diagram's prescribed action.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · statement
def upperInertia (D : RingActionRestriction) (q : Ideal D.upperRing.carrier) :
    Subgroup D.upperGroup.carrier
def

lowerInertia

L62 ↗
SchemeTheory.RingActionRestriction.lowerInertia
Documentation

Lower inertia for the diagram's prescribed action.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · statement
def lowerInertia (D : RingActionRestriction) (p : Ideal D.lowerRing.carrier) :
    Subgroup D.lowerGroup.carrier
def

upperDecomposition

L68 ↗
SchemeTheory.RingActionRestriction.upperDecomposition
Documentation

Upper decomposition group for the prescribed action.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · statement
def upperDecomposition (D : RingActionRestriction) (q : Ideal D.upperRing.carrier) :
    Subgroup D.upperGroup.carrier
def

lowerDecomposition

L74 ↗
SchemeTheory.RingActionRestriction.lowerDecomposition
Documentation

Lower decomposition group for the prescribed action.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · statement
def lowerDecomposition (D : RingActionRestriction) (p : Ideal D.lowerRing.carrier) :
    Subgroup D.lowerGroup.carrier
def

HasFixedPreimages

L81 ↗
SchemeTheory.RingActionRestriction.HasFixedPreimages
Documentation

Every element fixed by the prescribed kernel comes from the literal lower coefficient map. This is a hypothesis to prove, never stored data.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · statement
def HasFixedPreimages (D : RingActionRestriction) : Prop
def

IsEquivariant

L88 ↗
SchemeTheory.RingActionRestriction.IsEquivariant
Documentation

The actual action square, stated before introducing any ring algebra.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · statement
def IsEquivariant (D : RingActionRestriction) : Prop
def

HasOpenFixedSets

L97 ↗
SchemeTheory.RingActionRestriction.HasOpenFixedSets
Documentation

Open fixed sets for the prescribed kernel topology and upper action.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · statement
def HasOpenFixedSets (D : RingActionRestriction) : Prop
theorem

isInvariant_of_fixedPreimages

L103 ↗
SchemeTheory.RingActionRestriction.isInvariant_of_fixedPreimages
Documentation

The literal ring-map algebra has precisely the supplied fixed preimages.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · full declaration
theorem isInvariant_of_fixedPreimages (D : RingActionRestriction)
    (hfixed : D.HasFixedPreimages) :
    let : MulSemiringAction D.upperGroup.carrier D.upperRing.carrier := D.upperAction
    let : Algebra D.lowerRing.carrier D.upperRing.carrier := D.ringMap.toAlgebra
    Algebra.IsInvariant D.lowerRing.carrier D.upperRing.carrier D.kernelGroup := by
  intro upperAction ringAlgebra
  constructor
  intro b hb
  exact hfixed b (fun g hg => hb ⟨g, hg⟩)
theorem

liesOver_of_contraction

L114 ↗
SchemeTheory.RingActionRestriction.liesOver_of_contraction
Documentation

The literal ring-map algebra realizes the supplied contraction.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · full declaration
theorem liesOver_of_contraction (D : RingActionRestriction)
    (p : Ideal D.lowerRing.carrier) (q : Ideal D.upperRing.carrier)
    (hcontract : ∀ a : D.lowerRing.carrier, p.carrier a ↔ q.carrier (D.ringMap.toFun a)) :
    let : Algebra D.lowerRing.carrier D.upperRing.carrier := D.ringMap.toAlgebra
    q.LiesOver p := by
  intro ringAlgebra
  constructor
  apply Ideal.ext
  intro a
  exact hcontract a
theorem

continuousSMul_of_openFixedSets

L127 ↗
SchemeTheory.RingActionRestriction.continuousSMul_of_openFixedSets
Documentation

Open fixed sets give continuity for the prescribed kernel action on its discrete coefficient ring, without the lower group or ring algebra.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · full declaration
theorem continuousSMul_of_openFixedSets (D : RingActionRestriction)
    (hopen : D.HasOpenFixedSets) :
    let : MulSemiringAction D.upperGroup.carrier D.upperRing.carrier := D.upperAction
    let : TopologicalSpace D.kernelGroup := D.kernelTopology
    let : TopologicalSpace D.upperRing.carrier := ⊥
    IsTopologicalGroup D.kernelGroup → ContinuousSMul D.kernelGroup D.upperRing.carrier := by
  intro upperAction kernelTopology ringTopology htopological
  have : DiscreteTopology D.upperRing.carrier := ⟨rfl⟩
  exact continuousSMul_iff_stabilizer_isOpen.mpr hopen
theorem

images_of_profinite

L140 ↗
SchemeTheory.RingActionRestriction.images_of_profinite
Documentation

A compact zero-dimensional correcting kernel gives both decomposition and inertia images. The only scalar extension and discrete ring topology are introduced here, after every field constructor has been eliminated.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped Pointwise
universe u v w x
namespace RingActionRestriction
Lean source · full declaration
theorem images_of_profinite (D : RingActionRestriction)
    (p : Ideal D.lowerRing.carrier) (q : Ideal D.upperRing.carrier) [hq : q.IsPrime] :
    let : TopologicalSpace D.kernelGroup := D.kernelTopology
    CompactSpace D.kernelGroup → TotallyDisconnectedSpace D.kernelGroup →
    IsTopologicalGroup D.kernelGroup →
    (∀ a : D.lowerRing.carrier, p.carrier a ↔ q.carrier (D.ringMap.toFun a)) →
    D.HasFixedPreimages → D.HasOpenFixedSets →
    Function.Surjective D.groupMap.toFun →
    (∀ g : D.upperGroup.carrier, D.kernelGroup.carrier g → D.groupMap.toFun g = 1) →
    D.IsEquivariant →
    (D.upperDecomposition q).map D.groupMap = D.lowerDecomposition p ∧
      (D.upperInertia q).map D.groupMap = D.lowerInertia p := by
  intro kernelTopology hcompact hdisconnected htopological
    hcontract hfixed hopen hsurj hker hequiv
  let : MulSemiringAction D.upperGroup.carrier D.upperRing.carrier := D.upperAction
  let : MulSemiringAction D.lowerGroup.carrier D.lowerRing.carrier := D.lowerAction
  let : Algebra D.lowerRing.carrier D.upperRing.carrier := D.ringMap.toAlgebra
  let : TopologicalSpace D.upperRing.carrier := ⊥
  have : DiscreteTopology D.upperRing.carrier := ⟨rfl⟩
  have hcontinuous := continuousSMul_of_openFixedSets D hopen htopological
  have hinvariant := isInvariant_of_fixedPreimages D hfixed
  have hover := liesOver_of_contraction D p q hcontract
  have hcomm (g : D.upperGroup.carrier) (a : D.lowerRing.carrier) :=
    congrArg (fun j : D.lowerRing.carrier →+* D.upperRing.carrier => j.toFun a)
      (hequiv g)
  exact ⟨map_stabilizer_of_surjective_of_profinite D.groupMap D.kernelGroup p q
      hsurj (fun g hg => hker g hg) hcomm,
    map_inertia_of_surjective_of_profinite D.groupMap D.kernelGroup p q
      hsurj (fun g hg => hker g hg) hcomm⟩

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