Categories #
Defines a category, as a type class parametrised by the type of objects.
Notations #
Introduces notations
X ⟶ Y
for the morphism spaces,f ≫ g
for composition in the 'arrows' convention.
Users may like to add f ⊚ g
for composition in the standard convention, using
local notation f ` ⊚ `:80 g:80 := category.comp g f -- type as \oo
A preliminary structure on the way to defining a category, containing the data, but none of the axioms.
Instances
- category_theory.category.to_category_struct
- category_theory.limits.wide_pullback_shape.struct
- category_theory.limits.wide_pushout_shape.struct
- category_theory.monad.algebra.category_theory.category_struct
- category_theory.comonad.coalgebra.category_theory.category_struct
- category_theory.single_obj.category_struct
- category_theory.Kleisli.category_struct
- category_theory.sigma.sigma_hom.sigma.category_theory.category_struct
- to_category_struct : category_theory.category_struct obj
- id_comp' : (∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f) . "obviously"
- comp_id' : (∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f) . "obviously"
- assoc' : (∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h) . "obviously"
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 large_category
and small_category
.)
See https://stacks.math.columbia.edu/tag/0014.
Instances
- preorder.small_category
- category_theory.groupoid.to_category
- category_theory.ulift_category
- category_theory.functor.category
- category_theory.types
- category_theory.induced_category.category
- category_theory.full_subcategory
- category_theory.functor.ess_image.category_theory.category
- category_theory.category.opposite
- category_theory.bundled_hom.category
- Mon.large_category
- AddMon.large_category
- CommMon.large_category
- AddCommMon.large_category
- Group.large_category
- AddGroup.large_category
- CommGroup.large_category
- AddCommGroup.large_category
- SemiRing.large_category
- Ring.large_category
- CommSemiRing.large_category
- CommRing.large_category
- category_theory.discrete_category
- category_theory.prod
- category_theory.uniform_prod
- category_theory.prod_category_instance_1
- category_theory.prod_category_instance_2
- category_theory.limits.cone.category
- category_theory.limits.cocone.category
- category_theory.comma_category
- category_theory.structured_arrow.category
- category_theory.costructured_arrow.category
- category_theory.over.category
- category_theory.under.category
- category_theory.limits.walking_parallel_pair_hom_category
- category_theory.limits.wide_pullback_shape.category
- category_theory.limits.wide_pushout_shape.category
- category_theory.arrow.category
- category_theory.Cat.str
- category_theory.Cat.category
- Module.Module_category
- Algebra.category_theory.category
- category_theory.monoidal_nat_trans.category_lax_monoidal_functor
- category_theory.monoidal_nat_trans.category_monoidal_functor
- category_theory.lax_braided_functor.category_lax_braided_functor
- category_theory.braided_functor.category_braided_functor
- category_theory.monoidal_of_chosen_finite_products.monoidal_of_chosen_finite_products_synonym.category
- category_theory.monad.category
- category_theory.comonad.category
- category_theory.monad.algebra.EilenbergMoore
- category_theory.comonad.coalgebra.EilenbergMoore
- category_theory.mono_over.category
- category_theory.skeleton.category
- category_theory.subobject.category
- category_theory.small_category_small_model
- category_theory.shrink_homs.category_theory.category
- Magma.large_category
- AddMagma.large_category
- Semigroup.large_category
- AddSemigroup.large_category
- category_theory.pi
- category_theory.pi'
- category_theory.pi.sum_elim_category
- category_theory.graded_object.category_of_graded_objects
- category_theory.differential_object.category_of_differential_objects
- Top.large_category
- Top.presheaf.category
- algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces
- Top.sheaf.category_theory.category
- algebraic_geometry.SheafedSpace.category_theory.category
- topological_space.open_nhds.open_nhds_category
- algebraic_geometry.LocallyRingedSpace.category_theory.category
- TopCommRing.category_theory.category
- algebraic_geometry.Scheme.category_theory.category
- Preorder.large_category
- PartialOrder.large_category
- LinearOrder.large_category
- NonemptyFinLinOrd.large_category
- simplex_category.small_category
- simplex_category.truncated.small_category
- category_theory.simplicial_object.category
- category_theory.simplicial_object.truncated.category
- sSet.large_category
- sSet.truncated.large_category
- category_theory.category_of_elements
- category_theory.single_obj.category
- category_theory.action_category.category
- category_theory.Groupoid.category
- category_theory.Kleisli.category
- category_theory.pairwise.category_theory.category
- category_theory.paths.category_paths
- category_theory.Quiv.category
- category_theory.rel
- category_theory.sigma.sigma
- category_theory.component.category
- category_theory.center.category_theory.category
- category_theory.category_forget_enrichment
- Fintype.category_theory.category
- Fintype.skeleton.category_theory.category
- category_theory.grothendieck.category_theory.category
- category_theory.kleisli.kleisli.category
- Mon_.category_theory.category
- CommMon_.category_theory.category
- category_theory.free_monoidal_category.category_free_monoidal_category
- Mod.category_theory.category
- category_theory.monoidal.transported.category
- category_theory.Mat_.category_theory.category
- category_theory.quotient.category
- category_theory.SheafOfTypes.category
- category_theory.Sheaf.category
- category_theory.subterminals.category
- category_theory.sum
- category_theory.triangulated.triangle_category
- category_theory.with_terminal.category_theory.category
- category_theory.with_initial.category_theory.category
- Meas.large_category
- ωCPO.large_category
- CompHaus.category
- Compactum.category
- Profinite.category
- UniformSpace.large_category
- CpltSepUniformSpace.category
- Top.presheaf.sheaf_condition.opens_le_cover.category_theory.category
A large_category
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.
A small_category
has objects and morphisms in the same universe level.
postcompose an equation between morphisms by another morphism
precompose an equation between morphisms by another morphism
A morphism f
is an epimorphism if it can be "cancelled" when precomposed:
f ≫ g = f ≫ h
implies g = h
.
See https://stacks.math.columbia.edu/tag/003B.
Instances
- category_theory.is_iso.epi_of_iso
- category_theory.split_epi.epi
- category_theory.epi_of_strong_epi
- category_theory.regular_epi.epi
- category_theory.category_struct.id.epi
- category_theory.is_equivalence.epi_map
- category_theory.unop_epi_of_mono
- category_theory.op_epi_of_mono
- category_theory.limits.initial.epi_to
- category_theory.limits.coprod.epi_desc_of_epi_left
- category_theory.limits.coprod.epi_desc_of_epi_right
- category_theory.limits.coequalizer.π_epi
- category_theory.limits.pushout.inl_of_epi
- category_theory.limits.pushout.inr_of_epi
- category_theory.limits.factor_thru_image.category_theory.epi
- category_theory.limits.image.pre_comp_epi_of_epi
- category_theory.limits.has_zero_object.category_theory.epi
- category_theory.limits.cokernel.desc_epi
- category_theory.preadditive.has_neg.neg.category_theory.epi
- category_theory.linear.has_scalar.smul.category_theory.epi
- Module.epi_as_hom''_mkq
- category_theory.limits.biprod.epi_desc_of_epi_left
- category_theory.limits.biprod.epi_desc_of_epi_right
- category_theory.non_preadditive_abelian.factor_thru_image.category_theory.epi
- category_theory.non_preadditive_abelian.epi_factor_thru_coimage
- category_theory.non_preadditive_abelian.epi_r
- category_theory.abelian.images.factor_thru_image.category_theory.epi
- category_theory.abelian.coimages.epi_factor_thru_coimage
- category_theory.abelian.epi_pullback_of_epi_f
- category_theory.abelian.epi_pullback_of_epi_g
- category_theory.exact.epi
- category_theory.projective.π.category_theory.epi
- category_theory.limits.factor_thru_image_subobject.category_theory.epi
- category_theory.limits.image_subobject_comp_le_epi_of_epi
A morphism f
is a monomorphism if it can be "cancelled" when postcomposed:
g ≫ f = h ≫ f
implies g = h
.
See https://stacks.math.columbia.edu/tag/003B.
Instances
- category_theory.is_iso.mono_of_iso
- category_theory.split_mono.mono
- category_theory.regular_mono.mono
- category_theory.category_struct.id.mono
- category_theory.is_equivalence.mono_map
- category_theory.unop_mono_of_epi
- category_theory.op_mono_of_epi
- category_theory.limits.terminal.mono_from
- category_theory.over.mono_left_of_mono
- category_theory.limits.prod.mono_lift_of_mono_left
- category_theory.limits.prod.mono_lift_of_mono_right
- category_theory.limits.equalizer.ι_mono
- category_theory.limits.pullback.fst_of_mono
- category_theory.limits.pullback.snd_of_mono
- category_theory.limits.mono_factorisation.m_mono
- category_theory.limits.image.ι.category_theory.mono
- category_theory.limits.lift_mono
- category_theory.limits.image.pre_comp_mono
- category_theory.limits.has_zero_object.category_theory.mono
- category_theory.limits.kernel.lift_mono
- category_theory.preadditive.has_neg.neg.category_theory.mono
- category_theory.linear.has_scalar.smul.category_theory.mono
- category_theory.limits.types.image.ι.category_theory.mono
- Module.mono_as_hom'_subtype
- category_theory.limits.biprod.mono_lift_of_mono_left
- category_theory.limits.biprod.mono_lift_of_mono_right
- category_theory.non_preadditive_abelian.mono_factor_thru_image
- category_theory.non_preadditive_abelian.factor_thru_coimage.category_theory.mono
- category_theory.non_preadditive_abelian.mono_Δ
- category_theory.non_preadditive_abelian.mono_r
- category_theory.abelian.images.mono_factor_thru_image
- category_theory.abelian.coimages.factor_thru_coimage.category_theory.mono
- category_theory.abelian.mono_pushout_of_mono_f
- category_theory.abelian.mono_pushout_of_mono_g
- AddCommGroup.image.ι.category_theory.mono
- category_theory.mono_over.mono
- category_theory.mono_comp
- category_theory.subobject.arrow_mono
- category_theory.subobject.of_le.category_theory.mono
- category_theory.subobject.of_le_mk.mono
- category_theory.subobject.of_mk_le.mono
- category_theory.subobject.of_mk_le_mk.mono
- category_theory.initial.mono_to
- category_theory.preserves_mono
- category_theory.sieve.functor_inclusion_is_mono
- category_theory.subobject.wide_pullback_ι_mono
We now put a category instance on any preorder.
Because we do not allow the morphisms of a category to live in Prop
,
unfortunately we need to use plift
and ulift
when defining the morphisms.
As convenience functions, we provide hom_of_le
and le_of_hom
to wrap and unwrap inequalities.
The category structure coming from a preorder. There is a morphism X ⟶ Y
if and only if X ≤ Y
.
Because we don't allow morphisms to live in Prop
,
we have to define X ⟶ Y
as ulift (plift (X ≤ Y))
.
See category_theory.hom_of_le
and category_theory.le_of_hom
.
Express an inequality as a morphism in the corresponding preorder category.
Equations
- category_theory.hom_of_le h = {down := {down := h}}
Extract the underlying inequality from a morphism in a preorder category.