Irreducible maps and binary biproducts #
This file formalizes the standard Butler--Ringel observation that two irreducible maps from one local object assemble to an irreducible map into a binary biproduct when every morphism between the two target summands is categorically radical. The dual statement treats a binary-biproduct source.
theorem
MagnitudeConjecture.CategoryTheory.isIrreducibleMorphism_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
{f : X ⟶ Y}
(hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f)
:
Negating a morphism preserves categorical irreducibility.
theorem
MagnitudeConjecture.CategoryTheory.isIrreducibleMorphism_biprod_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X Y₁ Y₂ : C}
[IsLocalRing (CategoryTheory.End X)]
(f₁ : X ⟶ Y₁)
(f₂ : X ⟶ Y₂)
(hf₁ : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f₁)
(hf₂ : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f₂)
(h₁₂ : ∀ (q : Y₁ ⟶ Y₂), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism q)
(h₂₁ : ∀ (q : Y₂ ⟶ Y₁), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism q)
:
QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.Limits.biprod.lift f₁ f₂)
Two irreducible maps with a common local source assemble to an irreducible map into a binary biproduct when both off-diagonal Hom groups are radical.
theorem
MagnitudeConjecture.CategoryTheory.isIrreducibleMorphism_biprod_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{Y₁ Y₂ Z : C}
[IsLocalRing (CategoryTheory.End Z)]
(g₁ : Y₁ ⟶ Z)
(g₂ : Y₂ ⟶ Z)
(hg₁ : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g₁)
(hg₂ : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g₂)
(h₁₂ : ∀ (q : Y₁ ⟶ Y₂), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism q)
(h₂₁ : ∀ (q : Y₂ ⟶ Y₁), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism q)
:
QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.Limits.biprod.desc g₁ g₂)
Two irreducible maps with a common local target assemble to an irreducible map out of a binary biproduct when both off-diagonal Hom groups are radical.