Multiplication and powers of categorical Hom ideals

The product of two two-sided additive Hom ideals is generated by composites through arbitrary intermediate objects. This file proves the elementary ideal arithmetic needed to state nilpotence of a categorical radical and to deduce separation of its power filtration.

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.IdealLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I J : HomIdeal C) : Prop

Pointwise inclusion of categorical Hom ideals.

@[instance_reducible]

instance MBDVendor.QSE.CategoricalIdeal.HomIdeal.instLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : LE (HomIdeal C)

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.le_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : HomIdeal C} : I ≤ J ↔ ∀ (X Y : C), I.hom X Y ≤ J.hom X Y

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.ext_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : HomIdeal C} (h : ∀ (X Y : C), I.hom X Y = J.hom X Y) : I = J

Two Hom ideals are equal when their Hom subgroups agree pointwise.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.ext_hom_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : HomIdeal C} : I = J ↔ ∀ (X Y : C), I.hom X Y = J.hom X Y

@[instance_reducible]

instance MBDVendor.QSE.CategoricalIdeal.HomIdeal.instPartialOrder {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : PartialOrder (HomIdeal C)

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.zero (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : HomIdeal C

The zero categorical Hom ideal.

@[instance_reducible]

instance MBDVendor.QSE.CategoricalIdeal.HomIdeal.instBot {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Bot (HomIdeal C)

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.bot_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) : ⊥.hom X Y = ⊥

@[instance_reducible]

instance MBDVendor.QSE.CategoricalIdeal.HomIdeal.instOrderBot {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : OrderBot (HomIdeal C)

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.whole (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : HomIdeal C

The whole categorical Hom ideal.

@[instance_reducible]

instance MBDVendor.QSE.CategoricalIdeal.HomIdeal.instTop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Top (HomIdeal C)

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.top_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Y : C) : ⊤.hom X Y = ⊤

@[instance_reducible]

instance MBDVendor.QSE.CategoricalIdeal.HomIdeal.instOrderTop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : OrderTop (HomIdeal C)

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.compositeGenerators {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I J : HomIdeal C) (X Z : C) : Set (X ⟶ Z)

Composites of one morphism from I followed by one from J.

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I J : HomIdeal C) : HomIdeal C

Product of two categorical Hom ideals: the additive subgroup generated by composites f ≫ g with f ∈ I and g ∈ J.

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.«term_⋆ᵢ_» : Lean.TrailingParserDescr

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.comp_mem_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : HomIdeal C} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : f ∈ I.hom X Y) (hg : g ∈ J.hom Y Z) : CategoryTheory.CategoryStruct.comp f g ∈ (I ⋆ᵢ J).hom X Z

A single allowed composite belongs to the product ideal.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.mul_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I I' J J' : HomIdeal C} (hI : I ≤ I') (hJ : J ≤ J') : I ⋆ᵢ J ≤ I' ⋆ᵢ J'

Multiplication is monotone in both variables.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.mul_le_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I J : HomIdeal C) : I ⋆ᵢ J ≤ I

Every product lies in its left factor, since the left factor is closed under postcomposition.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.mul_le_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I J : HomIdeal C) : I ⋆ᵢ J ≤ J

Every product lies in its right factor, since the right factor is closed under precomposition.

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.top_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : ⊤ ⋆ᵢ I = I

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.mul_top {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : I ⋆ᵢ ⊤ = I

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.bot_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : ⊥ ⋆ᵢ I = ⊥

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.mul_bot {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : I ⋆ᵢ ⊥ = ⊥

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.mul_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I J K : HomIdeal C) : I ⋆ᵢ J ⋆ᵢ K = I ⋆ᵢ (J ⋆ᵢ K)

Associativity follows from associativity and bilinearity of categorical composition; the closure induction accounts for finite additive sums.

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : ℕ → HomIdeal C

Right-recursive powers of a categorical Hom ideal. The zeroth power is the whole Hom ideal.

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : I.pow 0 = ⊤

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) (n : ℕ) : I.pow (n + 1) = I.pow n ⋆ᵢ I

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : I.pow 1 = I

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow_succ_eq_mul_pow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) (n : ℕ) : I.pow (n + 1) = I ⋆ᵢ I.pow n

Powers also have the left-recursive form.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : HomIdeal C} (hIJ : I ≤ J) (n : ℕ) : I.pow n ≤ J.pow n

Pointwise inclusion is preserved by every power.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow_succ_le_pow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) (n : ℕ) : I.pow (n + 1) ≤ I.pow n

Ideal powers form a descending chain.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.pow_le_pow_of_le {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) {m n : ℕ} (hmn : m ≤ n) : I.pow n ≤ I.pow m

Larger exponents give smaller powers.

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.powerIntersection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : HomIdeal C

The pointwise intersection of all powers.

@[simp]

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.mem_powerIntersection_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I : HomIdeal C} {X Y : C} {f : X ⟶ Y} : f ∈ I.powerIntersection.hom X Y ↔ ∀ (n : ℕ), f ∈ (I.pow n).hom X Y

def MBDVendor.QSE.CategoricalIdeal.HomIdeal.IsNilpotent {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : HomIdeal C) : Prop

A categorical Hom ideal is nilpotent if one of its powers is zero.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.powerIntersection_eq_bot_of_isNilpotent {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I : HomIdeal C} (hI : I.IsNilpotent) : I.powerIntersection = ⊥

Nilpotence forces the intersection of all powers to vanish.

theorem MBDVendor.QSE.CategoricalIdeal.HomIdeal.eq_zero_of_mem_every_power {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I : HomIdeal C} (hI : I.IsNilpotent) {X Y : C} {f : X ⟶ Y} (hf : ∀ (n : ℕ), f ∈ (I.pow n).hom X Y) : f = 0

Elementwise form of the same separatedness conclusion.