Local comparison of ideal products with a full subcategory #
def
MagnitudeConjecture.fullSubcategoryHomAddEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(P : CategoryTheory.ObjectProperty C)
(X Y : P.FullSubcategory)
:
(X.obj ⟶ Y.obj) ≃+ (X ⟶ Y)
Bundle an ambient map between two objects of a full subcategory.
Instances For
theorem
MagnitudeConjecture.homIdealProduct_fullSubcategory_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
(P : CategoryTheory.ObjectProperty C)
(hdec : ∀ (M : C), Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M))
(I J : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal C)
(X Y : P.FullSubcategory)
(hY : ∀ (Z : C), CategoryTheory.Indecomposable Z → ∀ (b : Z ⟶ Y.obj), b ≠ 0 → P Z)
(f : X ⟶ Y)
:
f.hom ∈ (I ⋆ᵢ J).hom X.obj Y.obj ↔ f ∈ (QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap P.ι I ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap P.ι J).hom
X Y
At a target whose nonzero incoming indecomposables lie in the full subcategory, multiplication of categorical ideals commutes with restriction.