Quotient

📁 Source: Mathlib/CategoryTheory/Quotient.lean

Statistics

Metric	Count
Definitions homRel, CompClosure, IsStableUnderPostcomp, IsStableUnderPrecomp, Quotient, CompClosure, as, category, comp, equiv, functor, groupoid, instInhabitedHom, instUnique, inv, isLift, natIsoLift, natTransLift, instInhabitedQuotient, HomRel, instInhabitedHomRel	21
Theorems compLeft, compRight, equivalence, toIsStableUnderPostcomp, toIsStableUnderPrecomp, congruence_homRel, homRel_iff, of, comp_right, comp_left, compClosure_eq_self, compClosure_iff_self, instIsStableUnderPostcompCompClosure, instIsStableUnderPrecompCompClosure, of, congruence, compClosure_eq_self, compClosure_iff_self, comp_left, comp_mk, comp_natTransLift, comp_natTransLift_assoc, comp_right, essSurj_functor, ext, ext_iff, faithful_whiskeringLeft_functor, full_functor, full_whiskeringLeft_functor, functor_homRel_eq_compClosure_eqvGen, functor_map_eq_iff, induction, instSubsingletonHom, inv_mk, isLift_hom, isLift_inv, lift_map_functor_map, lift_obj_functor_obj, lift_spec, lift_unique, lift_unique', natIsoLift_hom, natIsoLift_inv, natTransLift_app, natTransLift_id, natTrans_ext, sound	47
Total	68

CategoryTheory

Definitions

Name	Category	Theorems
Quotient 📖	CompData	34 math math: Quotient.natIsoLift_inv, Quotient.Linear.smul_eq, Quotient.functor_additive, Quotient.comp_natTransLift_assoc, Quotient.lift.isLift_hom, HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor, Quotient.linear_functor, Quotient.full_functor, Quotient.LiftCommShift.iso_hom_app, Quotient.liftCommShift_compatibility, Quotient.natTransLift_id, Quotient.lift_map_functor_map, quotientPathsTo_obj, Quotient.instSubsingletonHom, Quotient.functor_homRel_eq_compClosure_eqvGen, MorphismProperty.eq_inverseImage_quotientFunctor, Quotient.functor_map_eq_iff, Quotient.natIsoLift_hom, Quotient.lift_obj_functor_obj, Quotient.essSurj_functor, Quotient.full_whiskeringLeft_functor, Quotient.faithful_whiskeringLeft_functor, toQuotientPaths_obj_as, Quotient.liftCommShift_commShiftIso, Quotient.lift.isLift_inv, Quotient.LiftCommShift.iso_inv_app, Quiver.FreeGroupoid.of_eq, Quotient.lift_spec, Quotient.sound, toQuotientPaths_map, Quotient.natTransLift_app, quotientPathsTo_map, MorphismProperty.quotient_iff, Quotient.comp_natTransLift
instInhabitedQuotient 📖	CompOp	—

CategoryTheory.Congruence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compLeft 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left
compRight 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right
equivalence 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
toIsStableUnderPostcomp 📖	mathematical	—	CategoryTheory.HomRel.IsStableUnderPostcomp	—	—
toIsStableUnderPrecomp 📖	mathematical	—	CategoryTheory.HomRel.IsStableUnderPrecomp	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
homRel 📖	CompOp	3 math math: homRel_iff, CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen, congruence_homRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congruence_homRel 📖	mathematical	—	CategoryTheory.Congruence homRel	—	map_comp
homRel_iff 📖	mathematical	—	homRel map	—	—

CategoryTheory.HomRel

Definitions

Name	Category	Theorems
CompClosure 📖	CompData	21 math math: HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.Quotient.CompClosure.of, HomotopyCategory.quot_mk_eq_quotient_map, CategoryTheory.Localization.Construction.lift_map, CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen, compClosure_iff_self, CategoryTheory.Quotient.compClosure.congruence, Quiver.FreeGroupoid.congr_comp_reverse, instIsStableUnderPostcompCompClosure, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, CategoryTheory.Quotient.compClosure_iff_self, CategoryTheory.Quotient.inv_mk, compClosure_eq_self, CompClosure.of, CategoryTheory.Quotient.compClosure_eq_self, instIsStableUnderPrecompCompClosure, HomotopyCategory.quotient_map_out, Quiver.FreeGroupoid.congr_reverse_comp, CategoryTheory.toQuotientPaths_map, CategoryTheory.quotientPathsTo_map, CategoryTheory.Quotient.comp_mk
IsStableUnderPostcomp 📖	CompData	5 math math: instIsStableUnderPostcompCompClosure, HomotopicalAlgebra.BifibrantObject.instIsStableUnderPostcompHomRel, CategoryTheory.Congruence.toIsStableUnderPostcomp, HomotopicalAlgebra.CofibrantObject.instIsStableUnderPostcompHomRel, HomotopicalAlgebra.FibrantObject.instIsStableUnderPostcompHomRel
IsStableUnderPrecomp 📖	CompData	5 math math: HomotopicalAlgebra.FibrantObject.instIsStableUnderPrecompHomRel, CategoryTheory.Congruence.toIsStableUnderPrecomp, HomotopicalAlgebra.CofibrantObject.instIsStableUnderPrecompHomRel, HomotopicalAlgebra.BifibrantObject.instIsStableUnderPrecompHomRel, instIsStableUnderPrecompCompClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compClosure_eq_self 📖	mathematical	—	CompClosure	—	—
compClosure_iff_self 📖	mathematical	—	CompClosure	—	IsStableUnderPrecomp.comp_left IsStableUnderPostcomp.comp_right CompClosure.of
instIsStableUnderPostcompCompClosure 📖	mathematical	—	IsStableUnderPostcomp CompClosure	—	CategoryTheory.Category.assoc
instIsStableUnderPrecompCompClosure 📖	mathematical	—	IsStableUnderPrecomp CompClosure	—	CategoryTheory.Category.assoc

