Documentation Verification Report

Comma

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

Statistics

Metric	Count
Definitions `Comma`, `liftQuotient`, `projectQuotient`, `quotientEquiv`, `liftSubobject`, `projectSubobject`, `subobjectEquiv`	7
Theorems `lift_projectQuotient`, `projectQuotient_factors`, `projectQuotient_mk`, `unop_left_comp_ofMkLEMk_unop`, `unop_left_comp_underlyingIso_hom_unop`, `well_copowered_costructuredArrow`, `lift_projectSubobject`, `projectSubobject_factors`, `projectSubobject_mk`, `wellPowered_structuredArrow`	10
Total	17

CategoryTheory

Definitions

Name	Category	Theorems
`Comma` 📖	CompData	432 math math: `TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_hom_right`, `CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_hom`, `StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_left`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left`, `WithInitial.equivComma_functor_obj_right_obj`, `StructuredArrow.ofCommaSndEquivalenceFunctor_map_right`, `Comma.snd_obj`, `Comma.mapLeftEq_inv_app_right`, `Comma.mapLeftIso_inverse_map_right`, `Functor.leftExtensionEquivalenceOfIso₁_functor_map_left`, `Comma.opFunctor_obj`, `WithTerminal.equivComma_functor_obj_left_obj`, `StructuredArrow.mapIso_functor_obj_left`, `WithTerminal.equivComma_counitIso_hom_app_left_app`, `Comma.toPUnitIdEquiv_functor_map`, `StructuredArrow.commaMapEquivalenceInverse_map`, `Comma.map_obj_hom`, `WithTerminal.equivComma_counitIso_inv_app_left_app`, `StructuredArrow.ofCommaSndEquivalence_functor`, `Comma.toIdPUnitEquiv_inverse_map_right`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app`, `Comma.map_final`, `Comma.mapLeft_map_left`, `StructuredArrow.mapIso_inverse_obj_hom`, `CostructuredArrow.grothendieckPrecompFunctorToComma_map_left`, `Comma.fromProd_obj_hom`, `CostructuredArrow.mapNatIso_inverse_obj_left`, `CostructuredArrow.mapIso_functor_obj_hom`, `StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_right`, `Comma.fst_obj`, `Comma.mapLeftIso_functor_map_left`, `Comma.mapLeftIso_unitIso_inv_app_left`, `Functor.leftExtensionEquivalenceOfIso₁_functor_obj_left`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left`, `Comma.mapRightIso_counitIso_inv_app_left`, `TwoSquare.EquivalenceJ.inverse_map`, `StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_right`, `Comma.mapRightEq_hom_app_right`, `Comma.initial_fst`, `Comma.mapRightIso_counitIso_inv_app_right`, `Comma.opEquiv_counitIso`, `Comma.mapLeftEq_hom_app_left`, `Comma.isConnected_comma_of_initial`, `Comma.hasColimitsOfSize`, `Comma.coneOfPreserves_π_app_right`, `Comma.eqToHom_left`, `Comma.limitAuxiliaryCone_pt`, `WithTerminal.equivComma_inverse_obj_obj`, `Comma.hasColimitsOfShape`, `Comma.mapRightIso_functor_map_left`, `Comma.mapLeftIso_counitIso_inv_app_right`, `WithTerminal.equivComma_counitIso_hom_app_right`, `Comma.map_map_right`, `Comma.instEssSurjCompPostOfFull`, `CostructuredArrow.mapNatIso_inverse_map_right`, `StructuredArrow.mapNatIso_functor_obj_right`, `Comma.mapRight_obj_hom`, `Comma.mapRightIso_inverse_map_right`, `WithTerminal.equivComma_functor_obj_left_map`, `CostructuredArrow.mapNatIso_unitIso_inv_app_left`, `Comma.inv_left`, `CostructuredArrow.mapIso_unitIso_hom_app_left`, `WithTerminal.equivComma_functor_obj_right`, `Comma.mapRightIso_unitIso_inv_app_right`, `Comma.toPUnitIdEquiv_counitIso_hom_app`, `Comma.mapSnd_inv_app`, `Comma.fromProd_obj_right`, `CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor`, `Comma.mapRightIso_functor_obj_right`, `Comma.opFunctor_map`, `CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber`, `CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber`, `Comma.preRight_obj_left`, `WithTerminal.commaFromOver_map_left`, `WithInitial.equivComma_functor_obj_right_map`, `WithInitial.equivComma_counitIso_hom_app_right_app`, `Comma.rightIso_hom`, `CostructuredArrow.ιCompGrothendieckProj_inv_app`, `Comma.mapLeftIso_inverse_obj_left`, `CostructuredArrow.mapIso_inverse_obj_right`, `Comma.mapRight_obj_left`, `Comma.equivProd_unitIso_hom_app_left`, `Comma.comp_right`, `WithTerminal.commaFromOver_obj_right`, `StructuredArrow.ofCommaSndEquivalence_unitIso`, `TwoSquare.costructuredArrowRightwards_map`, `StructuredArrow.ofCommaSndEquivalence_counitIso`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map`, `CostructuredArrow.mapIso_functor_map_left`, `Comma.mapLeftIso_inverse_obj_right`, `Functor.leftExtensionEquivalenceOfIso₁_inverse_map_left`, `Comma.equivProd_counitIso_hom_app`, `Comma.mapRightId_inv_app_left`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj`, `Comma.instFaithfulCompPreLeft`, `Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_left`, `Comma.mapLeftId_hom_app_right`, `Comma.post_obj_right`, `Comma.preRight_map_left`, `MorphismProperty.Comma.instFullTopCommaForget`, `MorphismProperty.Comma.isoFromComma_hom`, `StructuredArrow.mapNatIso_functor_obj_hom`, `CostructuredArrow.mapIso_unitIso_inv_app_left`, `CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right`, `Comma.preLeft_obj_right`, `StructuredArrow.mapIso_inverse_obj_right`, `CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base`, `Comma.mapRightComp_inv_app_right`, `StructuredArrow.mapNatIso_inverse_map_right`, `Comma.instFaithfulCompPost`, `StructuredArrow.mapNatIso_functor_map_right`, `CostructuredArrow.ofCommaFstEquivalence_inverse`, `StructuredArrow.ofCommaSndEquivalenceInverse_map_right_left`, `CostructuredArrow.mapIso_functor_obj_left`, `WithInitial.equivComma_counitIso_inv_app_right_app`, `Comma.hasColimit`, `CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_hom`, `StructuredArrow.mapNatIso_inverse_obj_left`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left`, `WithTerminal.equivComma_functor_map_right`, `Comma.faithful_map`, `Comma.comp_left`, `Comma.toPUnitIdEquiv_functor_obj`, `WithInitial.commaFromUnder_map_left`, `Comma.fromProd_obj_left`, `StructuredArrow.ofCommaSndEquivalenceFunctor_map_left`, `Comma.mapLeftComp_inv_app_left`, `Comma.mapLeftIso_functor_obj_left`, `StructuredArrow.mapNatIso_unitIso_hom_app_right`, `Comma.natTrans_app`, `Comma.map_obj_right`, `Comma.coneOfPreserves_pt_right`, `Comma.equivProd_inverse_map_left`, `CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app`, `Comma.instFullCompPreLeft`, `Comma.equivProd_unitIso_hom_app_right`, `CostructuredArrow.ofCommaFstEquivalenceInverse_obj_right_as`, `Comma.preRight_map_right`, `CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_left`, `CostructuredArrow.mapNatIso_functor_obj_hom`, `Comma.map_map_left`, `Comma.mapRightIso_functor_obj_hom`, `Comma.toIdPUnitEquiv_unitIso_inv_app_right`, `Comma.post_map_left`, `CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left`, `Comma.toPUnitIdEquiv_unitIso_inv_app_left`, `Comma.colimitAuxiliaryCocone_pt`, `StructuredArrow.ofCommaSndEquivalenceFunctor_obj_right`, `Comma.coconeOfPreserves_pt_right`, `Comma.isCofiltered_of_initial`, `Comma.preservesColimitsOfShape_snd`, `Comma.snd_map`, `Comma.preRight_obj_right`, `Comma.mapLeftIso_unitIso_inv_app_right`, `CostructuredArrow.mapNatIso_counitIso_inv_app_left`, `Comma.isEquivalence_post`, `Comma.mapLeftIso_unitIso_hom_app_left`, `CostructuredArrow.mapIso_counitIso_hom_app_left`, `WithInitial.equivComma_functor_map_left`, `CostructuredArrow.mapCompιCompGrothendieckProj_inv_app`, `Comma.mapRightEq_inv_app_left`, `Functor.leftExtensionEquivalenceOfIso₁_inverse_map_right`, `Comma.isEquivalenceMap`, `Comma.eqToHom_right`, `CostructuredArrow.mapIso_functor_map_right`, `WithTerminal.equivComma_functor_obj_hom_app`, `WithInitial.equivComma_inverse_map_app`, `Comma.unopFunctor_obj`, `CostructuredArrow.mapNatIso_inverse_map_left`, `Comma.mapLeftComp_inv_app_right`, `Comma.equivProd_counitIso_inv_app`, `Comma.isEquivalence_preLeft`, `Comma.coconeOfPreserves_ι_app_right`, `Comma.toIdPUnitEquiv_unitIso_hom_app_right`, `WithInitial.equivComma_counitIso_hom_app_left`, `Comma.mapRightIso_inverse_obj_right`, `CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso`, `Comma.coconeOfPreserves_pt_hom`, `Comma.mapLeftIso_counitIso_hom_app_left`, `Comma.mapRightIso_functor_map_right`, `Comma.limitAuxiliaryCone_π_app`, `WithInitial.equivComma_functor_map_right_app`, `Comma.toIdPUnitEquiv_functor_map`, `Comma.toIdPUnitEquiv_inverse_obj_left_as`, `Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_right`, `StructuredArrow.commaMapEquivalenceInverse_obj`, `Functor.leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app`, `Comma.inv_right`, `WithInitial.equivComma_functor_obj_hom_app`, `Comma.toIdPUnitEquiv_functor_obj`, `StructuredArrow.mapNatIso_inverse_obj_hom`, `WithInitial.commaFromUnder_obj_hom_app`, `StructuredArrow.commaMapEquivalenceFunctor_obj_left`, `CostructuredArrow.mapNatIso_inverse_obj_hom`, `WithInitial.commaFromUnder_obj_right`, `WithInitial.equivComma_inverse_obj_map`, `Comma.toIdPUnitEquiv_counitIso_hom_app`, `Comma.mapRightComp_hom_app_left`, `StructuredArrow.commaMapEquivalenceFunctor_map_left`, `CostructuredArrow.ofCommaFstEquivalence_functor`, `Comma.toPUnitIdEquiv_inverse_map_left`, `Comma.mapRightIso_functor_obj_left`, `CostructuredArrow.ofCommaFstEquivalenceFunctor_map_right`, `MorphismProperty.Comma.forget_obj`, `Comma.unopFunctorCompSnd_inv_app`, `Comma.coconeOfPreserves_ι_app_left`, `Comma.equivProd_inverse_map_right`, `CostructuredArrow.mapNatIso_unitIso_hom_app_left`, `Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app`, `Comma.isoMk_inv_left`, `CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse`, `Comma.toPUnitIdEquiv_functor_iso`, `CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_left`, `StructuredArrow.mapIso_functor_obj_right`, `Comma.mapLeftEq_hom_app_right`, `StructuredArrow.mapIso_unitIso_inv_app_right`, `Comma.mapLeft_obj_right`, `Comma.hasLimitsOfSize`, `Comma.preservesColimitsOfShape_fst`, `Comma.opFunctorCompSnd_hom_app`, `StructuredArrow.mapIso_functor_map_left`, `Functor.leftExtensionEquivalenceOfIso₁_functor_obj_hom_app`, `Comma.mapLeftIso_inverse_obj_hom`, `StructuredArrow.commaMapEquivalenceFunctor_map_right`, `Comma.mapLeftId_hom_app_left`, `Comma.hasLimitsOfShape`, `Comma.post_obj_left`, `Comma.mapLeftId_inv_app_left`, `Comma.mapRightIso_counitIso_hom_app_right`, `Comma.fromProd_map_right`, `MorphismProperty.Comma.forget_map`, `Comma.equivProd_inverse_obj_right`, `Comma.isFiltered_of_final`, `WithTerminal.commaFromOver_obj_hom_app`, `Comma.opFunctorCompFst_hom_app`, `Comma.toPUnitIdEquiv_unitIso_hom_app_left`, `Comma.mapRightIso_unitIso_hom_app_left`, `WithInitial.equivComma_unitIso_inv_app_app`, `Comma.fromProd_map_left`, `Comma.full_map`, `WithInitial.commaFromUnder_map_right`, `WithInitial.equivComma_functor_obj_left`, `StructuredArrow.ofCommaSndEquivalenceInverse_obj_hom`, `Comma.opFunctorCompFst_inv_app`, `Comma.preRight_obj_hom`, `Comma.unopFunctor_map`, `Comma.instFullCompPreRight`, `CostructuredArrow.mapNatIso_functor_obj_left`, `Comma.instFullCompPostOfFaithful`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app`, `Comma.opEquiv_functor`, `MorphismProperty.Comma.id_hom`, `Comma.initial_snd`, `MorphismProperty.Comma.isoFromComma_inv`, `Comma.instFaithfulCompPreRight`, `Comma.mapLeftIso_unitIso_hom_app_right`, `CostructuredArrow.ofCommaFstEquivalence_counitIso`, `Comma.opEquiv_unitIso`, `StructuredArrow.mapNatIso_counitIso_hom_app_right`, `Comma.mapRightId_hom_app_right`, `CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_left`, `Comma.mapLeftIso_counitIso_inv_app_left`, `Comma.toPUnitIdEquiv_inverse_obj_right_as`, `MorphismProperty.Comma.instIsIsoCommaHom`, `Comma.mapRightIso_counitIso_hom_app_left`, `WithInitial.equivComma_unitIso_hom_app_app`, `CostructuredArrow.mapNatIso_functor_obj_right`, `StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_right`, `Comma.mapRightId_hom_app_left`, `CostructuredArrow.ofCommaFstEquivalenceFunctor_map_left`, `Comma.final_fst`, `Comma.mapLeftEq_inv_app_left`, `WithTerminal.commaFromOver_map_right`, `Comma.mapLeftIso_counitIso_hom_app_right`, `WithInitial.equivComma_inverse_obj_obj`, `Comma.instEssSurjCompPreLeft`, `StructuredArrow.ofCommaSndEquivalenceInverse_map_right_right`, `CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_right`, `Comma.mapFst_hom_app`, `Comma.mapLeft_map_right`, `Comma.mapLeft_obj_left`, `Comma.coneOfPreserves_pt_hom`, `Comma.unopFunctorCompFst_inv_app`, `Comma.leftIso_hom`, `Comma.equivProd_unitIso_inv_app_right`, `WithInitial.commaFromUnder_obj_left`, `CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso`, `TwoSquare.EquivalenceJ.functor_obj`, `Comma.toPUnitIdEquiv_inverse_obj_left`, `StructuredArrow.mapIso_unitIso_hom_app_right`, `MorphismProperty.Comma.instFaithfulCommaForget`, `Comma.mapLeftIso_functor_obj_hom`, `Comma.isEquivalence_preRight`, `StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_right`, `CostructuredArrow.mapNatIso_counitIso_hom_app_left`, `Comma.final_snd`, `Comma.leftIso_inv`, `StructuredArrow.mapIso_functor_obj_hom`, `StructuredArrow.mapNatIso_unitIso_inv_app_right`, `WithInitial.equivComma_counitIso_inv_app_left`, `Comma.isConnected_comma_of_final`, `Comma.mapRight_map_left`, `Comma.mapRightId_inv_app_right`, `Comma.mapRightComp_hom_app_right`, `Comma.opFunctorCompSnd_inv_app`, `Comma.isoMk_hom_right`, `Comma.mapRightIso_inverse_obj_hom`, `CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_right`, `StructuredArrow.mapIso_inverse_map_right`, `Comma.id_left`, `TwoSquare.structuredArrowDownwards_map`, `CostructuredArrow.mapCompιCompGrothendieckProj_hom_app`, `WithTerminal.equivComma_functor_map_left_app`, `Comma.preLeft_map_left`, `StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left`, `Comma.opEquiv_inverse`, `TwoSquare.structuredArrowDownwards_obj`, `CostructuredArrow.mapNatIso_inverse_obj_right`, `MorphismProperty.Comma.inv_hom`, `Comma.id_right`, `MorphismProperty.Comma.instReflectsIsomorphismsCommaForgetOfRespectsIso`, `CostructuredArrow.mapNatIso_functor_map_left`, `Comma.mapRightIso_unitIso_inv_app_left`, `WithInitial.liftFromUnder_map_app`, `CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app`, `Comma.essSurj_map`, `Comma.equivProd_inverse_obj_left`, `Functor.leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app`, `Comma.hasLimit`, `Comma.mapSnd_hom_app`, `StructuredArrow.mapNatIso_functor_obj_left`, `StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_left`, `Comma.toPUnitIdEquiv_counitIso_inv_app`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app`, `CostructuredArrow.ofCommaFstEquivalence_unitIso`, `TwoSquare.EquivalenceJ.functor_map`, `StructuredArrow.mapIso_inverse_obj_left`, `Comma.instEssSurjCompPreRight`, `Comma.locallySmall`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map`, `Comma.mapRightEq_hom_app_left`, `StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_left`, `Comma.mapRightEq_inv_app_right`, `StructuredArrow.mapIso_functor_map_right`, `Comma.coneOfPreserves_pt_left`, `StructuredArrow.ofCommaSndEquivalence_inverse`, `Comma.post_map_right`, `WithTerminal.equivComma_inverse_map_app`, `CostructuredArrow.mapIso_functor_obj_right`, `WithTerminal.equivComma_inverse_obj_map`, `Comma.toIdPUnitEquiv_counitIso_inv_app`, `Comma.coconeOfPreserves_pt_left`, `MorphismProperty.Comma.comp_hom`, `WithTerminal.liftFromOver_map_app`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app`, `CostructuredArrow.grothendieckPrecompFunctorToComma_map_right`, `MorphismProperty.instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`, `Comma.equivProd_functor_map`, `TwoSquare.EquivalenceJ.inverse_obj`, `Comma.mapLeftIso_inverse_map_left`, `Comma.preLeft_obj_left`, `Comma.mapRight_obj_right`, `Comma.mapLeftComp_hom_app_left`, `Comma.mapLeftIso_functor_obj_right`, `StructuredArrow.mapIso_inverse_map_left`, `Comma.mapLeft_obj_hom`, `CostructuredArrow.ιCompGrothendieckProj_hom_app`, `StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_hom`, `CostructuredArrow.mapNatIso_functor_map_right`, `CostructuredArrow.mapIso_inverse_obj_hom`, `WithTerminal.commaFromOver_obj_left`, `Comma.equivProd_unitIso_inv_app_left`, `Comma.unopFunctorCompSnd_hom_app`, `Comma.preLeft_map_right`, `Comma.toIdPUnitEquiv_functor_iso`, `CostructuredArrow.mapIso_inverse_map_right`, `StructuredArrow.ofCommaSndEquivalenceInverse_obj_left_as`, `Comma.post_obj_hom`, `Functor.leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app`, `WithTerminal.equivComma_counitIso_inv_app_right`, `Comma.unopFunctorCompFst_hom_app`, `CostructuredArrow.mapIso_inverse_map_left`, `Comma.isoMk_inv_right`, `StructuredArrow.mapNatIso_inverse_map_left`, `Comma.map_fst`, `CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base`, `WithTerminal.equivComma_unitIso_hom_app_app`, `TwoSquare.costructuredArrowRightwards_obj`, `Comma.toIdPUnitEquiv_inverse_obj_right`, `Comma.colimitAuxiliaryCocone_ι_app`, `Comma.mapRightIso_inverse_obj_left`, `CostructuredArrow.ofCommaFstEquivalenceInverse_obj_hom`, `Comma.fst_map`, `StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_right`, `Comma.mapRightIso_inverse_map_left`, `Comma.mapLeftId_inv_app_right`, `StructuredArrow.mapNatIso_functor_map_left`, `Comma.map_snd`, `StructuredArrow.mapNatIso_counitIso_inv_app_right`, `StructuredArrow.commaMapEquivalenceFunctor_obj_right`, `Functor.leftExtensionEquivalenceOfIso₁_functor_map_right`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app`, `Comma.rightIso_inv`, `WithTerminal.equivComma_unitIso_inv_app_app`, `CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom`, `Comma.mapLeftComp_hom_app_right`, `StructuredArrow.ofCommaSndEquivalenceFunctor_obj_hom`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj`, `Comma.mapRight_map_right`, `Comma.isoMk_hom_left`, `Functor.leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app`, `Comma.mapFst_inv_app`, `CostructuredArrow.mapIso_counitIso_inv_app_left`, `Comma.mapLeftIso_functor_map_right`, `StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_right`, `StructuredArrow.mapIso_counitIso_hom_app_right`, `Comma.equivProd_functor_obj`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left`, `Comma.map_obj_left`, `AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app`, `Comma.mapRightComp_inv_app_left`, `StructuredArrow.mapNatIso_inverse_obj_right`, `StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_right`, `StructuredArrow.mapIso_counitIso_inv_app_right`, `Comma.mapRightIso_unitIso_hom_app_right`, `StructuredArrow.commaMapEquivalenceFunctor_obj_hom`, `Comma.preLeft_obj_hom`, `Functor.leftExtensionEquivalenceOfIso₁_functor_obj_right`, `CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_right`, `CostructuredArrow.mapIso_inverse_obj_left`, `Comma.coneOfPreserves_π_app_left`

CategoryTheory.CostructuredArrow

Definitions

Name	Category	Theorems
`liftQuotient` 📖	CompOp	1 math math: `lift_projectQuotient`
`projectQuotient` 📖	CompOp	2 math math: `projectQuotient_factors`, `projectQuotient_mk`
`quotientEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_projectQuotient` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite.unop` `Opposite.op` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Subobject` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `projectQuotient` `CategoryTheory.Comma.right` `CategoryTheory.Functor.map` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Subobject.arrow` `CategoryTheory.Comma.hom`	`liftQuotient`	—	`CategoryTheory.Subobject.ind` `CategoryTheory.Subobject.mk_eq_mk_of_comm` `CategoryTheory.op_mono_of_epi` `epi_left_of_epi` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits` `CategoryTheory.unop_epi_of_mono` `CategoryTheory.cancel_epi` `CategoryTheory.Functor.map_epi` `CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape` `CategoryTheory.Functor.map_comp` `unop_left_comp_underlyingIso_hom_unop` `CategoryTheory.CommaMorphism.w` `CategoryTheory.Category.comp_id`
`projectQuotient_factors` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite.unop` `Opposite.op` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Subobject` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `projectQuotient` `CategoryTheory.Comma.right` `CategoryTheory.Functor.map` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Subobject.arrow` `CategoryTheory.Comma.hom`	—	`CategoryTheory.Subobject.ind` `CategoryTheory.MonoOver.mono` `CategoryTheory.op_mono_of_epi` `epi_left_of_epi` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits` `CategoryTheory.unop_epi_of_mono` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.unop_comp` `CategoryTheory.Subobject.underlyingIso_arrow` `CategoryTheory.CommaMorphism.w` `CategoryTheory.Category.comp_id`
`projectQuotient_mk` 📖	mathematical	—	`projectQuotient` `Opposite` `CategoryTheory.CostructuredArrow` `CategoryTheory.Category.opposite` `CategoryTheory.instCategoryCostructuredArrow` `Opposite.op` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CommaMorphism.left` `Quiver.Hom.unop` `CategoryTheory.op_mono_of_epi` `epi_left_of_epi` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.finCategoryWidePushout` `CategoryTheory.unop_epi_of_mono`	—	—
`unop_left_comp_ofMkLEMk_unop` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `Opposite.unop` `CategoryTheory.CostructuredArrow` `Opposite.op` `CategoryTheory.CommaMorphism.left` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.Subobject.ofMkLEMk` `Opposite` `CategoryTheory.Category.opposite` `Quiver.Hom.op`	—	`Quiver.Hom.unop_op` `CategoryTheory.unop_comp` `CategoryTheory.Subobject.ofMkLEMk_comp`
`unop_left_comp_underlyingIso_hom_unop` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `Opposite.unop` `CategoryTheory.CostructuredArrow` `Opposite.op` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.CommaMorphism.left` `Quiver.Hom.unop` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.Iso.hom` `CategoryTheory.Subobject.underlyingIso` `CategoryTheory.Subobject.arrow`	—	`Quiver.Hom.unop_op` `CategoryTheory.unop_comp`
`well_copowered_costructuredArrow` 📖	mathematical	—	`CategoryTheory.WellPowered` `Opposite` `CategoryTheory.CostructuredArrow` `CategoryTheory.Category.opposite` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.instLocallySmallOpposite` `locallySmall`	—	`CategoryTheory.instLocallySmallOpposite` `locallySmall` `small_map` `small_subtype` `CategoryTheory.small_subobject`

