FactorThru

📁 Source: Mathlib/CategoryTheory/Subobject/FactorThru.lean

Statistics

Metric	Count
Definitions factorThru, factorThru, homOfFactors	3
Theorems factors_congr, factorThru_add, factorThru_add_sub_factorThru_left, factorThru_add_sub_factorThru_right, factorThru_arrow, factorThru_arrow_assoc, factorThru_comp_arrow, factorThru_eq_zero, factorThru_mk_self, factorThru_ofLE, factorThru_right, factorThru_self, factorThru_zero, factors_add, factors_comp_arrow, factors_iff, factors_left_of_factors_add, factors_of_factors_right, factors_of_le, factors_right_of_factors_add, factors_self, factors_zero, le_of_factors, mk_factors_iff, mk_factors_self	25
Total	28

CategoryTheory.MonoOver

Definitions

Name	Category	Theorems
factorThru 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factors_congr 📖	mathematical	—	Factors	—	CategoryTheory.Category.assoc CategoryTheory.Over.w

CategoryTheory.Subobject

Definitions

Name	Category	Theorems
factorThru 📖	CompOp	17 math math: factorThru_right, AlgebraicTopology.NormalizedMooreComplex.obj_d, factorThru_eq_zero, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, factorThru_comp_arrow, factorThru_mk_self, CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc, factorThru_arrow_assoc, factorThru_add_sub_factorThru_right, factorThru_self, factorThru_ofLE, AlgebraicTopology.NormalizedMooreComplex.map_f, factorThru_add_sub_factorThru_left, factorThru_arrow, factorThru_add, factorThru_zero, CategoryTheory.Limits.factorThruImageSubobject_comp_self
homOfFactors 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorThru_add 📖	mathematical	Factors Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	factorThru CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying	—	eq_of_comp_arrow_eq factorThru_arrow CategoryTheory.Preadditive.add_comp
factorThru_add_sub_factorThru_left 📖	mathematical	Factors Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup factorThru factors_right_of_factors_add	—	eq_of_comp_arrow_eq factors_right_of_factors_add CategoryTheory.Preadditive.sub_comp factorThru_arrow add_sub_cancel_left
factorThru_add_sub_factorThru_right 📖	mathematical	Factors Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup factorThru factors_left_of_factors_add	—	eq_of_comp_arrow_eq factors_left_of_factors_add CategoryTheory.Preadditive.sub_comp factorThru_arrow add_sub_cancel_right
factorThru_arrow 📖	mathematical	Factors	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying factorThru arrow	—	factors_iff
factorThru_arrow_assoc 📖	mathematical	Factors	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying factorThru arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThru_arrow
factorThru_comp_arrow 📖	mathematical	Factors CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	factorThru	—	eq_of_comp_arrow_eq factorThru_arrow
factorThru_eq_zero 📖	mathematical	Factors	factorThru Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.eq_whisker factorThru_arrow CategoryTheory.Limits.zero_comp eq_of_comp_arrow_eq
factorThru_mk_self 📖	mathematical	—	factorThru mk_factors_self CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying underlyingIso	—	eq_of_comp_arrow_eq mk_factors_self factorThru_arrow underlyingIso_arrow
factorThru_ofLE 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject Factors	factorThru factors_of_le CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE	—	eq_of_comp_arrow_eq factors_of_le factorThru_arrow CategoryTheory.Category.assoc ofLE_arrow
factorThru_right 📖	mathematical	Factors	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying factorThru factors_of_factors_right	—	factors_of_factors_right CategoryTheory.cancel_mono arrow_mono CategoryTheory.Category.assoc factorThru_arrow
factorThru_self 📖	mathematical	Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	factorThru CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	eq_of_comp_arrow_eq factorThru_arrow CategoryTheory.Category.id_comp
factorThru_zero 📖	mathematical	Factors Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	factorThru CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying	—	—
factors_add 📖	mathematical	Factors	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	factors_iff CategoryTheory.Preadditive.add_comp factorThru_arrow
factors_comp_arrow 📖	mathematical	—	Factors CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	—	factors_iff
factors_iff 📖	mathematical	—	Factors CategoryTheory.MonoOver.Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono representative	—	CategoryTheory.MonoOver.factors_congr
factors_left_of_factors_add 📖	—	Factors Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—	factors_iff CategoryTheory.Preadditive.sub_comp factorThru_arrow add_sub_cancel_right
factors_of_factors_right 📖	mathematical	Factors	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	Quotient.ind' CategoryTheory.Category.assoc
factors_of_le 📖	—	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject Factors	—	—	CategoryTheory.Category.assoc ofLE_arrow
factors_right_of_factors_add 📖	—	Factors Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—	factors_iff CategoryTheory.Preadditive.sub_comp factorThru_arrow add_sub_cancel_left
factors_self 📖	mathematical	—	Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	—	factors_iff CategoryTheory.Category.id_comp
factors_zero 📖	mathematical	—	Factors Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	factors_iff CategoryTheory.Limits.zero_comp
le_of_factors 📖	mathematical	Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	Preorder.toLE	—	le_of_comm factorThru_arrow
mk_factors_iff 📖	mathematical	—	Factors CategoryTheory.MonoOver.Factors	—	—
mk_factors_self 📖	mathematical	—	Factors	—	CategoryTheory.Category.id_comp

---

← Back to Index