Comma

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

Statistics

Metric	Count
Definitions `Comma`, `hom`, `comp`, `hom`, `toCommaMorphism`, `changeProp`, `forget`, `forgetFullyFaithful`, `fullyFaithfulChangeProp`, `homFromCommaOfIsIso`, `id`, `instCategory`, `isoFromComma`, `isoMk`, `mapLeft`, `mapRight`, `toComma`, `forget`, `homMk`, `mk`, `toOver`, `mk`, `forget`, `homMk`, `isoMk`, `mk`, `Under`, `mk`, `forget`, `homMk`, `isoMk`, `mk`, `commaObj`, `costructuredArrowObj`, `over`, `overObj`, `structuredArrowObj`, `under`, `underObj`	39
Theorems `comp_left`, `comp_right`, `ext`, `ext'`, `ext'_iff`, `ext_iff`, `hom_left`, `hom_mk`, `hom_right`, `prop_hom_left`, `prop_hom_right`, `comp_hom`, `comp_left`, `comp_left_assoc`, `comp_right`, `comp_right_assoc`, `eqToHom_left`, `eqToHom_right`, `ext`, `ext_iff`, `forget_map`, `forget_obj`, `homFromCommaOfIsIso_hom`, `hom_homFromCommaOfIsIso`, `id_hom`, `id_left`, `id_right`, `instFaithfulChangeProp`, `instFaithfulCommaForget`, `instFullChangeProp`, `instFullTopCommaForget`, `instIsIsoCommaHom`, `instIsIsoHomFromCommaOfIsIso`, `instReflectsIsomorphismsCommaForgetOfRespectsIso`, `inv_hom`, `isoFromComma_hom`, `isoFromComma_inv`, `isoMk_hom_left`, `isoMk_hom_right`, `isoMk_inv_left`, `isoMk_inv_right`, `lift_map_hom`, `lift_obj_toComma`, `mapLeft_map_left`, `mapLeft_map_right`, `mapLeft_obj_hom`, `mapLeft_obj_left`, `mapLeft_obj_right`, `mapRight_map_left`, `mapRight_map_right`, `mapRight_obj_hom`, `mapRight_obj_left`, `mapRight_obj_right`, `prop`, `toCommaMorphism_eq_hom`, `ext`, `ext_iff`, `homMk_left`, `mk_hom`, `mk_left`, `toOver_map`, `toOver_obj`, `over`, `ext`, `ext_iff`, `mk_hom`, `forget_comp_forget_map`, `homMk_hom`, `isoMk_hom_left`, `isoMk_inv_left`, `mk_hom`, `mk_left`, `w`, `w_assoc`, `ext`, `ext_iff`, `mk_hom`, `forget_comp_forget_map`, `homMk_hom`, `isoMk_hom_right`, `isoMk_inv_right`, `mk_hom`, `mk_left`, `w`, `w_assoc`, `commaObj_iff`, `costructuredArrowObj_iff`, `costructuredArrow_iso_iff`, `instFaithfulCostructuredArrowTopOverToOver`, `instFaithfulOverTopOverForget`, `instFaithfulUnderTopUnderForget`, `instFullCostructuredArrowTopOverToOver`, `instFullOverTopOverForget`, `instFullUnderTopUnderForget`, `instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`, `instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso`, `instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso`, `instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso`, `instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso`, `overObj_iff`, `over_eq_inverseImage`, `over_iff`, `over_iso_iff`, `structuredArrowObj_iff`, `underObj_iff`, `under_eq_inverseImage`, `under_iff`	107
Total	146

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`Comma` 📖	CompData	39 math math: `Comma.instFaithfulChangeProp`, `Comma.eqToHom_left`, `Comma.comp_right`, `Comma.instFullChangeProp`, `Comma.isoMk_hom_left`, `Comma.comp_left_assoc`, `Comma.mapLeft_obj_hom`, `Comma.instFullTopCommaForget`, `Comma.isoFromComma_hom`, `Comma.isoMk_hom_right`, `Comma.isoMk_inv_left`, `Comma.mapRight_obj_left`, `Comma.lift_obj_toComma`, `Comma.comp_right_assoc`, `Comma.mapLeft_map_right`, `Comma.mapLeft_obj_left`, `Comma.forget_obj`, `Comma.mapRight_obj_right`, `Comma.mapRight_map_right`, `Comma.forget_map`, `Comma.comp_left`, `Comma.id_hom`, `Comma.isoFromComma_inv`, `Comma.isoMk_inv_right`, `Comma.mapRight_map_left`, `Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape`, `Comma.instFaithfulCommaForget`, `Comma.mapRight_obj_hom`, `Comma.hasColimit_of_closedUnderColimitsOfShape`, `Comma.mapLeft_obj_right`, `Comma.inv_hom`, `Comma.instReflectsIsomorphismsCommaForgetOfRespectsIso`, `Comma.instIsIsoHomFromCommaOfIsIso`, `Comma.eqToHom_right`, `Comma.comp_hom`, `Comma.lift_map_hom`, `Comma.mapLeft_map_left`, `Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape`, `Comma.hasLimit_of_closedUnderLimitsOfShape`
`Under` 📖	CompOp	6 math math: `Under.isoMk_inv_right`, `Under.isoMk_hom_right`, `instFullUnderTopUnderForget`, `Under.forget_comp_forget_map`, `essentiallySmall_of_le`, `instFaithfulUnderTopUnderForget`
`commaObj` 📖	CompOp	2 math math: `commaObj_iff`, `instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`
`costructuredArrowObj` 📖	CompOp	4 math math: `CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty`, `instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso`, `CategoryTheory.CostructuredArrow.isClosedUnderColimitsOfShape`, `costructuredArrowObj_iff`
`over` 📖	CompOp	8 math math: `over_eq_inverseImage`, `HasFactorization.over`, `HomotopicalAlgebra.trivialFibrations_over_eq`, `HomotopicalAlgebra.trivialCofibrations_over_eq`, `HomotopicalAlgebra.fibrations_over_def`, `HomotopicalAlgebra.cofibrations_over_def`, `over_iff`, `HomotopicalAlgebra.weakEquivalences_over_def`
`overObj` 📖	CompOp	4 math math: `instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso`, `overObj_iff`, `CategoryTheory.Over.closedUnderLimitsOfShape_pullback`, `CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty`
`structuredArrowObj` 📖	CompOp	2 math math: `instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso`, `structuredArrowObj_iff`
`under` 📖	CompOp	2 math math: `under_iff`, `under_eq_inverseImage`
`underObj` 📖	CompOp	4 math math: `instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso`, `ind_iff_ind_underMk`, `underObj_ind_eq_ind_underObj`, `underObj_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commaObj_iff` 📖	mathematical	—	`commaObj` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	—
`costructuredArrowObj_iff` 📖	mathematical	—	`costructuredArrowObj` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	—
`costructuredArrow_iso_iff` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	`comma_iso_iff`
`instFaithfulCostructuredArrowTopOverToOver` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CostructuredArrow` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `instCompleteBooleanAlgebra` `Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `IsMultiplicative.instTop` `Over` `CategoryTheory.Functor.id` `CostructuredArrow.toOver`	—	`IsMultiplicative.instTop` `CostructuredArrow.Hom.ext` `CategoryTheory.Functor.map_injective`
`instFaithfulOverTopOverForget` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Over` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `instCompleteBooleanAlgebra` `Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `IsMultiplicative.instTop` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `Over.forget`	—	`IsMultiplicative.instTop` `Comma.instFaithfulCommaForget`
`instFaithfulUnderTopUnderForget` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Under` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `instCompleteBooleanAlgebra` `Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `IsMultiplicative.instTop` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `Under.forget`	—	`IsMultiplicative.instTop` `Comma.instFaithfulCommaForget`
`instFullCostructuredArrowTopOverToOver` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CostructuredArrow` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `instCompleteBooleanAlgebra` `Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `IsMultiplicative.instTop` `Over` `CategoryTheory.Functor.id` `CostructuredArrow.toOver`	—	`IsMultiplicative.instTop` `CategoryTheory.Functor.map_preimage` `CategoryTheory.Discrete.functor_map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.CommaMorphism.w` `Over.Hom.ext` `Over.homMk.congr_simp`
`instFullOverTopOverForget` 📖	mathematical	—	`CategoryTheory.Functor.Full` `Over` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `instCompleteBooleanAlgebra` `Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `IsMultiplicative.instTop` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `Over.forget`	—	`IsMultiplicative.instTop` `Comma.instFullTopCommaForget`
`instFullUnderTopUnderForget` 📖	mathematical	—	`CategoryTheory.Functor.Full` `Under` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `instCompleteBooleanAlgebra` `Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `IsMultiplicative.instTop` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `Under.forget`	—	`IsMultiplicative.instTop` `Comma.instFullTopCommaForget`
`instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `commaObj`	—	`commaObj_iff` `cancel_left_of_respectsIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Comma.instIsIsoLeft` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.CommaMorphism.w` `cancel_right_of_respectsIso` `CategoryTheory.Comma.instIsIsoRight`
`instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `CategoryTheory.CostructuredArrow` `CategoryTheory.instCategoryCostructuredArrow` `costructuredArrowObj`	—	`instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`
`instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `overObj`	—	`instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`
`instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `structuredArrowObj`	—	`instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`
`instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `underObj`	—	`instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso`
`overObj_iff` 📖	mathematical	—	`overObj` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	—
`over_eq_inverseImage` 📖	mathematical	—	`over` `inverseImage` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.forget`	—	—
`over_iff` 📖	mathematical	—	`over` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	—
`over_iso_iff` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	`comma_iso_iff`
`structuredArrowObj_iff` 📖	mathematical	—	`structuredArrowObj` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	—
`underObj_iff` 📖	mathematical	—	`underObj` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	—
`under_eq_inverseImage` 📖	mathematical	—	`under` `inverseImage` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.Under.forget`	—	—
`under_iff` 📖	mathematical	—	`under` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.CommaMorphism.right`	—	—

CategoryTheory.MorphismProperty.Comma

Definitions

Name	Category	Theorems
`changeProp` 📖	CompOp	2 math math: `instFaithfulChangeProp`, `instFullChangeProp`
`forget` 📖	CompOp	5 math math: `instFullTopCommaForget`, `forget_obj`, `forget_map`, `instFaithfulCommaForget`, `instReflectsIsomorphismsCommaForgetOfRespectsIso`
`forgetFullyFaithful` 📖	CompOp	—
`fullyFaithfulChangeProp` 📖	CompOp	—
`homFromCommaOfIsIso` 📖	CompOp	5 math math: `isoFromComma_hom`, `homFromCommaOfIsIso_hom`, `hom_homFromCommaOfIsIso`, `isoFromComma_inv`, `instIsIsoHomFromCommaOfIsIso`
`id` 📖	CompOp	2 math math: `id_left`, `id_right`
`instCategory` 📖	CompOp	104 math math: `CategoryTheory.MorphismProperty.Over.hasPullbacks`, `instFaithfulChangeProp`, `CategoryTheory.MorphismProperty.Over.instHasTerminalTopOfContainsIdentities`, `eqToHom_left`, `CategoryTheory.MorphismProperty.Over.map_obj_left`, `CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left`, `AlgebraicGeometry.Scheme.locallyCoverDense_of_le`, `comp_right`, `AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan`, `CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left`, `instFullChangeProp`, `CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app`, `CategoryTheory.MorphismProperty.Over.pullback_obj_left`, `CategoryTheory.MorphismProperty.Over.map_map_left`, `isoMk_hom_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap`, `comp_left_assoc`, `CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst`, `CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt`, `CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id`, `CategoryTheory.MorphismProperty.Over.map_comp`, `mapLeft_obj_hom`, `instFullTopCommaForget`, `isoFromComma_hom`, `CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopPullback`, `CategoryTheory.MorphismProperty.Over.isoMk_inv_left`, `CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app`, `CategoryTheory.MorphismProperty.Under.isoMk_inv_right`, `CategoryTheory.MorphismProperty.Over.mapId_inv_app_left`, `isoMk_hom_right`, `CategoryTheory.MorphismProperty.Under.isoMk_hom_right`, `CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left`, `isoMk_inv_left`, `mapRight_obj_left`, `CategoryTheory.MorphismProperty.Over.forget_comp_forget_map`, `CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app`, `lift_obj_toComma`, `comp_right_assoc`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f`, `mapLeft_map_right`, `AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology`, `CategoryTheory.MorphismProperty.instFullUnderTopUnderForget`, `CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong`, `mapLeft_obj_left`, `CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc`, `forget_obj`, `CategoryTheory.MorphismProperty.instFaithfulCostructuredArrowTopOverToOver`, `CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map`, `AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall`, `mapRight_obj_right`, `CategoryTheory.MorphismProperty.CostructuredArrow.toOver_obj`, `mapRight_map_right`, `forget_map`, `comp_left`, `id_hom`, `isoFromComma_inv`, `isoMk_inv_right`, `CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopOverForget`, `mapRight_map_left`, `CategoryTheory.MorphismProperty.Under.forget_comp_forget_map`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X`, `CategoryTheory.MorphismProperty.instFullOverTopOverForget`, `hasColimitsOfShape_of_closedUnderColimitsOfShape`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left`, `AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp`, `instFaithfulCommaForget`, `mapRight_obj_hom`, `hasColimit_of_closedUnderColimitsOfShape`, `AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology`, `CategoryTheory.MorphismProperty.Over.pullback_map_left`, `mapLeft_obj_right`, `AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget`, `inv_hom`, `instReflectsIsomorphismsCommaForgetOfRespectsIso`, `CategoryTheory.MorphismProperty.Over.pullback_obj_hom`, `CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left`, `instIsIsoHomFromCommaOfIsIso`, `CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver`, `AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology`, `CategoryTheory.MorphismProperty.Over.isoMk_hom_left`, `eqToHom_right`, `comp_hom`, `lift_map_hom`, `essentiallySmall_of_le`, `AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map`, `mapLeft_map_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj`, `AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology`, `CategoryTheory.MorphismProperty.Over.mapId_hom_app_left`, `CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst`, `hasLimitsOfShape_of_closedUnderLimitsOfShape`, `AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty`, `CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc`, `hasLimit_of_closedUnderLimitsOfShape`, `CategoryTheory.MorphismProperty.Over.map_obj_hom`, `CategoryTheory.MorphismProperty.instFaithfulUnderTopUnderForget`
`isoFromComma` 📖	CompOp	2 math math: `isoFromComma_hom`, `isoFromComma_inv`
`isoMk` 📖	CompOp	4 math math: `isoMk_hom_left`, `isoMk_hom_right`, `isoMk_inv_left`, `isoMk_inv_right`
`mapLeft` 📖	CompOp	5 math math: `mapLeft_obj_hom`, `mapLeft_map_right`, `mapLeft_obj_left`, `mapLeft_obj_right`, `mapLeft_map_left`
`mapRight` 📖	CompOp	5 math math: `mapRight_obj_left`, `mapRight_obj_right`, `mapRight_map_right`, `mapRight_map_left`, `mapRight_obj_hom`
`toComma` 📖	CompOp	81 math math: `Hom.ext_iff`, `eqToHom_left`, `CategoryTheory.MorphismProperty.Over.map_obj_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc`, `CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback`, `CategoryTheory.MorphismProperty.Under.mk_hom`, `comp_right`, `AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan`, `CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left`, `CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app`, `CategoryTheory.MorphismProperty.Over.mk_hom`, `CategoryTheory.MorphismProperty.Over.pullback_obj_left`, `CategoryTheory.MorphismProperty.Over.map_map_left`, `CategoryTheory.MorphismProperty.Over.Hom.ext_iff`, `comp_left_assoc`, `CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst`, `CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f`, `isoFromComma_hom`, `CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app`, `CategoryTheory.MorphismProperty.Over.mapId_inv_app_left`, `CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι`, `CategoryTheory.MorphismProperty.Over.forget_comp_forget_map`, `CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left`, `Hom.prop_hom_left`, `CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong`, `lift_obj_toComma`, `comp_right_assoc`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc`, `Hom.hom_right`, `ext_iff`, `CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left`, `CategoryTheory.MorphismProperty.Over.w_assoc`, `forget_obj`, `CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map`, `Hom.comp_left`, `CategoryTheory.MorphismProperty.CostructuredArrow.toOver_obj`, `CategoryTheory.MorphismProperty.Under.w`, `prop`, `CategoryTheory.MorphismProperty.Over.mk_left`, `CategoryTheory.MorphismProperty.CostructuredArrow.mk_left`, `CategoryTheory.MorphismProperty.Under.Hom.ext_iff`, `comp_left`, `id_hom`, `isoFromComma_inv`, `CategoryTheory.MorphismProperty.Under.mk_left`, `instIsIsoCommaHom`, `CategoryTheory.MorphismProperty.Under.forget_comp_forget_map`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X`, `CategoryTheory.MorphismProperty.Over.w`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left`, `CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext_iff`, `CategoryTheory.MorphismProperty.Over.pullback_map_left`, `inv_hom`, `Hom.hom_left`, `CategoryTheory.MorphismProperty.Over.pullback_obj_hom`, `CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left`, `CategoryTheory.MorphismProperty.Under.w_assoc`, `CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong`, `eqToHom_right`, `comp_hom`, `Hom.prop_hom_right`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj`, `AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology`, `CategoryTheory.MorphismProperty.Over.mapId_hom_app_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app`, `CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst`, `Hom.comp_right`, `id_left`, `CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc`, `CategoryTheory.MorphismProperty.CostructuredArrow.mk_hom`, `CategoryTheory.MorphismProperty.Over.map_obj_hom`, `id_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.Comma` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `toComma`	—	—
`comp_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `toComma` `Hom.toCommaMorphism` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.Comma` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Comma.left`	—	—
`comp_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.CommaMorphism.left` `Hom.toCommaMorphism` `CategoryTheory.MorphismProperty.Comma` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_left`
`comp_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `toComma` `Hom.toCommaMorphism` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.Comma` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Comma.right`	—	—
`comp_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right` `toComma` `CategoryTheory.CommaMorphism.right` `Hom.toCommaMorphism` `CategoryTheory.MorphismProperty.Comma` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_right`
`eqToHom_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `toComma` `Hom.toCommaMorphism` `CategoryTheory.eqToHom` `CategoryTheory.MorphismProperty.Comma` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Comma.left`	—	—
`eqToHom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `toComma` `Hom.toCommaMorphism` `CategoryTheory.eqToHom` `CategoryTheory.MorphismProperty.Comma` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Comma.right`	—	—
`ext` 📖	—	`CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.hom`	—	—	—
`ext_iff` 📖	mathematical	—	`CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.hom`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Comma` `instCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `forget` `Hom.hom`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Comma` `instCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `forget` `toComma`	—	—
`homFromCommaOfIsIso_hom` 📖	mathematical	—	`Hom.hom` `homFromCommaOfIsIso`	—	—
`hom_homFromCommaOfIsIso` 📖	mathematical	—	`homFromCommaOfIsIso` `Hom.hom`	—	—
`id_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.MorphismProperty.Comma` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `toComma`	—	—
`id_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `toComma` `Hom.toCommaMorphism` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left`	—	—
`id_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `toComma` `Hom.toCommaMorphism` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right`	—	—
`instFaithfulChangeProp` 📖	mathematical	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	`CategoryTheory.Functor.Faithful` `CategoryTheory.MorphismProperty.Comma` `instCategory` `changeProp`	—	`Hom.ext'`
`instFaithfulCommaForget` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.MorphismProperty.Comma` `instCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `forget`	—	`Hom.ext'`
`instFullChangeProp` 📖	mathematical	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	`CategoryTheory.Functor.Full` `CategoryTheory.MorphismProperty.Comma` `instCategory` `changeProp` `le_rfl`	—	`CategoryTheory.Functor.FullyFaithful.full` `le_rfl`
`instFullTopCommaForget` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.MorphismProperty.Comma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `forget`	—	`CategoryTheory.Functor.FullyFaithful.full` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`instIsIsoCommaHom` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `toComma` `Hom.hom`	—	`CategoryTheory.Functor.map_isIso`
`instIsIsoHomFromCommaOfIsIso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MorphismProperty.Comma` `instCategory` `homFromCommaOfIsIso`	—	`CategoryTheory.IsIso.inv_isIso` `Hom.ext'` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.IsIso.inv_hom_id`
`instReflectsIsomorphismsCommaForgetOfRespectsIso` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `CategoryTheory.MorphismProperty.Comma` `instCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `forget`	—	`hom_homFromCommaOfIsIso` `instIsIsoHomFromCommaOfIsIso`
`inv_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.inv` `CategoryTheory.MorphismProperty.Comma` `instCategory` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `toComma` `instIsIsoCommaHom`	—	`CategoryTheory.IsIso.eq_inv_of_hom_inv_id` `instIsIsoCommaHom` `comp_hom` `CategoryTheory.IsIso.hom_inv_id` `id_hom`
`isoFromComma_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.MorphismProperty.Comma` `instCategory` `isoFromComma` `homFromCommaOfIsIso` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `toComma`	—	—
`isoFromComma_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.MorphismProperty.Comma` `instCategory` `isoFromComma` `homFromCommaOfIsIso` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `toComma`	—	—
`isoMk_hom_left` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.left` `Hom.toCommaMorphism` `CategoryTheory.MorphismProperty.Comma` `instCategory` `isoMk`	—	—
`isoMk_hom_right` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.right` `Hom.toCommaMorphism` `CategoryTheory.MorphismProperty.Comma` `instCategory` `isoMk`	—	—
`isoMk_inv_left` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.left` `Hom.toCommaMorphism` `CategoryTheory.Iso.inv` `CategoryTheory.MorphismProperty.Comma` `instCategory` `isoMk`	—	—
`isoMk_inv_right` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.right` `Hom.toCommaMorphism` `CategoryTheory.Iso.inv` `CategoryTheory.MorphismProperty.Comma` `instCategory` `isoMk`	—	—
`lift_map_hom` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.map` `CategoryTheory.CommaMorphism.right`	`Hom.hom` `CategoryTheory.MorphismProperty.Comma` `instCategory` `lift`	—	—
`lift_obj_toComma` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `CategoryTheory.Comma` `CategoryTheory.commaCategory` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.map` `CategoryTheory.CommaMorphism.right`	`toComma` `CategoryTheory.MorphismProperty.Comma` `instCategory` `lift`	—	—
`mapLeft_map_left` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.left` `Hom.toCommaMorphism` `CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Comma` `instCategory` `mapLeft` `Hom.hom`	—	—
`mapLeft_map_right` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.right` `Hom.toCommaMorphism` `CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Comma` `instCategory` `mapLeft` `Hom.hom`	—	—
`mapLeft_obj_hom` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Comma.hom`	`CategoryTheory.MorphismProperty.Comma` `instCategory` `mapLeft`	—	—
`mapLeft_obj_left` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Comma.hom`	`CategoryTheory.MorphismProperty.Comma` `instCategory` `mapLeft`	—	—
`mapLeft_obj_right` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Comma.hom`	`CategoryTheory.MorphismProperty.Comma` `instCategory` `mapLeft`	—	—
`mapRight_map_left` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.NatTrans.app`	`CategoryTheory.CommaMorphism.left` `Hom.toCommaMorphism` `CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Comma` `instCategory` `mapRight` `Hom.hom`	—	—
`mapRight_map_right` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.NatTrans.app`	`CategoryTheory.CommaMorphism.right` `Hom.toCommaMorphism` `CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Comma` `instCategory` `mapRight` `Hom.hom`	—	—
`mapRight_obj_hom` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.NatTrans.app`	`CategoryTheory.MorphismProperty.Comma` `instCategory` `mapRight`	—	—
`mapRight_obj_left` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.NatTrans.app`	`CategoryTheory.MorphismProperty.Comma` `instCategory` `mapRight`	—	—
`mapRight_obj_right` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.hom` `CategoryTheory.NatTrans.app`	`CategoryTheory.MorphismProperty.Comma` `instCategory` `mapRight`	—	—
`prop` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `toComma` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	—
`toCommaMorphism_eq_hom` 📖	mathematical	—	`Hom.toCommaMorphism` `Hom.hom`	—	—