CategoryTheory.StructuredArrow

Definitions

Name	Category	Theorems
`liftSubobject` 📖	CompOp	1 math math: `lift_projectSubobject`
`projectSubobject` 📖	CompOp	2 math math: `projectSubobject_mk`, `projectSubobject_factors`
`subobjectEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_projectSubobject` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Subobject` `CategoryTheory.Comma.right` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `projectSubobject` `CategoryTheory.Functor.map` `CategoryTheory.Subobject.arrow` `CategoryTheory.Comma.hom`	`liftSubobject`	—	`CategoryTheory.Subobject.ind` `CategoryTheory.Subobject.mk_eq_mk_of_comm` `CategoryTheory.MonoOver.mono` `CategoryTheory.cancel_mono` `CategoryTheory.Functor.map_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `mono_right_of_mono` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `w` `ext`
`projectSubobject_factors` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Subobject` `CategoryTheory.Comma.right` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `projectSubobject` `CategoryTheory.Functor.map` `CategoryTheory.Subobject.arrow` `CategoryTheory.Comma.hom`	—	`CategoryTheory.Subobject.ind` `CategoryTheory.MonoOver.mono` `mono_right_of_mono` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Subobject.underlyingIso_arrow` `w`
`projectSubobject_mk` 📖	mathematical	—	`projectSubobject` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.right` `mono_right_of_mono` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.finCategoryWidePullback`	—	—
`wellPowered_structuredArrow` 📖	mathematical	—	`CategoryTheory.WellPowered` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `locallySmall`	—	`locallySmall` `small_map` `small_subtype` `CategoryTheory.small_subobject`

---

← Back to Index