Categories #
Defines a category, as a type class parametrised by the type of objects.
Notations #
Introduces notations in the CategoryTheory scope
X ⟶ Yfor the morphism spaces (type as\hom),𝟙 Xfor the identity morphism onX(type as\b1),f ≫ gfor composition in the 'arrows' convention (type as\gg).
Users may like to add g ⊚ f for composition in the standard convention, using
local notation g ` ⊚ `:80 f:80 := category.comp f g -- type as \oo
Porting note #
I am experimenting with using the aesop tactic as a replacement for tidy.
A wrapper for ext that we can pass to aesop.
Equations
- One or more equations did not get rendered due to their size.
A preliminary structure on the way to defining a category, containing the data, but none of the axioms.
Notation for the identity morphism in a category.
Equations
- CategoryTheory.«term𝟙» = Lean.ParserDescr.node `CategoryTheory.term𝟙 1024 (Lean.ParserDescr.symbol "𝟙")
Notation for composition of morphisms in a category.
Equations
- One or more equations did not get rendered due to their size.
A thin wrapper for aesop which adds the CategoryTheory rule set and
allows aesop to look through semireducible definitions when calling intros.
It also turns on zetaDelta in the simp config, allowing aesop_cat to unfold any lets.
This tactic fails when it is unable to solve the goal, making it suitable for
use in auto-params.
Equations
- One or more equations did not get rendered due to their size.
We also use aesop_cat? to pass along a Try this suggestion when using aesop_cat
Equations
- One or more equations did not get rendered due to their size.
A variant of aesop_cat which does not fail when it is unable to solve the
goal. Use this only for exploration! Nonterminal aesop is even worse than
nonterminal simp.
Equations
- One or more equations did not get rendered due to their size.
class
CategoryTheory.Category
(obj : Type u)
extends
CategoryTheory.CategoryStruct
:
Type (max u (v + 1))
The typeclass Category C describes morphisms associated to objects of type C.
The universe levels of the objects and morphisms are unconstrained, and will often need to be
specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.)
See
- Hom : obj → obj → Type v
- id : (X : obj) → X ⟶ X
- id_comp : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
Identity morphisms are left identities for composition.
- comp_id : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
Identity morphisms are right identities for composition.
- assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
Composition in a category is associative.
Instances
- CategoryTheory.BundledHom.category
- CategoryTheory.Cat.category
- CategoryTheory.Cat.instCategoryObjCatToQuiverToCategoryStructCategoryTypeToQuiverToCategoryStructTypesToPrefunctorObjects
- CategoryTheory.Cat.str
- CategoryTheory.Category.opposite
- CategoryTheory.FinCategory.categoryAsType
- CategoryTheory.FullSubcategory.category
- CategoryTheory.Functor.category
- CategoryTheory.Functor.instCategoryEssImageSubcategory
- CategoryTheory.InducedCategory.category
- CategoryTheory.Limits.Bicone.category
- CategoryTheory.Limits.BinaryBicone.category
- CategoryTheory.Limits.Cocone.category
- CategoryTheory.Limits.Cone.category
- CategoryTheory.Limits.WalkingMulticospan.instSmallCategoryWalkingMulticospan
- CategoryTheory.Limits.WalkingMultispan.instSmallCategoryWalkingMultispan
- CategoryTheory.Limits.WidePullbackShape.category
- CategoryTheory.Limits.WidePushoutShape.category
- CategoryTheory.Limits.walkingParallelPairHomCategory
- CategoryTheory.Pi.instForAllCategoryCompType
- CategoryTheory.Pi.sumElimCategory
- CategoryTheory.ShortComplex.SnakeInput.instCategorySnakeInput
- CategoryTheory.ShortComplex.instCategoryShortComplex
- CategoryTheory.Shrink.instCategoryShrink
- CategoryTheory.ShrinkHoms.instCategoryShrinkHoms
- CategoryTheory.StrictBicategory.category
- CategoryTheory.ULiftHom.category
- CategoryTheory.commaCategory
- CategoryTheory.discreteCategory
- CategoryTheory.instCategoryAdditiveFunctor
- CategoryTheory.instCategoryArrow
- CategoryTheory.instCategoryCostructuredArrow
- CategoryTheory.instCategoryExactFunctor
- CategoryTheory.instCategoryLeftExactFunctor
- CategoryTheory.instCategoryMonoOver
- CategoryTheory.instCategoryOver
- CategoryTheory.instCategoryRightExactFunctor
- CategoryTheory.instCategorySkeleton
- CategoryTheory.instCategoryStructuredArrow
- CategoryTheory.instCategoryUnder
- CategoryTheory.instSmallCategoryAsSmall
- CategoryTheory.pi
- CategoryTheory.pi'
- CategoryTheory.prod
- CategoryTheory.prodCategoryInstance1
- CategoryTheory.prodCategoryInstance2
- CategoryTheory.smallCategorySmallModel
- CategoryTheory.types
- CategoryTheory.uliftCategory
- CategoryTheory.uniformProd
- ModuleCat.moduleCategory
- Preorder.smallCategory
- instAddCommGroupCatLargeCategory
- instAddCommMonCatLargeCategory
- instAddGroupCatLargeCategory
- instAddMonCatLargeCategory
@[inline, reducible]
A LargeCategory has objects in one universe level higher than the universe level of
the morphisms. It is useful for examples such as the category of types, or the category
of groups, etc.
theorem
CategoryTheory.eq_whisker
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(w : f = g)
(h : Y ⟶ Z)
:
postcompose an equation between morphisms by another morphism
theorem
CategoryTheory.whisker_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
{g : Y ⟶ Z}
{h : Y ⟶ Z}
(w : g = h)
:
precompose an equation between morphisms by another morphism
Notation for whiskering an equation by a morphism (on the right).
If f g : X ⟶ Y and w : f = g and h : Y ⟶ Z, then w =≫ h : f ≫ h = g ≫ h.
Equations
- One or more equations did not get rendered due to their size.
Notation for whiskering an equation by a morphism (on the left).
If g h : Y ⟶ Z and w : g = h and h : X ⟶ Y, then f ≫= w : f ≫ g = f ≫ h.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.eq_of_comp_left_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(w : ∀ {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h)
:
f = g
theorem
CategoryTheory.eq_of_comp_right_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{Y : C}
{Z : C}
{f : Y ⟶ Z}
{g : Y ⟶ Z}
(w : ∀ {X : C} (h : X ⟶ Y), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g)
:
f = g
theorem
CategoryTheory.eq_of_comp_left_eq'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
(w : (fun {Z : C} (h : Y ⟶ Z) => CategoryTheory.CategoryStruct.comp f h) = fun {Z : C} (h : Y ⟶ Z) =>
CategoryTheory.CategoryStruct.comp g h)
:
f = g
theorem
CategoryTheory.eq_of_comp_right_eq'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{Y : C}
{Z : C}
(f : Y ⟶ Z)
(g : Y ⟶ Z)
(w : (fun {X : C} (h : X ⟶ Y) => CategoryTheory.CategoryStruct.comp h f) = fun {X : C} (h : X ⟶ Y) =>
CategoryTheory.CategoryStruct.comp h g)
:
f = g
theorem
CategoryTheory.id_of_comp_left_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
(f : X ⟶ X)
(w : ∀ {Y : C} (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp f g = g)
:
theorem
CategoryTheory.id_of_comp_right_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
(f : X ⟶ X)
(w : ∀ {Y : C} (g : Y ⟶ X), CategoryTheory.CategoryStruct.comp g f = g)
:
theorem
CategoryTheory.comp_ite
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{P : Prop}
[Decidable P]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(g' : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp f (if P then g else g') = if P then CategoryTheory.CategoryStruct.comp f g else CategoryTheory.CategoryStruct.comp f g'
theorem
CategoryTheory.ite_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{P : Prop}
[Decidable P]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(f' : X ⟶ Y)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (if P then f else f') g = if P then CategoryTheory.CategoryStruct.comp f g else CategoryTheory.CategoryStruct.comp f' g
theorem
CategoryTheory.comp_dite
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{P : Prop}
[Decidable P]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : P → (Y ⟶ Z))
(g' : ¬P → (Y ⟶ Z))
:
CategoryTheory.CategoryStruct.comp f (if h : P then g h else g' h) = if h : P then CategoryTheory.CategoryStruct.comp f (g h) else CategoryTheory.CategoryStruct.comp f (g' h)
theorem
CategoryTheory.dite_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{P : Prop}
[Decidable P]
{X : C}
{Y : C}
{Z : C}
(f : P → (X ⟶ Y))
(f' : ¬P → (X ⟶ Y))
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (if h : P then f h else f' h) g = if h : P then CategoryTheory.CategoryStruct.comp (f h) g else CategoryTheory.CategoryStruct.comp (f' h) g
class
CategoryTheory.Epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A morphism f is an epimorphism if it can be cancelled when precomposed:
f ≫ g = f ≫ h implies g = h.
See
- left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h → g = h
A morphism
fis an epimorphism if it can be cancelled when precomposed.
Instances
- CategoryTheory.Abelian.epi_factorThruCoimage
- CategoryTheory.Abelian.epi_pullback_of_epi_f
- CategoryTheory.Abelian.epi_pullback_of_epi_g
- CategoryTheory.Abelian.instEpiImageToHasZeroMorphismsNonPreadditiveAbelianHas_kernelsHas_cokernelsFactorThruImage
- CategoryTheory.Arrow.epi_right
- CategoryTheory.CostructuredArrow.epi_homMk
- CategoryTheory.CostructuredArrow.epi_left_of_epi
- CategoryTheory.Exact.epi_factorThruKernelSubobject
- CategoryTheory.Functor.map_epi
- CategoryTheory.IsIso.epi_of_iso
- CategoryTheory.IsSplitEpi.epi
- CategoryTheory.Limits.HasZeroObject.instEpiOfNatToOfNat0Zero'
- CategoryTheory.Limits.Multicoequalizer.instEpiSigmaObjRRightMulticoequalizerSigmaπ
- CategoryTheory.Limits.Sigma.map_epi
- CategoryTheory.Limits.biprod.epi_desc_of_epi_left
- CategoryTheory.Limits.biprod.epi_desc_of_epi_right
- CategoryTheory.Limits.coequalizer.π_epi
- CategoryTheory.Limits.cokernel.desc_epi
- CategoryTheory.Limits.colimMap_epi
- CategoryTheory.Limits.colimMap_epi'
- CategoryTheory.Limits.colimitQuotientCoproduct_epi
- CategoryTheory.Limits.coprod.epi_desc_of_epi_left
- CategoryTheory.Limits.coprod.epi_desc_of_epi_right
- CategoryTheory.Limits.coprod.map_epi
- CategoryTheory.Limits.epi_coprod_to_pushout
- CategoryTheory.Limits.image.preComp_epi_of_epi
- CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi
- CategoryTheory.Limits.instEpiImageFactorThruImage
- CategoryTheory.Limits.instEpiObjSubobjectToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderSubobjectToQuiverToCategoryStructToPrefunctorUnderlyingImageSubobjectFactorThruImageSubobject
- CategoryTheory.Limits.map_π_epi
- CategoryTheory.Limits.pushout.inl_of_epi
- CategoryTheory.Limits.pushout.inr_of_epi
- CategoryTheory.Linear.instEpiHSMulHomToQuiverToCategoryStructInstHSMulToSMulZeroPreadditiveHasZeroMorphismsToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroToAddCommMonoidHomGroupHomModule
- CategoryTheory.NonPreadditiveAbelian.epi_r
- CategoryTheory.NonPreadditiveAbelian.instEpiImageToHasZeroMorphismsHas_kernelsHas_cokernelsFactorThruImage
- CategoryTheory.Preadditive.instEpiNegHomToQuiverToCategoryStructToNegToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidHomGroup
- CategoryTheory.Projective.π_epi
- CategoryTheory.RegularEpi.epi
- CategoryTheory.ShortComplex.LeftHomologyData.instEpiKHπ
- CategoryTheory.ShortComplex.RightHomologyData.instEpiX₂QP
- CategoryTheory.ShortComplex.SnakeInput.epi_L₃_g
- CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₁
- CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₂
- CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₃
- CategoryTheory.ShortComplex.SnakeInput.instEpiX₂PreadditiveHasZeroMorphismsToPreadditiveL₀'X₃G
- CategoryTheory.ShortComplex.epi_homologyMap_of_epi_cyclesMap
- CategoryTheory.ShortComplex.instEpiCokernelPreadditiveHasZeroMorphismsToPreadditiveX₁X₂FHas_colimitHasCokernels_of_hasCoequalizersHasCoequalizersCoimageHasKernels_of_hasEqualizersHasEqualizersX₃GCokernelToAbelianCoimage
- CategoryTheory.ShortComplex.instEpiCyclesHasLeftHomology_of_hasHomologyHomologyHomologyπ
- CategoryTheory.ShortComplex.instEpiCyclesLeftHomologyLeftHomologyπ
- CategoryTheory.ShortComplex.instEpiModuleCatModuleCategoryOfSubtypeCarrierX₂PreadditiveHasZeroMorphismsInstPreadditiveModuleCatModuleCategoryMemSubmoduleToSemiringToAddCommMonoidIsAddCommGroupIsModuleInstMembershipSetLikeKerX₃IdToNonAssocSemiringHomToQuiverToCategoryStructInstFunLikeHomModuleCatToQuiverToCategoryStructModuleCategoryCarrierInstLinearMapClassHomModuleCatToQuiverToCategoryStructModuleCategoryCarrierToSemiringToAddCommMonoidIsAddCommGroupIsModuleInstFunLikeHomModuleCatToQuiverToCategoryStructModuleCategoryCarrierGAddCommGroupModuleModuleCatHomologyModuleCatHomologyπ
- CategoryTheory.ShortComplex.instEpiX₂OpcyclesPOpcycles
- CategoryTheory.StructuredArrow.epi_homMk
- CategoryTheory.Under.epi_right_of_epi
- CategoryTheory.epi_of_strongEpi
- CategoryTheory.instEpiIdToCategoryStruct
- CategoryTheory.op_epi_of_mono
- CategoryTheory.unop_epi_of_mono
- ModuleCat.epi_as_hom''_mkQ
- imageToKernel_epi_of_epi_of_zero
- imageToKernel_epi_of_zero_of_mono
class
CategoryTheory.Mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A morphism f is a monomorphism if it can be cancelled when postcomposed:
g ≫ f = h ≫ f implies g = h.
See
- right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f → g = h
A morphism
fis a monomorphism if it can be cancelled when postcomposed.
Instances
- CategoryTheory.Abelian.instMonoCoimageToHasZeroMorphismsNonPreadditiveAbelianHas_kernelsHas_cokernelsFactorThruCoimage
- CategoryTheory.Abelian.mono_factorThruImage
- CategoryTheory.Abelian.mono_pushout_of_mono_f
- CategoryTheory.Abelian.mono_pushout_of_mono_g
- CategoryTheory.Adjunction.instMonoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCoeEquivHomObjToPrefunctorHomInstFunLikeEquivHomEquiv
- CategoryTheory.Arrow.mono_left
- CategoryTheory.CostructuredArrow.mono_homMk
- CategoryTheory.Functor.map_mono
- CategoryTheory.Injective.ι_mono
- CategoryTheory.IsIso.mono_of_iso
- CategoryTheory.IsSplitMono.mono
- CategoryTheory.Limits.HasZeroObject.instMonoOfNat
- CategoryTheory.Limits.Multiequalizer.instMonoMultiequalizerPiObjLLeftιPi
- CategoryTheory.Limits.Pi.map_mono
- CategoryTheory.Limits.Types.instMonoTypeTypesImageι
- CategoryTheory.Limits.biprod.mono_lift_of_mono_left
- CategoryTheory.Limits.biprod.mono_lift_of_mono_right
- CategoryTheory.Limits.equalizer.ι_mono
- CategoryTheory.Limits.image.lift_mono
- CategoryTheory.Limits.image.preComp_mono
- CategoryTheory.Limits.initial.mono_from
- CategoryTheory.Limits.instMonoImageι
- CategoryTheory.Limits.kernel.lift_mono
- CategoryTheory.Limits.limMap_mono
- CategoryTheory.Limits.limMap_mono'
- CategoryTheory.Limits.limitSubobjectProduct_mono
- CategoryTheory.Limits.mono_pullback_to_prod
- CategoryTheory.Limits.prod.map_mono
- CategoryTheory.Limits.prod.mono_lift_of_mono_left
- CategoryTheory.Limits.prod.mono_lift_of_mono_right
- CategoryTheory.Limits.pullback.fst_of_mono
- CategoryTheory.Limits.pullback.snd_of_mono
- CategoryTheory.Linear.instMonoHSMulHomToQuiverToCategoryStructInstHSMulToSMulZeroPreadditiveHasZeroMorphismsToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroToAddCommMonoidHomGroupHomModule
- CategoryTheory.MonoOver.mono
- CategoryTheory.NonPreadditiveAbelian.instMonoCoimageToHasZeroMorphismsHas_kernelsHas_cokernelsFactorThruCoimage
- CategoryTheory.NonPreadditiveAbelian.mono_r
- CategoryTheory.NonPreadditiveAbelian.mono_Δ
- CategoryTheory.Over.mono_left_of_mono
- CategoryTheory.Preadditive.instMonoNegHomToQuiverToCategoryStructToNegToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidHomGroup
- CategoryTheory.RegularMono.mono
- CategoryTheory.ShortComplex.LeftHomologyData.instMonoKX₂I
- CategoryTheory.ShortComplex.RightHomologyData.instMonoHQι
- CategoryTheory.ShortComplex.SnakeInput.instMonoX₁PreadditiveHasZeroMorphismsToPreadditiveL₀'X₂F
- CategoryTheory.ShortComplex.SnakeInput.mono_L₀_f
- CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₁
- CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₂
- CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₃
- CategoryTheory.ShortComplex.instMonoCyclesX₂ICycles
- CategoryTheory.ShortComplex.instMonoHomologyOpcyclesHasRightHomology_of_hasHomologyHomologyι
- CategoryTheory.ShortComplex.instMonoImagePreadditiveHasZeroMorphismsToPreadditiveHasKernels_of_hasEqualizersHasEqualizersHasCokernels_of_hasCoequalizersHasCoequalizersX₁X₂FKernelX₃GHas_limitAbelianImageToKernel
- CategoryTheory.ShortComplex.instMonoRightHomologyOpcyclesRightHomologyι
- CategoryTheory.ShortComplex.mono_homologyMap_of_mono_opcyclesMap
- CategoryTheory.StructuredArrow.mono_homMk
- CategoryTheory.StructuredArrow.mono_right_of_mono
- CategoryTheory.Subobject.arrow_mono
- CategoryTheory.Subobject.instMonoObjSubobjectToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderSubobjectToQuiverToCategoryStructToPrefunctorUnderlyingOfLE
- CategoryTheory.Subobject.instMonoObjSubobjectToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderSubobjectToQuiverToCategoryStructToPrefunctorUnderlyingOfLEMk
- CategoryTheory.Subobject.instMonoObjSubobjectToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderSubobjectToQuiverToCategoryStructToPrefunctorUnderlyingOfMkLE
- CategoryTheory.Subobject.instMonoOfMkLEMk
- CategoryTheory.Subobject.widePullbackι_mono
- CategoryTheory.instMonoIdToCategoryStruct
- CategoryTheory.mono_of_strongMono
- CategoryTheory.op_mono_of_epi
- CategoryTheory.unop_mono_of_epi
- ModuleCat.mono_as_hom'_subtype
- instMonoObjSubobjectToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderSubobjectToQuiverToCategoryStructToPrefunctorUnderlyingImageSubobjectKernelSubobjectImageToKernel
instance
CategoryTheory.instEpiIdToCategoryStruct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : C)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.instMonoIdToCategoryStruct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : C)
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.cancel_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
{g : Y ⟶ Z}
{h : Y ⟶ Z}
:
theorem
CategoryTheory.cancel_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
{g : Z ⟶ X}
{h : Z ⟶ X}
:
theorem
CategoryTheory.cancel_epi_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
{h : Y ⟶ Y}
:
theorem
CategoryTheory.cancel_mono_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
{g : X ⟶ X}
:
theorem
CategoryTheory.epi_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
(g : Y ⟶ Z)
[CategoryTheory.Epi g]
:
theorem
CategoryTheory.mono_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
(g : Y ⟶ Z)
[CategoryTheory.Mono g]
:
theorem
CategoryTheory.mono_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp f g)]
:
theorem
CategoryTheory.mono_of_mono_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
{h : X ⟶ Z}
[CategoryTheory.Mono h]
(w : CategoryTheory.CategoryStruct.comp f g = h)
:
theorem
CategoryTheory.epi_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)]
:
theorem
CategoryTheory.epi_of_epi_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
{h : X ⟶ Z}
[CategoryTheory.Epi h]
(w : CategoryTheory.CategoryStruct.comp f g = h)
: