Socle-level constructions

This file contains the p-socle and its interaction with the Ulm filtration.

def UlmsTheorem.pSocle (p : ℕ) {G : Type u_1} [AddCommGroup G] : AddSubgroup G

The p-socle P = {x | p • x = 0}.

Equations

• UlmsTheorem.pSocle p = { carrier := {x : G | p • x = 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem UlmsTheorem.mem_pSocle (p : ℕ) {G : Type u_1} [AddCommGroup G] (x : G) : x ∈ pSocle p ↔ p • x = 0

noncomputable def UlmsTheorem.pSocleAt (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : AddSubgroup G

The filtered socle P_α = P ∩ G_α.

Equations

• UlmsTheorem.pSocleAt p α = UlmsTheorem.pSocle p ⊓ UlmsTheorem.ulmSubgroup p α

@[simp]

theorem UlmsTheorem.mem_pSocleAt (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) (x : G) : x ∈ pSocleAt p α ↔ p • x = 0 ∧ x ∈ ulmSubgroup p α

theorem UlmsTheorem.pSocleAt_zero (p : ℕ) {G : Type u_1} [AddCommGroup G] : pSocleAt p 0 = pSocle p

theorem UlmsTheorem.pSocleAt_antitone (p : ℕ) {G : Type u_1} [AddCommGroup G] : Antitone fun (α : Ordinal.{u_2}) => pSocleAt p α

theorem UlmsTheorem.pSocleAt_succ_le (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : pSocleAt p (Order.succ α) ≤ pSocleAt p α

theorem UlmsTheorem.pSocleAt_le_pSocle (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : pSocleAt p α ≤ pSocle p

@[instance_reducible]

noncomputable instance UlmsTheorem.pSocleZModModule (p : ℕ) {G : Type u_1} [AddCommGroup G] : Module (ZMod p) ↥(pSocle p)

Equations

• UlmsTheorem.pSocleZModModule p = AddCommGroup.zmodModule ⋯

@[instance_reducible]

noncomputable instance UlmsTheorem.pSocleAtZModModule (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Module (ZMod p) ↥(pSocleAt p α)

Equations

• UlmsTheorem.pSocleAtZModModule p α = AddCommGroup.zmodModule ⋯

noncomputable def UlmsTheorem.pSocleAtSuccSubgroupOf (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : AddSubgroup ↥(pSocleAt p α)

P_{α+1} viewed as a subgroup of P_α.

Equations

• UlmsTheorem.pSocleAtSuccSubgroupOf p α = AddSubgroup.comap (UlmsTheorem.pSocleAt p α).subtype (UlmsTheorem.pSocleAt p (Order.succ α))

@[instance_reducible]

noncomputable instance UlmsTheorem.pSocleAtQuotModule (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Module (ZMod p) (↥(pSocleAt p α) ⧸ pSocleAtSuccSubgroupOf p α)

Equations

• UlmsTheorem.pSocleAtQuotModule p α = QuotientAddGroup.zmodModule ⋯