CategoryTheory.MorphismProperty.Comma.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	2 math math: `comp_left`, `comp_right`
`hom` 📖	CompOp	22 math math: `CategoryTheory.MorphismProperty.Over.map_map_left`, `hom_mk`, `CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso_hom`, `CategoryTheory.MorphismProperty.Comma.hom_homFromCommaOfIsIso`, `CategoryTheory.MorphismProperty.Under.homMk_hom`, `CategoryTheory.MorphismProperty.Comma.mapLeft_map_right`, `hom_right`, `CategoryTheory.MorphismProperty.Comma.toCommaMorphism_eq_hom`, `CategoryTheory.MorphismProperty.Under.Hom.mk_hom`, `ext'_iff`, `CategoryTheory.MorphismProperty.Comma.mapRight_map_right`, `CategoryTheory.MorphismProperty.Comma.forget_map`, `CategoryTheory.MorphismProperty.Over.homMk_hom`, `CategoryTheory.MorphismProperty.Comma.id_hom`, `CategoryTheory.MorphismProperty.Comma.instIsIsoCommaHom`, `CategoryTheory.MorphismProperty.Comma.mapRight_map_left`, `CategoryTheory.MorphismProperty.Comma.inv_hom`, `hom_left`, `CategoryTheory.MorphismProperty.Comma.comp_hom`, `CategoryTheory.MorphismProperty.Comma.lift_map_hom`, `CategoryTheory.MorphismProperty.Comma.mapLeft_map_left`, `CategoryTheory.MorphismProperty.Over.Hom.mk_hom`
`toCommaMorphism` 📖	CompOp	65 math math: `ext_iff`, `CategoryTheory.MorphismProperty.Comma.eqToHom_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc`, `CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback`, `CategoryTheory.MorphismProperty.Comma.comp_right`, `AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan`, `CategoryTheory.MorphismProperty.CostructuredArrow.homMk_left`, `CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left`, `CategoryTheory.MorphismProperty.Over.map_map_left`, `CategoryTheory.MorphismProperty.Comma.isoMk_hom_left`, `CategoryTheory.MorphismProperty.Over.Hom.ext_iff`, `CategoryTheory.MorphismProperty.Comma.comp_left_assoc`, `CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f`, `CategoryTheory.MorphismProperty.Over.isoMk_inv_left`, `CategoryTheory.MorphismProperty.Under.isoMk_inv_right`, `CategoryTheory.MorphismProperty.Over.mapId_inv_app_left`, `CategoryTheory.MorphismProperty.Comma.isoMk_hom_right`, `CategoryTheory.MorphismProperty.Under.isoMk_hom_right`, `CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left`, `CategoryTheory.MorphismProperty.Comma.isoMk_inv_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι`, `CategoryTheory.MorphismProperty.Over.forget_comp_forget_map`, `CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left`, `prop_hom_left`, `CategoryTheory.MorphismProperty.Comma.comp_right_assoc`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f`, `CategoryTheory.MorphismProperty.Comma.mapLeft_map_right`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc`, `hom_right`, `CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left`, `CategoryTheory.MorphismProperty.Over.w_assoc`, `CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map`, `CategoryTheory.MorphismProperty.Comma.toCommaMorphism_eq_hom`, `comp_left`, `CategoryTheory.MorphismProperty.Under.w`, `CategoryTheory.MorphismProperty.Comma.mapRight_map_right`, `CategoryTheory.MorphismProperty.Under.Hom.ext_iff`, `CategoryTheory.MorphismProperty.Comma.comp_left`, `CategoryTheory.MorphismProperty.Comma.isoMk_inv_right`, `CategoryTheory.MorphismProperty.Comma.mapRight_map_left`, `CategoryTheory.MorphismProperty.Under.forget_comp_forget_map`, `CategoryTheory.MorphismProperty.Over.w`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left`, `CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext_iff`, `CategoryTheory.MorphismProperty.Over.pullback_map_left`, `hom_left`, `CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left`, `CategoryTheory.MorphismProperty.Under.w_assoc`, `CategoryTheory.MorphismProperty.Over.isoMk_hom_left`, `CategoryTheory.MorphismProperty.Comma.eqToHom_right`, `prop_hom_right`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map`, `CategoryTheory.MorphismProperty.Comma.mapLeft_map_left`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd`, `AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst`, `AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology`, `CategoryTheory.MorphismProperty.Over.mapId_hom_app_left`, `CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst`, `comp_right`, `CategoryTheory.MorphismProperty.Comma.id_left`, `CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc`, `CategoryTheory.MorphismProperty.Comma.id_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.toComma` `toCommaMorphism` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left`	—	—
`comp_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.MorphismProperty.Comma.toComma` `toCommaMorphism` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right`	—	—
`ext` 📖	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.toComma` `toCommaMorphism` `CategoryTheory.CommaMorphism.right`	—	—	—
`ext'` 📖	—	`hom`	—	—	`ext`
`ext'_iff` 📖	mathematical	—	`hom`	—	`ext'`
`ext_iff` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.toComma` `toCommaMorphism` `CategoryTheory.CommaMorphism.right`	—	`ext`
`hom_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.toComma` `hom` `toCommaMorphism`	—	—
`hom_mk` 📖	mathematical	`CategoryTheory.Comma.left` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Comma.right` `CategoryTheory.CommaMorphism.right`	`hom`	—	—
`hom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.MorphismProperty.Comma.toComma` `hom` `toCommaMorphism`	—	—
`prop_hom_left` 📖	mathematical	—	`CategoryTheory.Comma.left` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.CommaMorphism.left` `toCommaMorphism`	—	—
`prop_hom_right` 📖	mathematical	—	`CategoryTheory.Comma.right` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.CommaMorphism.right` `toCommaMorphism`	—	—

