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 of this typeclass
- category_theory.category.to_category_struct
- category_theory.bicategory.to_category_struct
- category_theory.limits.wide_pullback_shape.struct
- category_theory.limits.wide_pushout_shape.struct
- category_theory.locally_discrete.category_theory.category_struct
- category_theory.bicone_category_struct
- category_theory.single_obj.category_struct
- category_theory.monad.algebra.category_theory.category_struct
- category_theory.comonad.coalgebra.category_theory.category_struct
- category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct
- category_theory.Kleisli.category_struct
- category_theory.sigma.sigma_hom.sigma.category_theory.category_struct
- category_theory.endofunctor.algebra.category_theory.category_struct
Instances of other typeclasses for category_theory.category_struct
- category_theory.category_struct.has_sizeof_inst
- 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 of this typeclass
- category_theory.groupoid.to_category
- preorder.small_category
- category_theory.strict_bicategory.category
- category_theory.locally_discrete.hom_small_category
- category_theory.ulift_category
- category_theory.functor.category
- category_theory.induced_category.category
- category_theory.full_subcategory
- category_theory.functor.ess_image.category_theory.category
- category_theory.category.opposite
- category_theory.prod
- category_theory.uniform_prod
- category_theory.pi
- category_theory.pi'
- category_theory.pi.sum_elim_category
- category_theory.types
- 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_instance_1
- category_theory.prod_category_instance_2
- category_theory.limits.cone.category
- category_theory.limits.cocone.category
- category_theory.ulift_hom.category
- category_theory.as_small.small_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.comma_category
- category_theory.structured_arrow.category
- category_theory.costructured_arrow.category
- category_theory.over.category
- category_theory.under.category
- category_theory.arrow.category
- category_theory.bicategory.hom_category
- category_theory.Cat.str
- category_theory.Cat.category
- Module.Module_category
- Algebra.category_theory.category
- category_theory.fin_category.category_as_type
- category_theory.limits.walking_multicospan.category_theory.small_category
- category_theory.limits.walking_multispan.category_theory.small_category
- Pointed.large_category
- Bipointed.large_category
- Preorder.large_category
- PartialOrder.large_category
- BoundedOrder.large_category
- Lattice.category_theory.large_category
- SemilatticeSup.category_theory.large_category
- SemilatticeInf.category_theory.large_category
- BoundedLattice.category_theory.large_category
- DistribLattice.large_category
- BoundedDistribLattice.category_theory.large_category
- BoolAlg.category_theory.large_category
- BoolRing.large_category
- category_theory.free_monoidal_category.category_free_monoidal_category
- category_theory.quotient.category
- category_theory.paths.category_paths
- category_theory.free_bicategory.hom_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.AdditiveFunctor.category
- FinVect.large_category
- 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
- GroupWithZero.category_theory.large_category
- category_theory.monoidal_of_chosen_finite_products.monoidal_of_chosen_finite_products_synonym.category
- category_theory.category_Free
- Magma.large_category
- AddMagma.large_category
- Semigroup.large_category
- AddSemigroup.large_category
- category_theory.graded_object.category_of_graded_objects
- homological_complex.category_theory.category
- category_theory.differential_object.category_of_differential_objects
- homotopy_category.category
- Top.large_category
- Top.presheaf.category
- algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces
- Top.sheaf.category
- category_theory.SheafOfTypes.category_theory.category
- category_theory.Sheaf.category_theory.category
- category_theory.category_of_elements
- category_theory.bicone_category
- category_theory.bicone_small_category
- category_theory.pairwise.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
- 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
- category_theory.simplicial_object.augmented.category
- category_theory.cosimplicial_object.category
- category_theory.cosimplicial_object.truncated.category
- category_theory.cosimplicial_object.augmented.category
- category_theory.single_obj.category
- category_theory.Groupoid.category
- sSet.large_category
- sSet.truncated.large_category
- SemiNormedGroup.large_category
- SemiNormedGroup₁.category_theory.large_category
- Fintype.category_theory.category
- Fintype.skeleton.category_theory.small_category
- category_theory.action_category.category
- category_theory.limits.walking_parallel_family.category
- category_theory.monad.category
- category_theory.comonad.category
- category_theory.monad.algebra.EilenbergMoore
- category_theory.comonad.coalgebra.EilenbergMoore
- category_theory.End_monoidal.category
- category_theory.oplax_nat_trans.category
- category_theory.Cat.has_limits.category_objects
- category_theory.Cat.has_limits.category_theory.limits.limit.category_theory.category
- category_theory.Kleisli.category
- PartialFun.large_category
- category_theory.Quiv.category
- category_theory.rel
- Twop.large_category
- category_theory.subterminals.category
- category_theory.sigma.sigma
- category_theory.component.category
- category_theory.endofunctor.algebra.category_theory.category
- category_theory.center.category_theory.category
- category_theory.category_forget_enrichment
- category_theory.grothendieck.category_theory.category
- category_theory.idempotents.karoubi.category_theory.category
- category_theory.kleisli.kleisli.category
- Mon_.category_theory.category
- CommMon_.category_theory.category
- Mod.category_theory.category
- category_theory.monoidal_opposite.monoidal_opposite_category
- category_theory.monoidal.transported.category
- category_theory.Mat_.category_theory.category
- category_theory.Mat.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
- CompleteLattice.category_theory.large_category
- FinPartialOrder.large_category
- FinBoolAlg.large_category
- CompHaus.category
- Frame.large_category
- ωCPO.large_category
- Action.category_theory.category
- Rep.large_category
- fdRep.large_category
- Born.category_theory.large_category
- Profinite.category
- Compactum.category
- Locale.large_category
- UniformSpace.large_category
- CpltSepUniformSpace.category
- Top.presheaf.sheaf_condition.opens_le_cover.category_theory.category
Instances of other typeclasses for category_theory.category
- category_theory.category.has_sizeof_inst
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 of this typeclass
- 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.unop_epi_of_mono
- category_theory.op_epi_of_mono
- category_theory.is_equivalence.epi_map
- category_theory.limits.coequalizer.π_epi
- category_theory.limits.coprod.epi_desc_of_epi_left
- category_theory.limits.coprod.epi_desc_of_epi_right
- category_theory.limits.coprod.map_epi
- category_theory.limits.pushout.inl_of_epi
- category_theory.limits.pushout.inr_of_epi
- category_theory.limits.epi_coprod_to_pushout
- category_theory.arrow.epi_right
- 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
- category_theory.limits.multicoequalizer.sigma_π.category_theory.epi
- category_theory.limits.biprod.epi_desc_of_epi_left
- category_theory.limits.biprod.epi_desc_of_epi_right
- Module.epi_as_hom''_mkq
- category_theory.limits.colimit_quotient_coproduct_epi
- category_theory.abelian.epi_factor_thru_coimage
- category_theory.non_preadditive_abelian.category_theory.abelian.factor_thru_image.category_theory.epi
- category_theory.non_preadditive_abelian.epi_r
- category_theory.abelian.factor_thru_image.category_theory.epi
- category_theory.abelian.epi_pullback_of_epi_f
- category_theory.abelian.epi_pullback_of_epi_g
- category_theory.limits.factor_thru_image_subobject.category_theory.epi
- category_theory.limits.image_subobject_comp_le_epi_of_epi
- image_to_kernel_epi_of_zero_of_mono
- image_to_kernel_epi_of_epi_of_zero
- category_theory.exact.epi
- category_theory.limits.factor_thru_kernel_subobject.epi
- category_theory.limits.kernel.lift.epi
- category_theory.projective.π_epi
- category_theory.splitting.retraction.category_theory.epi
- algebraic_geometry.structure_sheaf.to_basic_open_epi
- category_theory.preserves_epi
- category_theory.glue_data.π_epi
- algebraic_geometry.SheafedSpace.base.category_theory.epi
- algebraic_geometry.Scheme.open_cover.base.category_theory.epi
- simplex_category.σ.category_theory.epi
- SemiNormedGroup.explicit_cokernel_π.epi
- category_theory.ProjectiveResolution.epi
- category_theory.ProjectiveResolution.f.category_theory.epi
- category_theory.abelian.homology_c_to_k.category_theory.epi
- category_theory.limits.wide_coequalizer.π_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 of this typeclass
- category_theory.is_iso.mono_of_iso
- category_theory.split_mono.mono
- category_theory.limits.initial.mono_from
- category_theory.mono_of_strong_mono
- category_theory.regular_mono.mono
- category_theory.category_struct.id.mono
- category_theory.unop_mono_of_epi
- category_theory.op_mono_of_epi
- category_theory.is_equivalence.mono_map
- category_theory.limits.equalizer.ι_mono
- 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.prod.map_mono
- category_theory.limits.pullback.fst_of_mono
- category_theory.limits.pullback.snd_of_mono
- category_theory.limits.mono_pullback_to_prod
- category_theory.arrow.mono_left
- category_theory.limits.mono_factorisation.m_mono
- category_theory.limits.image.ι.category_theory.mono
- category_theory.limits.image.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
- category_theory.limits.multiequalizer.ι_pi.category_theory.mono
- category_theory.limits.biprod.mono_lift_of_mono_left
- category_theory.limits.biprod.mono_lift_of_mono_right
- Module.mono_as_hom'_subtype
- category_theory.limits.limit_subobject_product_mono
- category_theory.abelian.mono_factor_thru_image
- category_theory.non_preadditive_abelian.category_theory.abelian.factor_thru_coimage.category_theory.mono
- category_theory.non_preadditive_abelian.mono_Δ
- category_theory.non_preadditive_abelian.mono_r
- category_theory.abelian.factor_thru_coimage.category_theory.mono
- category_theory.abelian.mono_pushout_of_mono_f
- category_theory.abelian.mono_pushout_of_mono_g
- 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.subobject.wide_pullback_ι_mono
- image_to_kernel.mono
- category_theory.abelian.category_theory.limits.cokernel.desc.category_theory.mono
- AddCommGroup.image.ι.category_theory.mono
- Module.image.ι.category_theory.mono
- category_theory.splitting.section.category_theory.mono
- algebraic_geometry.PresheafedSpace.of_restrict_mono
- category_theory.sieve.functor_inclusion_is_mono
- algebraic_geometry.PresheafedSpace.is_open_immersion.mono
- algebraic_geometry.SheafedSpace.is_open_immersion.category_theory.mono
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.mono
- algebraic_geometry.is_open_immersion.mono
- category_theory.preserves_mono
- category_theory.glue_data.f_mono
- Top.glue_data.ι_mono
- simplex_category.δ.category_theory.mono
- category_theory.abelian.homology_c_to_k.category_theory.mono
- category_theory.injective.ι_mono
- category_theory.InjectiveResolution.mono
- category_theory.InjectiveResolution.f.category_theory.mono
- category_theory.limits.wide_equalizer.ι_mono
- category_theory.initial.mono_to
- category_theory.limits.coprod.inl.category_theory.mono
- category_theory.limits.coprod.inr.category_theory.mono
- category_theory.simple_subobject_arrow.mono