Lemma 2.5 in the opposite category

graded-category.tex: "Applying these arguments to the opposite module category proves exactness of the second sequence in (1) and the assertion at injective labels." This file transfers the hypotheses of the abstract Lemma 2.5 (StrictLayers.strict) to Cᵒᵖ:

• the categorical radical and its powers are self-dual (isRadicalMorphism_op_iff, mem_Ipow_op_iff);
• the Krull–Schmidt target normal form of C (split epimorphism and radical map) is the source normal form of Cᵒᵖ (hasSplitRadicalNormalForm_op);
• a left tau-sequence Y → E → T with epic second map is a right radical approximation of Y in Cᵒᵖ (approxOfLeftTau).

theorem MultiplicativeBasisDeformations.StrictLayers.isRadicalMorphism_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f.op ↔ MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f

theorem MultiplicativeBasisDeformations.StrictLayers.isRadicalMorphism_unop_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f.unop ↔ MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f

theorem MultiplicativeBasisDeformations.StrictLayers.mem_Ipow_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {X Y : C} (f : X ⟶ Y) : f.op ∈ (Ipow n).hom (Opposite.op Y) (Opposite.op X) ↔ f ∈ (Ipow n).hom X Y

The powers of the radical are self-dual.

theorem MultiplicativeBasisDeformations.StrictLayers.mem_Ipow_unop_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop ∈ (Ipow n).hom (Opposite.unop Y) (Opposite.unop X) ↔ f ∈ (Ipow n).hom X Y

def MultiplicativeBasisDeformations.StrictLayers.HasSplitRadicalConormalForm (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : Prop

The Krull–Schmidt target normal form: after an isomorphism of its target, every map is a column of a split epimorphism and a radical map.

noncomputable def MultiplicativeBasisDeformations.StrictLayers.opBiprodIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y Z U : C} (e : Y ≅ Z ⊞ U) : Opposite.op Y ≅ Opposite.op Z ⊞ Opposite.op U

A biproduct decomposition in C gives one in Cᵒᵖ.

theorem MultiplicativeBasisDeformations.StrictLayers.hasSplitRadicalNormalForm_op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (h : HasSplitRadicalConormalForm C) : HasSplitRadicalNormalForm Cᵒᵖ

def MultiplicativeBasisDeformations.StrictLayers.IsWeakCok {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.ShortComplex C) : Prop

The weak cokernel property of the second map of a short complex.

theorem MultiplicativeBasisDeformations.StrictLayers.isWeakCok_of_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.ShortComplex C) (hM : MBDVendor.QSE.Iyama.LeftTauSequence M) : IsWeakCok M

theorem MultiplicativeBasisDeformations.StrictLayers.isWeakCok_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : CategoryTheory.ShortComplex C} (e : M ≅ N) (h : IsWeakCok N) : IsWeakCok M

theorem MultiplicativeBasisDeformations.StrictLayers.epi_g_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M N : CategoryTheory.ShortComplex C} (e : M ≅ N) [CategoryTheory.Epi N.g] : CategoryTheory.Epi M.g

def MultiplicativeBasisDeformations.StrictLayers.approxOfLeftTau {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {Y : C} (M : CategoryTheory.ShortComplex C) (hM : MBDVendor.QSE.Iyama.TauApproximation M) (hcok : IsWeakCok M) (hepi : CategoryTheory.Epi M.g) (e : M.X₁ ≅ Y) : RightRadicalApprox (Opposite.op Y)

A complex Y → E → T with the radical approximation property, whose epic second map is a weak cokernel of the first (a left tau-sequence), is a right radical approximation of Y in Cᵒᵖ: dually, every radical map out of Y factors through f, and every map in I²(T, Z) is q ∘ g with q radical.