CategoryTheory.MorphismProperty.Comma.Hom.Simps

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	—

CategoryTheory.MorphismProperty.CostructuredArrow

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	—
`homMk` 📖	CompOp	1 math math: `homMk_left`
`mk` 📖	CompOp	—
`toOver` 📖	CompOp	4 math math: `CategoryTheory.MorphismProperty.instFaithfulCostructuredArrowTopOverToOver`, `toOver_map`, `toOver_obj`, `CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homMk_left` 📖	mathematical	`CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `homMk`	—	—
`mk_hom` 📖	mathematical	`CategoryTheory.Functor.obj`	`CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`mk_left` 📖	mathematical	`CategoryTheory.Functor.obj`	`CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`toOver_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.CostructuredArrow` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.Functor.id` `toOver` `CategoryTheory.MorphismProperty.Over.homMk` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.Comma.hom` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`toOver_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.CostructuredArrow` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.Functor.id` `toOver` `CategoryTheory.Comma.left` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.Comma.hom`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`

CategoryTheory.MorphismProperty.CostructuredArrow.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Comma.Hom.ext'` `CategoryTheory.Comma.hom_ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `ext`

CategoryTheory.MorphismProperty.HasFactorization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`over` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFactorization` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.MorphismProperty.over`	—	`CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc` `CategoryTheory.Over.w` `CategoryTheory.Over.OverMorphism.ext` `CategoryTheory.MorphismProperty.MapFactorizationData.fac` `CategoryTheory.MorphismProperty.MapFactorizationData.hi` `CategoryTheory.MorphismProperty.MapFactorizationData.hp`