CategoryTheory.HomRel.CompClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of 📖	mathematical	—	CategoryTheory.HomRel.CompClosure	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

CategoryTheory.HomRel.IsStableUnderPostcomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.HomRel.IsStableUnderPrecomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Quotient

Definitions

Name	Category	Theorems
CompClosure 📖	CompOp	—
as 📖	CompOp	19 math math: HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.Localization.Construction.lift_obj, CategoryTheory.NatTrans.mapHomotopyCategory_app, HomotopyCategory.quot_mk_eq_quotient_map, CategoryTheory.quotientPathsTo_obj, CategoryTheory.Localization.Construction.lift_map, CategoryTheory.FreeGroupoid.eq_mk, ext_iff, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, inv_mk, HomotopyCategory.quotient_obj_as, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj, CategoryTheory.Functor.mapHomotopyCategory_obj, CategoryTheory.toQuotientPaths_obj_as, CategoryTheory.Localization.Construction.objEquiv_symm_apply, HomotopyCategory.quotient_map_out, CategoryTheory.toQuotientPaths_map, CategoryTheory.quotientPathsTo_map, comp_mk
category 📖	CompOp	93 math math: HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj, natIsoLift_inv, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, Linear.smul_eq, functor_additive, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply, HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, comp_natTransLift_assoc, lift.isLift_hom, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply, HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac', HomotopicalAlgebra.FibrantObject.toHoCat_map_eq_iff, linear_functor, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply, HomotopicalAlgebra.FibrantObject.weakEquivalence_toHoCat_map_iff, full_functor, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq, HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence, LiftCommShift.iso_hom_app, liftCommShift_compatibility, HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, natTransLift_id, HomotopicalAlgebra.FibrantObject.instFullHoCatToHoCat, HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, lift_map_functor_map, CategoryTheory.quotientPathsTo_obj, instSubsingletonHom, HomotopicalAlgebra.CofibrantObject.instFullHoCatToHoCat, functor_homRel_eq_compClosure_eqvGen, HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective, HomotopicalAlgebra.FibrantObject.toHoCat_map_eq, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor, functor_map_eq_iff, HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj_hom_ext, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj_hom_ext, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map, natIsoLift_hom, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans_app, lift_obj_functor_obj, HomotopicalAlgebra.FibrantObject.toHoCat_obj_surjective, essSurj_functor, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', full_whiskeringLeft_functor, faithful_whiskeringLeft_functor, CategoryTheory.toQuotientPaths_obj_as, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, liftCommShift_commShiftIso, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, lift.isLift_inv, CategoryTheory.PreOneHypercover.Homotopy.map_eq_map, LiftCommShift.iso_inv_app, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans_app, Quiver.FreeGroupoid.of_eq, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map, CategoryTheory.GrothendieckTopology.HOneHypercover.isCofiltered_of_hasPullbacks, lift_spec, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution_functor, sound, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution_functor, CategoryTheory.toQuotientPaths_map, natTransLift_app, CategoryTheory.quotientPathsTo_map, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc, HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq, CategoryTheory.MorphismProperty.quotient_iff, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map, comp_natTransLift
comp 📖	CompOp	1 math math: comp_mk
equiv 📖	CompOp	—
functor 📖	CompOp	28 math math: natIsoLift_inv, Linear.smul_eq, functor_additive, comp_natTransLift_assoc, lift.isLift_hom, HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor, linear_functor, full_functor, LiftCommShift.iso_hom_app, liftCommShift_compatibility, natTransLift_id, lift_map_functor_map, functor_homRel_eq_compClosure_eqvGen, CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor, functor_map_eq_iff, natIsoLift_hom, lift_obj_functor_obj, essSurj_functor, full_whiskeringLeft_functor, faithful_whiskeringLeft_functor, lift.isLift_inv, LiftCommShift.iso_inv_app, Quiver.FreeGroupoid.of_eq, lift_spec, sound, natTransLift_app, CategoryTheory.MorphismProperty.quotient_iff, comp_natTransLift
groupoid 📖	CompOp	—
instInhabitedHom 📖	CompOp	—
instUnique 📖	CompOp	—
inv 📖	CompOp	1 math math: inv_mk
natIsoLift 📖	CompOp	2 math math: natIsoLift_inv, natIsoLift_hom
natTransLift 📖	CompOp	6 math math: natIsoLift_inv, comp_natTransLift_assoc, natTransLift_id, natIsoLift_hom, natTransLift_app, comp_natTransLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compClosure_eq_self 📖	mathematical	—	CategoryTheory.HomRel.CompClosure	—	CategoryTheory.HomRel.compClosure_eq_self
compClosure_iff_self 📖	mathematical	—	CategoryTheory.HomRel.CompClosure	—	CategoryTheory.HomRel.compClosure_iff_self
comp_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left
comp_mk 📖	mathematical	—	comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct as CategoryTheory.HomRel.CompClosure CategoryTheory.CategoryStruct.comp	—	—
comp_natTransLift 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Quotient category CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category natTransLift CategoryTheory.Functor.comp functor	—	—
comp_natTransLift_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Quotient category CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category natTransLift CategoryTheory.Functor.comp functor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_natTransLift
comp_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right
essSurj_functor 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.Quotient category functor	—	—
ext 📖	—	as	—	—	—
ext_iff 📖	mathematical	—	as	—	ext
faithful_whiskeringLeft_functor 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor CategoryTheory.Quotient category CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft functor	—	natTrans_ext
full_functor 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Quotient category functor	—	Quot.out_eq
full_whiskeringLeft_functor 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor CategoryTheory.Quotient category CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft functor	—	—
functor_homRel_eq_compClosure_eqvGen 📖	mathematical	—	CategoryTheory.Functor.homRel CategoryTheory.Quotient category functor Relation.EqvGen Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.HomRel.CompClosure	—	Quot.eq
functor_map_eq_iff 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Quotient category functor	—	Equivalence.quot_mk_eq_iff CategoryTheory.HomRel.compClosure_eq_self CategoryTheory.Congruence.toIsStableUnderPrecomp CategoryTheory.Congruence.toIsStableUnderPostcomp CategoryTheory.Congruence.equivalence
induction 📖	—	CategoryTheory.Functor.obj CategoryTheory.Quotient category functor CategoryTheory.Functor.map	—	—	—
instSubsingletonHom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Quotient category	—	Function.Surjective.subsingleton CategoryTheory.Functor.Full.map_surjective full_functor
inv_mk 📖	mathematical	—	inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory as CategoryTheory.HomRel.CompClosure CategoryTheory.Groupoid.inv	—	—
lift_map_functor_map 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.Quotient category lift CategoryTheory.Functor.obj functor	—	—
lift_obj_functor_obj 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.Functor.obj CategoryTheory.Quotient category lift functor	—	—
lift_spec 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.Functor.comp CategoryTheory.Quotient category functor lift	—	—
lift_unique 📖	mathematical	CategoryTheory.Functor.map CategoryTheory.Functor.comp CategoryTheory.Quotient category functor	lift	—	CategoryTheory.Functor.hext
lift_unique' 📖	—	CategoryTheory.Functor.comp CategoryTheory.Quotient category functor	—	—	sound lift_unique
natIsoLift_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Quotient category CategoryTheory.Functor.category natIsoLift natTransLift CategoryTheory.Functor.comp functor	—	—
natIsoLift_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Quotient category CategoryTheory.Functor.category natIsoLift natTransLift CategoryTheory.Functor.comp functor	—	—
natTransLift_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Quotient category natTransLift CategoryTheory.Functor.obj functor CategoryTheory.Functor.comp	—	—
natTransLift_id 📖	mathematical	—	natTransLift CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Quotient category functor	—	—
natTrans_ext 📖	—	CategoryTheory.Functor.whiskerLeft CategoryTheory.Quotient category functor	—	—	CategoryTheory.NatTrans.ext CategoryTheory.NatTrans.congr_app
sound 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Quotient category functor	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

CategoryTheory.Quotient.CompClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of 📖	mathematical	—	CategoryTheory.HomRel.CompClosure	—	CategoryTheory.HomRel.CompClosure.of

CategoryTheory.Quotient.compClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congruence 📖	mathematical	—	CategoryTheory.Congruence Relation.EqvGen Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.HomRel.CompClosure	—	CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen CategoryTheory.Functor.congruence_homRel

CategoryTheory.Quotient.lift

Definitions

Name	Category	Theorems
isLift 📖	CompOp	3 math math: isLift_hom, CategoryTheory.Quotient.liftCommShift_compatibility, isLift_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLift_hom 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Quotient CategoryTheory.Quotient.category CategoryTheory.Quotient.functor CategoryTheory.Quotient.lift CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category isLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
isLift_inv 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Quotient CategoryTheory.Quotient.category CategoryTheory.Quotient.functor CategoryTheory.Quotient.lift CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category isLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—

(root)

Definitions

Name	Category	Theorems
HomRel 📖	CompOp	—
instInhabitedHomRel 📖	CompOp	—

---

← Back to Index