Radical morphisms and minimal projective presentations #
This file records the generic radical calculus needed to recognize a minimal projective presentation after applying an exact additive functor. It also packages the componentwise criterion for radical maps between finite biproducts.
theorem
MagnitudeConjecture.CategoryTheory.isRadicalMorphism_iff_not_isSplitMono_of_local_end
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
[IsLocalRing (CategoryTheory.End X)]
(hX : ¬CategoryTheory.Limits.IsZero X)
(f : X ⟶ Y)
:
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f ↔ ¬CategoryTheory.IsSplitMono f
A morphism with nonzero local source is radical exactly when it is not split monic.
theorem
MagnitudeConjecture.CategoryTheory.isRadicalMorphism_iff_not_isSplitEpi_of_local_end
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
[IsLocalRing (CategoryTheory.End Y)]
(hY : ¬CategoryTheory.Limits.IsZero Y)
(f : X ⟶ Y)
:
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f ↔ ¬CategoryTheory.IsSplitEpi f
A morphism into a nonzero object with local endomorphism ring is radical exactly when it is not split epic.
theorem
MagnitudeConjecture.CategoryTheory.not_isSplitMono_of_isRadicalMorphism
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
(hX : ¬CategoryTheory.Limits.IsZero X)
{f : X ⟶ Y}
(hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f)
:
¬CategoryTheory.IsSplitMono f
A radical morphism with nonzero source cannot be split monic.
theorem
MagnitudeConjecture.CategoryTheory.isRadicalMorphism_finset_sum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{ι : Type w}
{X Y : C}
(s : Finset ι)
(f : ι → (X ⟶ Y))
(hf : ∀ i ∈ s, QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (f i))
:
A finite sum of radical morphisms is radical.
theorem
MagnitudeConjecture.CategoryTheory.ShortComplex.Exact.isRightMinimal_g_of_isRadicalMorphism_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Projective S.X₂]
(hS : S.Exact)
(hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism S.f)
:
In an exact complex, a radical first differential makes the second differential right minimal when its source is projective.
theorem
MagnitudeConjecture.CategoryTheory.isRadicalMorphism_kernel_ι_of_isRightMinimal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{X Y : C}
(f : X ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightMinimal f)
:
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (CategoryTheory.Limits.kernel.ι f)
The kernel inclusion of a right-minimal morphism is radical.
theorem
MagnitudeConjecture.CategoryTheory.isRightMinimal_iff_kernel_ι_isRadicalMorphism
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{X Y : C}
[CategoryTheory.Projective X]
(f : X ⟶ Y)
:
QuotientSubmoduleEquidistribution.IsRightMinimal f ↔ QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (CategoryTheory.Limits.kernel.ι f)
A morphism from a projective object is right minimal exactly when its kernel inclusion is radical.
theorem
MagnitudeConjecture.CategoryTheory.finBiproduct_eq_sum_components
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{I J : Type w}
[Fintype I]
[Fintype J]
(X : I → C)
(Y : J → C)
(f : ⨁ X ⟶ ⨁ Y)
:
f = ∑ i : I,
∑ j : J,
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π X i)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i)
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π Y j)))
(CategoryTheory.Limits.biproduct.ι Y j))
A map between finite biproducts is the finite sum of its matrix components inserted into the corresponding source and target summands.
theorem
MagnitudeConjecture.CategoryTheory.isRadicalMorphism_finBiproduct_component
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{I J : Type w}
[Fintype I]
[Fintype J]
(X : I → C)
(Y : J → C)
(f : ⨁ X ⟶ ⨁ Y)
(hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f)
(i : I)
(j : J)
:
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i)
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π Y j)))
Every matrix component of a radical finite-biproduct map is radical.
theorem
MagnitudeConjecture.CategoryTheory.isRadicalMorphism_finBiproduct_of_components
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{I J : Type w}
[Fintype I]
[Fintype J]
(X : I → C)
(Y : J → C)
(f : ⨁ X ⟶ ⨁ Y)
(hf :
∀ (i : I) (j : J),
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i)
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π Y j))))
:
A map of finite biproducts is radical when all of its matrix components are radical.
theorem
MagnitudeConjecture.CategoryTheory.map_finBiproduct_isRadicalMorphism
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{D : Type uD}
[CategoryTheory.Category.{vD, uD} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[F.Additive]
{I J : Type}
[Fintype I]
[Fintype J]
(X : I → C)
(Y : J → C)
(f : ⨁ X ⟶ ⨁ Y)
(hf :
∀ (i : I) (j : J),
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(F.map
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i)
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π Y j)))))
:
An additive functor maps a finite-biproduct morphism to a radical morphism when it maps every matrix component to a radical morphism.