CategoryTheory.MorphismProperty.Over

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	10 math math: `AlgebraicGeometry.Scheme.locallyCoverDense_of_le`, `CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget`, `forget_comp_forget_map`, `AlgebraicGeometry.instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget`, `instPreservesFiniteLimitsTopOverForget`, `CategoryTheory.MorphismProperty.instFullOverTopOverForget`, `AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology`, `AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget`, `AlgebraicGeometry.instPreservesColimitOverSchemeTopMorphismPropertyOverForget`, `AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit`
`homMk` 📖	CompOp	5 math math: `pullbackMapHomPullback_app`, `mapPullbackAdj_counit_app`, `mapPullbackAdj_unit_app`, `CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map`, `homMk_hom`
`isoMk` 📖	CompOp	2 math math: `isoMk_inv_left`, `isoMk_hom_left`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_comp_forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Functor.comp` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `forget` `CategoryTheory.Over.forget` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`homMk_hom` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Comma.hom`	`CategoryTheory.MorphismProperty.Comma.Hom.hom` `homMk` `CategoryTheory.Over.homMk`	—	—
`isoMk_hom_left` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `isoMk`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`isoMk_inv_left` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Comma.hom`	`CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Iso.inv` `CategoryTheory.MorphismProperty.Over` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `isoMk`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`mk_hom` 📖	mathematical	—	`CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`mk_left` 📖	mathematical	—	`CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Comma.hom`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Over.w`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.CommaMorphism.left` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

CategoryTheory.MorphismProperty.Over.Hom

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Comma.Hom.ext'` `CategoryTheory.Comma.hom_ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `ext`
`mk_hom` 📖	mathematical	`CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.CommaMorphism.left`	`CategoryTheory.MorphismProperty.Comma.Hom.hom`	—	—

CategoryTheory.MorphismProperty.Under

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	3 math math: `CategoryTheory.MorphismProperty.instFullUnderTopUnderForget`, `forget_comp_forget_map`, `CategoryTheory.MorphismProperty.instFaithfulUnderTopUnderForget`
`homMk` 📖	CompOp	1 math math: `homMk_hom`
`isoMk` 📖	CompOp	2 math math: `isoMk_inv_right`, `isoMk_hom_right`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_comp_forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Under` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Functor.comp` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `forget` `CategoryTheory.Under.forget` `CategoryTheory.CommaMorphism.right` `CategoryTheory.MorphismProperty.Comma.toComma` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`homMk_hom` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Comma.hom`	`CategoryTheory.MorphismProperty.Comma.Hom.hom` `homMk` `CategoryTheory.Under.homMk`	—	—
`isoMk_hom_right` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Comma.hom` `CategoryTheory.Iso.hom`	`CategoryTheory.CommaMorphism.right` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.MorphismProperty.Under` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `isoMk`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`isoMk_inv_right` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Comma.right` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Comma.hom` `CategoryTheory.Iso.hom`	`CategoryTheory.CommaMorphism.right` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism` `CategoryTheory.Iso.inv` `CategoryTheory.MorphismProperty.Under` `CategoryTheory.MorphismProperty.Comma.instCategory` `CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `isoMk`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop`
`mk_hom` 📖	mathematical	—	`CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`mk_left` 📖	mathematical	—	`CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom` `CategoryTheory.CommaMorphism.right` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Under.w`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom` `CategoryTheory.CommaMorphism.right` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

CategoryTheory.MorphismProperty.Under.Hom

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Comma.Hom.ext'` `CategoryTheory.Comma.hom_ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `ext`
`mk_hom` 📖	mathematical	`CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.MorphismProperty.Comma.toComma` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.CommaMorphism.right`	`CategoryTheory.MorphismProperty.Comma.Hom.hom`	—	—

---

← Back to Index