Basic

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

Statistics

Metric	Count
Definitions Respects, RespectsIso, RespectsLeft, RespectsRight, arrow, epimorphisms, functorCategory, homFamily, instCompleteBooleanAlgebra, instInhabited, inverseImage, isoClosure, isomorphisms, map, monomorphisms, ofHoms, op, pi, prod, strictMap, toSet, unop	22
Theorems toRespectsLeft, toRespectsRight, epimorphisms, inverseImage, isomorphisms, mk, monomorphisms, of_respects_arrow_iso, op, postcomp, precomp, unop, inf, precomp, inf, postcomp, arrow_iso_iff, arrow_mk_iso_iff, arrow_mk_mem_toSet_iff, cancel_left_of_respectsIso, cancel_right_of_respectsIso, comma_iso_iff, iff, infer_property, ext, ext_iff, homFamily_apply, homFamily_arrow_mk, iSup_iff, inf, instRespectsIsoTop, instRespectsLeftOppositeOpOfRespectsRight, instRespectsOfRespectsLeftOfRespectsRight, instRespectsRightOppositeOpOfRespectsLeft, inverseImage_equivalence_functor_eq_map_inverse, inverseImage_equivalence_inverse_eq_map_functor, inverseImage_iff, inverseImage_map_eq_of_isEquivalence, isoClosure_eq_iff, isoClosure_eq_self, isoClosure_isoClosure, isoClosure_le_iff, isoClosure_respectsIso, iff, infer_property, isomorphisms_op, le_def, le_isoClosure, map_eq_of_iso, map_id, map_id_eq_isoClosure, map_inverseImage_eq_of_isEquivalence, map_inverseImage_le, map_isoClosure, map_le_iff, map_map, map_mem_map, map_mem_strictMap, map_respectsIso, map_top_eq_top_of_essSurj_of_full, mem_toSet_iff, iff, infer_property, monotone_isoClosure, monotone_map, ofHoms_homFamily, ofHoms_iff, of_eq, of_eq_top, op_inverseImage, op_isomorphisms, op_unop, sSup_iff, toSet_iSup, toSet_max, top_apply, top_eq, unop_op, isIso_app_iff_of_iso	79
Total	101

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
Respects 📖	CompData	7 math math: IsLocalAtTarget.toRespects, instRespectsOfRespectsLeftOfRespectsRight, AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion, AlgebraicGeometry.instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion, instRespectsOfIsStableUnderComposition, AlgebraicGeometry.instRespectsSchemeSmoothIsOpenImmersion, IsLocalAtSource.toRespects
RespectsIso 📖	MathDef	71 math math: instRespectsIsoInd, relative_respectsIso, AlgebraicGeometry.IsDominant.respectsIso, CategoryTheory.ObjectProperty.instRespectsIsoIsColocal, HomotopyCategory.respectsIso_quasiIso, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso, instRespectsIsoPullbacks, AlgebraicGeometry.affineAnd_respectsIso, RespectsIso.unop, RespectsIso.monomorphisms, TopCat.instRespectsIsoIsOpenEmbedding, RespectsIso.op, CategoryTheory.Functor.relativelyRepresentable.respectsIso, HomologicalComplex.instRespectsIsoQuasiIso, instRespectsIsoTop, AlgebraicGeometry.IsClosedImmersion.respectsIso, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenEmbedding, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedEmbedding, AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk, RespectsIso.diagonal, AlgebraicGeometry.affineLocally_respectsIso, AlgebraicGeometry.specializingMap_respectsIso, HomotopicalAlgebra.instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition, AlgebraicGeometry.sourceLocalClosure.instRespectsIsoScheme, bijective_respectsIso, AlgebraicGeometry.instRespectsIsoSchemeSurjective, instRespectsIsoColimitsOfShape, RespectsIso.of_respects_arrow_iso, AlgebraicGeometry.UniversallyInjective.respectsIso, AlgebraicGeometry.stalkwise_respectsIso, AlgebraicGeometry.isOpenImmersion_respectsIso, RespectsIso.mk, isoClosure_eq_iff, instRespectsIsoTransfiniteCompositionsOfShape, map_respectsIso, IsStableUnderBaseChange.respectsIso, CategoryTheory.ObjectProperty.instRespectsIsoTrW, AlgebraicGeometry.sourceAffineLocally_respectsIso, AlgebraicGeometry.HasAffineProperty.instRespectsIsoScheme, inf, injective_respectsIso, RespectsIso.isomorphisms, IsStableUnderCobaseChange.respectsIso, CategoryTheory.NatTrans.instRespectsIsoFunctorCoequifibered, AlgebraicGeometry.topologically_respectsIso, RespectsIso.epimorphisms, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyInjective, RingHom.toMorphismProperty_respectsIso_iff, AlgebraicGeometry.instRespectsIsoSchemeTargetAffineLocallyOfToProperty, universally_respectsIso, surjective_respectsIso, respectsIso_of_isStableUnderComposition, instRespectsIsoPushouts, instRespectsIsoLimitsOfShape, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap, regularEpi.respectsIso, AlgebraicGeometry.IsSeparated.instRespectsIsoScheme, AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_of, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyGeneralizingMap, instRespectsIsoOfIsStableUnderRetracts, RespectsIso.inverseImage, isoClosure_respectsIso, CategoryTheory.ObjectProperty.instRespectsIsoIsLocal, AlgebraicGeometry.universallyClosed_respectsIso, AlgebraicGeometry.UniversallyOpen.instRespectsIsoScheme, CategoryTheory.NatTrans.instRespectsIsoFunctorEquifibered, AlgebraicGeometry.IsProper.instRespectsIsoScheme, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsEmbedding, regularMono.respectsIso, AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso
RespectsLeft 📖	CompData	7 math math: instRespectsLeftInd, AlgebraicGeometry.IsLocalAtSource.respectsLeft_isOpenImmersion, RespectsLeft.inf, AlgebraicGeometry.IsZariskiLocalAtSource.respectsLeft_isOpenImmersion, AlgebraicGeometry.sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange, Respects.toRespectsLeft, instRespectsLeftOppositeOpOfRespectsRight
RespectsRight 📖	CompData	4 math math: RespectsRight.inf, instRespectsRightOppositeOpOfRespectsLeft, AlgebraicGeometry.sourceLocalClosure.instRespectsRightScheme, Respects.toRespectsRight
arrow 📖	CompOp	4 math math: CategoryTheory.LocalizerMorphism.hasRightResolutions_arrow_of_functorial_resolutions, CategoryTheory.LocalizerMorphism.arrow_functor, HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism
epimorphisms 📖	CompOp	15 math math: IsStableUnderCobaseChange.hasOfPrecompProperty_epimorphisms, CategoryTheory.projective_iff_llp_epimorphisms_of_isZero, CategoryTheory.Abelian.instIsStableUnderBaseChangeEpimorphisms, CategoryTheory.projective_iff_llp_epimorphisms_zero, IsStableUnderRetracts.epimorphisms, epimorphisms.iff, CategoryTheory.ObjectProperty.epimorphisms_le_epiModSerre, functorCategory_epimorphisms, CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms_iff, RespectsIso.epimorphisms, CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms, IsStableUnderCobaseChange.epimorphisms, epimorphisms.infer_property, IsMultiplicative.instEpimorphisms, CategoryTheory.ConcreteCategory.surjective_le_epimorphisms
functorCategory 📖	CompOp	15 math math: instIsStableUnderTransfiniteCompositionOfShapeFunctorFunctorCategoryOfHasIterationOfShape, CategoryTheory.Functor.IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities, functorCategory_isomorphisms, IsStableUnderColimitsOfShape.functorCategory, instHasFunctorialFactorizationFunctorFunctorCategory, CategoryTheory.SmallObject.succStruct_prop_le_propArrow, functorCategory_monomorphisms, functorCategory_epimorphisms, instIsStableUnderBaseChangeFunctorFunctorCategoryOfHasPullbacks, IsStableUnderLimitsOfShape.functorCategory, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_unit, CategoryTheory.Localization.HasProductsOfShapeAux.inverts, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_counit, instIsStableUnderRetractsFunctorFunctorCategory, instIsStableUnderCobaseChangeFunctorFunctorCategoryOfHasPushouts
homFamily 📖	CompOp	11 math math: CategoryTheory.SmallObject.ιFunctorObj_eq, ofHoms_homFamily, homFamily_arrow_mk, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left, CategoryTheory.SmallObject.πFunctorObj_eq, IsCardinalForSmallObjectArgument.preservesColimit, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, CategoryTheory.SmallObject.preservesColimit, CategoryTheory.SmallObject.hasColimitsOfShape_discrete, homFamily_apply
instCompleteBooleanAlgebra 📖	CompOp	282 math math: AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', homotopyEquivalences_le_quasiIso, SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, isomorphisms_le_of_containsIdentities, comp_eq_top_iff, isStableUnderLimitsOfShape_iff_limitsOfShape_le, hasOfPostcompProperty_iff_le_diagonal, universally_inf, SSet.modelCategoryQuillen.I_le_monomorphisms, AlgebraicGeometry.HasAffineProperty.affineAnd_le_affineAnd, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W, DescendsAlong.top, Over.hasPullbacks, HasCardinalLT.iSup, Over.instHasTerminalTopOfContainsIdentities, ContainsIdentities.inf, Over.map_obj_left, Over.pullbackComp_hom_app_left, pushouts_le, Under.mk_hom, CategoryTheory.Localization.LeftBousfield.galoisConnection, CategoryTheory.ObjectProperty.isomorphisms_le_isoModSerre, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, AlgebraicGeometry.isImmersion_eq_inf, colimitsOfShape_le_coproducts, IsInvertedBy.iff_map_le_isomorphisms, AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, Over.mapCongr_inv_app_left, monotone_map, transfiniteCompositionsOfShape_le_transfiniteCompositions, AlgebraicGeometry.IsSeparated.eq_valuativeCriterion, AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms, IsMultiplicative.instTop, Over.pullbackMapHomPullback_app, IsMultiplicative.inf, colimitsOfShape_le, IsLocalAtSource.inf, Over.mk_hom, Over.pullback_obj_left, Over.map_map_left, SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk, CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms, transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, coproducts_monotone, CategoryTheory.Localization.Construction.morphismProperty_eq_top', Over.Hom.ext_iff, HomotopicalAlgebra.trivialCofibrations_sub_cofibrations, colimitsOfShape_discrete_le_llp_rlp, Over.pullbackCongr_hom_app_left_fst, Over.mapPullbackAdj_counit_app, isStableUnderRetracts_iff_retracts_le, multiplicativeClosure_monotone, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, CategoryTheory.Functor.relativelyRepresentable.isomorphisms_le, DescendsAlong.inf, CodescendsAlong.inf, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, retracts_le, instRespectsIsoTop, IsStableUnderBaseChange.inf, instFaithfulOverTopOverForget, IsLocalAtSource.top, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, Over.map_comp, AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, Comma.instFullTopCommaForget, HomotopicalAlgebra.trivialCofibrations_sub_weakEquivalences, AlgebraicGeometry.HasAffineProperty.affineAnd_eq_of_propertyIsLocal, CategoryTheory.Localization.LeftBousfield.le_W_iff, le_ind, AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, transfiniteCompositionsOfShape_le, HomotopicalAlgebra.trivialFibrations_sub_fibrations, AlgebraicGeometry.IsFinite.eq_proper_inf_locallyQuasiFinite, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms, Over.instPreservesFiniteLimitsTopPullback, CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk, transfiniteCompositionsOfShape_monotone, isStableUnderCobaseChange_iff_pushouts_le, Over.mapPullbackAdj_unit_app, universally_le, CategoryTheory.GrothendieckTopology.PreservesSheafification.le, AlgebraicGeometry.IsLocalIso.eq_iInf, AlgebraicGeometry.topologically_iso_le, Over.mapId_inv_app_left, SSet.Truncated.liftOfStrictSegal.naturalityProperty_eq_top, AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty, le_pushouts, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_W, Over.mapCongr_hom_app_left, IsLocalAtTarget.top, strictMap_multiplicativeClosure_le, CategoryTheory.SmallObject.succStruct_prop_le_propArrow, isoClosure_le_iff, instIsStableUnderCobaseChangeTop, Over.forget_comp_forget_map, Over.pullbackComp_inv_app_left, coproducts_le_iff, instHasPullbackHomDiscretePUnitOfHasPullbacksAlong, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, CategoryTheory.ObjectProperty.galoisConnection_isColocal, map_inverseImage_le, le_isLocal_isLocal, gc_llp_rlp, SimplexCategory.Truncated.morphismProperty_eq_top, HomotopicalAlgebra.trivialFibrations_sub_weakEquivalences, instHasOfPrecompPropertyTop, HasCardinalLT.sup, instIsStableUnderRetractsMin, retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, iSup_iff, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, map_le_iff, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, CategoryTheory.ObjectProperty.le_isLocal_iff, le_coproducts, RespectsLeft.inf, instFullUnderTopUnderForget, CategoryTheory.Paths.morphismProperty_eq_top', CategoryTheory.Localization.Construction.morphismProperty_is_top', instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, Over.mapComp_hom_app_left, le_pullbacks, CategoryTheory.ObjectProperty.epimorphisms_le_epiModSerre, antitone_rlp, bijective_eq_sup, IsStableUnderTransfiniteCompositionOfShape.le, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, instIsStableUnderBaseChangeTop, Over.w_assoc, le_llp_rlp, AlgebraicGeometry.HasRingHomProperty.inf, CategoryTheory.Localization.Construction.morphismProperty_eq_top, instHasOfPostcompPropertyTop, le_llp_iff_le_rlp, coproducts_le, CategoryTheory.ObjectProperty.le_isColocal_iff, instFaithfulCostructuredArrowTopOverToOver, AlgebraicGeometry.isOpenImmersion_eq_inf, CostructuredArrow.toOver_map, AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall, le_retracts, instHasOfPrecompPropertyMin, AlgebraicGeometry.IsClosedImmersion.eq_inf, CategoryTheory.ObjectProperty.monomorphisms_le_monoModSerre, CostructuredArrow.toOver_obj, Under.w, pretopology_inf, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, inf, RespectsRight.inf, coproducts_le_llp_rlp, Over.mk_left, AlgebraicGeometry.isPreimmersion_eq_inf, CostructuredArrow.mk_left, AlgebraicGeometry.isProper_eq, Under.Hom.ext_iff, limitsOfShape_le, Under.mk_left, retracts_le_iff, AlgebraicGeometry.universallyClosed_eq_universallySpecializing, transfiniteCompositionsOfShape_le_llp_rlp, Over.instPreservesFiniteLimitsTopOverForget, AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, AlgebraicGeometry.IsProper.eq_valuativeCriterion, Under.forget_comp_forget_map, IsInvertedBy.iff_le_inverseImage_isomorphisms, AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, instFullOverTopOverForget, isomorphisms_le_pushouts, Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape, Over.w, IsStableUnderComposition.inf, AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, le_leftBousfieldW_isLocal, AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, CodescendsAlong.top, colimitsOfShape_le_of_final, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, CategoryTheory.LocalizerMorphism.map, AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective, instHasOfPostcompPropertyMin, CategoryTheory.Cat.FreeRefl.morphismProperty_eq_top, CategoryTheory.Paths.morphismProperty_eq_top_of_isMultiplicative, transfiniteCompositions_le, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, Comma.hasColimit_of_closedUnderColimitsOfShape, AlgebraicGeometry.geometrically_inf, CostructuredArrow.Hom.ext_iff, AlgebraicGeometry.IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty, retracts_le_llp_rlp, AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology, Over.pullback_map_left, AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom, antitone_llp, AlgebraicGeometry.targetAffineLocally_affineAnd_le, sSup_iff, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, SSet.modelCategoryQuillen.J_le_monomorphisms, isStableUnderTransfiniteCompositionOfShape_iff, Over.pullback_obj_hom, CategoryTheory.FreeGroupoid.instIsLocalizationOfTopMorphismProperty, instHasTwoOutOfThreePropertyTop, le_isColocal_isColocal, Over.mapComp_inv_app_left, CategoryTheory.Localization.morphismProperty_eq_top, Under.w_assoc, instFullCostructuredArrowTopOverToOver, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, map_top_eq_top_of_essSurj_of_full, instHasTwoOutOfThreePropertyMin, instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, precoverage_inf, AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom, IsStableUnderCobaseChange.inf, monotone_isoClosure, AlgebraicGeometry.isomorphisms_eq_stalkwise, transfiniteCompositions_pushouts_coproducts_le_llp_rlp, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms, le_def, AlgebraicGeometry.IsFinite.eq_inf, pushouts_le_llp_rlp, AlgebraicGeometry.affineLocally_le, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W, isStableUnderColimitsOfShape_iff_colimitsOfShape_le, toSet_max, le_isoClosure, CategoryTheory.ObjectProperty.galoisConnection_isLocal, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, pullbacks_monotone, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, universally_mono, presheaf_monomorphisms_le_monomorphisms, pushouts_le_iff, isStableUnderBaseChange_iff_pullbacks_le, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W, AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom, pullbacks_le, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, CategoryTheory.ConcreteCategory.injective_le_monomorphisms, pushouts_monotone, le_colimitsOfShape_punit, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, retracts_monotone, Over.mapId_hom_app_left, Over.pullbackComp_left_fst_fst, CategoryTheory.ConcreteCategory.surjective_le_epimorphisms, IsLocalAtTarget.inf, Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape, CategoryTheory.isGroupoid_iff_isomorphisms_eq_top, le_multiplicativeClosure, CategoryTheory.Localization.instIsGroupoidLocalizationTopMorphismProperty, top_apply, AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty, CategoryTheory.Localization.Construction.morphismProperty_is_top, AlgebraicGeometry.ValuativeCriterion.eq, SSet.Truncated.HomotopyCategory.morphismProperty_eq_top, transfiniteCompositions_monotone, top_eq, Over.pullbackCongr_hom_app_left_fst_assoc, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_W, transfiniteCompositions_le_llp_rlp, AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, CostructuredArrow.mk_hom, CategoryTheory.Paths.morphismProperty_eq_top, Comma.hasLimit_of_closedUnderLimitsOfShape, AlgebraicGeometry.sourceLocalClosure.le, Over.map_obj_hom, AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, instFaithfulUnderTopUnderForget, multiplicativeClosure_le_iff, le_transfiniteCompositions, toSet_iSup, transfiniteCompositions_le_iff, SimplexCategory.morphismProperty_eq_top
instInhabited 📖	CompOp	—
inverseImage 📖	CompOp	40 math math: inverseImage_equivalence_inverse_eq_map_functor, over_eq_inverseImage, CategoryTheory.Adjunction.hasLeftCalculusOfFractions', instIsMonoidalInverseImageOfMonoidalOfRespectsIso, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms, IsMultiplicative.instInverseImage, CategoryTheory.ObjectProperty.isColocal_eq_inverseImage_isomorphisms, IsStableUnderComposition.inverseImage, CategoryTheory.Adjunction.isLocalization_rightAdjoint', CategoryTheory.Localization.LeftBousfield.W_eq_inverseImage_isomorphisms, inverseImage_map_eq_of_isEquivalence, CategoryTheory.Adjunction.isLocalization_leftAdjoint', CategoryTheory.GrothendieckTopology.PreservesSheafification.le, under_eq_inverseImage, CategoryTheory.Adjunction.isLocalization, CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft, map_inverseImage_le, comap_precoverage, eq_inverseImage_quotientFunctor, instIsStableUnderRetractsInverseImage, map_le_iff, op_inverseImage, CategoryTheory.Adjunction.isLocalization', IsInvertedBy.iff_le_inverseImage_isomorphisms, CategoryTheory.LocalizerMorphism.map, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_unit, ContainsIdentities.inverseImage, IsCompatibleWithShift.condition, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction, inverseImage_iff, TransfiniteCompositionOfShape.map_toTransfiniteCompositionOfShape, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_counit, CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms, CategoryTheory.Adjunction.hasRightCalculusOfFractions', inverseImage_equivalence_functor_eq_map_inverse, AlgebraicGeometry.isomorphisms_eq_stalkwise, RespectsIso.inverseImage, map_inverseImage_eq_of_isEquivalence, CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms, instHasTwoOutOfThreePropertyInverseImage
isoClosure 📖	CompOp	11 math math: map_isoClosure, isoClosure_le_iff, map_inverseImage_le, isoClosure_eq_iff, IsInvertedBy.isoClosure_iff, isoClosure_isoClosure, monotone_isoClosure, le_isoClosure, isoClosure_respectsIso, isoClosure_eq_self, map_id_eq_isoClosure
isomorphisms 📖	CompOp	53 math math: CategoryTheory.ObjectProperty.InheritedFromSource.instIsomorphismsOfIsClosedUnderIsomorphisms, CategoryTheory.Adjunction.hasLeftCalculusOfFractions', isomorphisms_le_of_containsIdentities, IsLocalAtTarget.toRespects, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms, IsStableUnderCobaseChange.isomorphisms, CategoryTheory.ObjectProperty.isomorphisms_le_isoModSerre, isomorphisms.iff, IsInvertedBy.iff_map_le_isomorphisms, AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, IsStableUnderBaseChange.isomorphisms, CategoryTheory.ObjectProperty.isColocal_eq_inverseImage_isomorphisms, functorCategory_isomorphisms, CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms, CategoryTheory.Adjunction.isLocalization_rightAdjoint', CategoryTheory.Localization.LeftBousfield.W_eq_inverseImage_isomorphisms, op_isomorphisms, CategoryTheory.Functor.relativelyRepresentable.isomorphisms_le, CategoryTheory.Adjunction.isLocalization_leftAdjoint', AlgebraicGeometry.topologically_iso_le, TransfiniteCompositionOfShape.instIsIsoAppIncl, CategoryTheory.Adjunction.isLocalization, instHasTwoOutOfThreePropertyIsomorphisms, IsStableUnderColimitsOfShape.isomorphisms, CategoryTheory.ObjectProperty.InheritedFromTarget.instIsomorphismsOfIsClosedUnderIsomorphisms, instIsStableUnderFilteredColimitsIsomorphisms, TransfiniteCompositionOfShape.instIsIsoMapF, RespectsIso.isomorphisms, CategoryTheory.Adjunction.isLocalization', CategoryTheory.Precoverage.ZeroHypercover.instIsLocalAtTargetIsomorphisms, isomorphisms.infer_property, IsStableUnderRetracts.isomorphisms, IsInvertedBy.iff_le_inverseImage_isomorphisms, isomorphisms_le_pushouts, AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_unit, instHasOfPostcompPropertyIsomorphismsOfRespectsIso, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right, CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_counit, AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage, CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms, CategoryTheory.Adjunction.hasRightCalculusOfFractions', AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, diagonal_isomorphisms, instHasOfPrecompPropertyIsomorphismsOfRespectsIso, AlgebraicGeometry.isomorphisms_eq_stalkwise, IsMultiplicative.instIsomorphisms, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right_assoc, IsLocalAtSource.toRespects, CategoryTheory.isGroupoid_iff_isomorphisms_eq_top, CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms, isomorphisms_op
map 📖	CompOp	18 math math: inverseImage_equivalence_inverse_eq_map_functor, map_id, IsInvertedBy.iff_map_le_isomorphisms, monotone_map, map_map, inverseImage_map_eq_of_isEquivalence, map_isoClosure, HomotopyCategory.quasiIso_eq_quasiIso_map_quotient, map_eq_of_iso, map_inverseImage_le, map_le_iff, map_respectsIso, inverseImage_equivalence_functor_eq_map_inverse, map_top_eq_top_of_essSurj_of_full, map_mem_map, map_id_eq_isoClosure, IsInvertedBy.map_iff, map_inverseImage_eq_of_isEquivalence
monomorphisms 📖	CompOp	44 math math: CategoryTheory.IsGrothendieckAbelian.instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp, instIsStableUnderTransfiniteCompositionOfShapeFunctorMonomorphismsOfHasPullbacksOfHasIterationOfShape, SSet.modelCategoryQuillen.I_le_monomorphisms, AlgebraicGeometry.instIsZariskiLocalAtTargetMonomorphismsScheme, SSet.instIsStableUnderFilteredColimitsMonomorphisms, AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms, SSet.modelCategoryQuillen.cofibrations_eq, RespectsIso.monomorphisms, CategoryTheory.IsGrothendieckAbelian.instIsStableUnderTransfiniteCompositionMonomorphisms, instIsStableUnderCoproductsMonomorphismsOfAB4OfSize, CategoryTheory.Types.instIsStableUnderCobaseChangeMonomorphismsType, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms, CategoryTheory.ConcreteCategory.injective_eq_monomorphisms, SSet.instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType, monomorphisms.iff, isStableUnderColimitsOfShape_monomorphisms, SSet.instIsStableUnderCobaseChangeMonomorphisms, CategoryTheory.ConcreteCategory.injective_eq_monomorphisms_iff, instIsStableUnderCoproductsOfShapeFunctorMonomorphismsOfHasCoproductsOfShapeOfHasPullbacks, CategoryTheory.Abelian.instIsStableUnderCobaseChangeMonomorphisms, CategoryTheory.Types.instIsStableUnderFilteredColimitsMonomorphismsType, functorCategory_monomorphisms, CategoryTheory.IsGrothendieckAbelian.llp_rlp_monomorphisms, CategoryTheory.ObjectProperty.monomorphisms_le_monoModSerre, instIsStableUnderFilteredColimitsMonomorphismsOfAB5OfSize, CategoryTheory.Types.instIsStableUnderCoproductsOfShapeMonomorphismsType, IsStableUnderBaseChange.hasOfPostcompProperty_monomorphisms, CategoryTheory.injective_iff_rlp_monomorphisms_of_isZero, AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono, CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_rlp, monomorphisms.infer_property, SSet.modelCategoryQuillen.J_le_monomorphisms, IsStableUnderBaseChange.monomorphisms, instIsStableUnderCoproductsFunctorMonomorphismsOfHasCoproductsOfHasPullbacks, CategoryTheory.IsGrothendieckAbelian.instHasFunctorialFactorizationMonomorphismsRlp, diagonal_isomorphisms, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms, presheaf_monomorphisms_le_monomorphisms, IsStableUnderRetracts.monomorphisms, CategoryTheory.Types.instIsStableUnderCoproductsMonomorphismsType, CategoryTheory.ConcreteCategory.injective_le_monomorphisms, CategoryTheory.injective_iff_rlp_monomorphisms_zero, IsMultiplicative.instMonomorphisms
ofHoms 📖	CompData	13 math math: ofHoms_iff, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W, isSmall_iff_eq_ofHoms, HomotopicalAlgebra.AttachCells.pushouts_coproducts, ofHoms_homFamily, HomotopicalAlgebra.nonempty_attachCells_iff, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_W, hasCardinalLT_ofHoms, isSmall_ofHoms, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W, HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape_toTransfiniteCompositionOfShape, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W
op 📖	CompOp	74 math math: CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_f, CategoryTheory.Localization.isLocalization_op, instHasOfPrecompPropertyOppositeOpOfHasOfPostcompProperty, IsStableUnderCobaseChange.op, LeftFraction.op_map, LeftFraction.op_X', HomotopicalAlgebra.weakEquivalences_op, CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_op, CategoryTheory.LocalizerMorphism.RightResolution.op_X₁, instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions, CategoryTheory.LocalizerMorphism.LeftResolution.unop_X₁, op_isomorphisms, CategoryTheory.LocalizerMorphism.RightResolution.unop_X₁, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_unitIso, CategoryTheory.LocalizerMorphism.instHasLeftResolutionsOppositeOpOpOfHasRightResolutions, RespectsIso.op, CategoryTheory.LocalizerMorphism.nonempty_rightResolution_iff_op, IsStableUnderComposition.op, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_inverse, instHasFactorizationOppositeOp, CategoryTheory.ObjectProperty.InheritedFromTarget.op, HomotopicalAlgebra.cofibrations_op, MapFactorizationData.op_Z, CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_obj, CategoryTheory.LocalizerMorphism.LeftResolution.unop_w, RightFractionRel.op, instHasTwoOutOfThreePropertyOppositeOp, IsStableUnderBaseChange.op, CategoryTheory.LocalizerMorphism.instIsLocalizedEquivalenceOppositeOpOp, instHasOfPostcompPropertyOppositeOpOfHasOfPrecompProperty, LeftFraction.op_f, CategoryTheory.Functor.op_iff, IsMultiplicative.op, LeftFraction.op_s, IsInvertedBy.leftOp, MapFactorizationData.op_i, CategoryTheory.Functor.IsLocalization.op_iff, CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_obj, rightFractionRel_op_iff, HomotopicalAlgebra.trivialCofibrations_op, op_inverseImage, RightFraction.op_f, RightFraction.op_map, IsInvertedBy.op, CategoryTheory.LocalizerMorphism.op_functor, CategoryTheory.LocalizerMorphism.nonempty_leftResolution_iff_op, ContainsIdentities.op, CategoryTheory.LocalizerMorphism.RightResolution.unop_w, HomotopicalAlgebra.fibrations_op, CategoryTheory.LocalizerMorphism.LeftResolution.op_w, CategoryTheory.ObjectProperty.InheritedFromSource.op, CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_f, instRespectsLeftOppositeOpOfRespectsRight, op_unop, leftFractionRel_op_iff, StableUnderInverse.op, instRespectsRightOppositeOpOfRespectsLeft, instHasRightCalculusOfFractionsOppositeOpOfHasLeftCalculusOfFractions, CategoryTheory.LocalizerMorphism.LeftResolution.op_X₁, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_counitIso, CategoryTheory.LocalizerMorphism.RightResolution.op_w, instIsStableUnderRetractsOppositeOp, LeftFractionRel.op, HomotopicalAlgebra.trivialFibrations_op, CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_op, CategoryTheory.Functor.IsLocalization.op, RightFraction.op_s, MapFactorizationData.op_p, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_functor, CategoryTheory.LocalizerMorphism.instHasRightResolutionsOppositeOpOpOfHasLeftResolutions, RightFraction.op_Y', isomorphisms_op, unop_op, CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_op
pi 📖	CompOp	3 math math: IsInvertedBy.pi, Pi.containsIdentities, CategoryTheory.Functor.IsLocalization.pi
prod 📖	CompOp	4 math math: CategoryTheory.Localization.Construction.prodIsLocalization, CategoryTheory.Functor.IsLocalization.prod, Prod.containsIdentities, IsInvertedBy.prod
strictMap 📖	CompData	3 math math: map_mem_strictMap, strictMap_multiplicativeClosure_le, SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap
toSet 📖	CompOp	21 math math: CategoryTheory.OrthogonalReflection.D₁.ι_comp_t_assoc, arrow_mk_mem_toSet_iff, CategoryTheory.SmallObject.ιFunctorObj_eq, ofHoms_homFamily, CategoryTheory.OrthogonalReflection.D₂.multispanIndex_left, homFamily_arrow_mk, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, mem_toSet_iff, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left, CategoryTheory.SmallObject.πFunctorObj_eq, CategoryTheory.OrthogonalReflection.D₁.ι_comp_t, IsSmall.small_toSet, CategoryTheory.OrthogonalReflection.D₂.multispanIndex_fst, IsCardinalForSmallObjectArgument.preservesColimit, toSet_max, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, CategoryTheory.SmallObject.preservesColimit, CategoryTheory.SmallObject.hasColimitsOfShape_discrete, homFamily_apply, CategoryTheory.OrthogonalReflection.D₂.multispanIndex_snd, toSet_iSup
unop 📖	CompOp	29 math math: LeftFractionRel.unop, instHasLeftCalculusOfFractionsUnopOfHasRightCalculusOfFractionsOpposite, IsStableUnderComposition.unop, RespectsIso.unop, RightFractionRel.unop, LeftFraction.unop_X', instHasTwoOutOfThreePropertyUnopOfOpposite, RightFraction.unop_s, ContainsIdentities.unop, instIsStableUnderRetractsUnopOfOpposite, IsStableUnderBaseChange.unop, LeftFraction.unop_f, HomotopicalAlgebra.fibrations_eq_unop, instHasOfPostcompPropertyUnopOfHasOfPrecompPropertyOpposite, LeftFraction.unop_s, instHasOfPrecompPropertyUnopOfHasOfPostcompPropertyOpposite, HomotopicalAlgebra.cofibrations_eq_unop, HomotopicalAlgebra.trivialFibrations_eq_unop, CategoryTheory.Functor.IsLocalization.unop, instHasRightCalculusOfFractionsUnopOfHasLeftCalculusOfFractionsOpposite, RightFraction.unop_f, HomotopicalAlgebra.trivialCofibrations_eq_unop, op_unop, HomotopicalAlgebra.weakEquivalences_eq_unop, IsStableUnderCobaseChange.unop, StableUnderInverse.unop, IsMultiplicative.unop, RightFraction.unop_Y', unop_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrow_iso_iff 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	comma_iso_iff
arrow_mk_iso_iff 📖	—	—	—	—	arrow_iso_iff
arrow_mk_mem_toSet_iff 📖	mathematical	—	CategoryTheory.Arrow Set Set.instMembership toSet	—	—
cancel_left_of_respectsIso 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.IsIso.inv_hom_id_assoc RespectsIso.precomp CategoryTheory.IsIso.inv_isIso
cancel_right_of_respectsIso 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id RespectsIso.postcomp CategoryTheory.IsIso.inv_isIso
comma_iso_iff 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Functor.map_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom CategoryTheory.Comma.inv_left_hom_right CategoryTheory.Functor.map_inv CategoryTheory.IsIso.inv_isIso CategoryTheory.Comma.instIsIsoRight
ext 📖	—	—	—	—	—
ext_iff 📖	—	—	—	—	ext
homFamily_apply 📖	mathematical	—	homFamily CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Arrow Set Set.instMembership toSet	—	—
homFamily_arrow_mk 📖	mathematical	—	homFamily CategoryTheory.Arrow Set Set.instMembership toSet	—	—
iSup_iff 📖	mathematical	—	iSup CategoryTheory.MorphismProperty CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	—	sSup_iff
inf 📖	mathematical	—	RespectsIso CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	—	RespectsLeft.inf Respects.toRespectsLeft RespectsRight.inf Respects.toRespectsRight
instRespectsIsoTop 📖	mathematical	—	RespectsIso Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—
instRespectsLeftOppositeOpOfRespectsRight 📖	mathematical	—	RespectsLeft Opposite CategoryTheory.CategoryStruct.opposite op	—	RespectsRight.postcomp
instRespectsOfRespectsLeftOfRespectsRight 📖	mathematical	—	Respects	—	—
instRespectsRightOppositeOpOfRespectsLeft 📖	mathematical	—	RespectsRight Opposite CategoryTheory.CategoryStruct.opposite op	—	RespectsLeft.precomp
inverseImage_equivalence_functor_eq_map_inverse 📖	mathematical	—	inverseImage CategoryTheory.Equivalence.inverse map CategoryTheory.Equivalence.functor	—	inverseImage_equivalence_inverse_eq_map_functor
inverseImage_equivalence_inverse_eq_map_functor 📖	mathematical	—	inverseImage CategoryTheory.Equivalence.functor map CategoryTheory.Equivalence.inverse	—	le_antisymm map_le_iff RespectsIso.inverseImage arrow_mk_iso_iff
inverseImage_iff 📖	mathematical	—	inverseImage CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
inverseImage_map_eq_of_isEquivalence 📖	mathematical	—	inverseImage map	—	inverseImage_equivalence_inverse_eq_map_functor map_respectsIso map_map map_eq_of_iso map_id
isoClosure_eq_iff 📖	mathematical	—	isoClosure RespectsIso	—	isoClosure_respectsIso le_antisymm arrow_mk_iso_iff le_isoClosure
isoClosure_eq_self 📖	mathematical	—	isoClosure	—	isoClosure_eq_iff
isoClosure_isoClosure 📖	mathematical	—	isoClosure	—	isoClosure_eq_self isoClosure_respectsIso
isoClosure_le_iff 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isoClosure	—	LE.le.trans le_isoClosure monotone_isoClosure isoClosure_eq_self le_refl
isoClosure_respectsIso 📖	mathematical	—	RespectsIso isoClosure	—	CategoryTheory.Arrow.isIso_left CategoryTheory.Iso.isIso_hom CategoryTheory.IsIso.inv_isIso CategoryTheory.Arrow.isIso_right CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.Arrow.w_mk_right CategoryTheory.Arrow.w_mk_right_assoc
isomorphisms_op 📖	mathematical	—	op CategoryTheory.Category.toCategoryStruct isomorphisms Opposite CategoryTheory.Category.opposite	—	op_isomorphisms
le_def 📖	mathematical	—	CategoryTheory.MorphismProperty Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	—	—
le_isoClosure 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isoClosure	—	—
map_eq_of_iso 📖	mathematical	—	map	—	le_antisymm
map_id 📖	mathematical	—	map CategoryTheory.Functor.id	—	map_id_eq_isoClosure isoClosure_eq_self
map_id_eq_isoClosure 📖	mathematical	—	map CategoryTheory.Functor.id isoClosure	—	—
map_inverseImage_eq_of_isEquivalence 📖	mathematical	—	map inverseImage	—	inverseImage_equivalence_inverse_eq_map_functor map_map map_eq_of_iso map_id
map_inverseImage_le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra map inverseImage isoClosure	—	—
map_isoClosure 📖	mathematical	—	map isoClosure	—	le_antisymm map_le_iff map_respectsIso monotone_map le_isoClosure
map_le_iff 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra map inverseImage	—	map_mem_map arrow_mk_iso_iff
map_map 📖	mathematical	—	map CategoryTheory.Functor.comp	—	le_antisymm map_le_iff map_respectsIso map_mem_map
map_mem_map 📖	mathematical	—	map CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
map_mem_strictMap 📖	mathematical	—	strictMap CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
map_respectsIso 📖	mathematical	—	RespectsIso map	—	RespectsIso.of_respects_arrow_iso
map_top_eq_top_of_essSurj_of_full 📖	mathematical	—	map Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	eq_top_iff CategoryTheory.Functor.map_preimage CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
mem_toSet_iff 📖	mathematical	—	CategoryTheory.Arrow Set Set.instMembership toSet CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
monotone_isoClosure 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra isoClosure	—	—
monotone_map 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra map	—	—
ofHoms_homFamily 📖	mathematical	—	ofHoms Set.Elem CategoryTheory.Arrow toSet CategoryTheory.Comma.left CategoryTheory.Functor.id Set Set.instMembership CategoryTheory.Comma.right homFamily	—	ext ofHoms_iff
ofHoms_iff 📖	mathematical	—	ofHoms	—	arrow_mk_mem_toSet_iff
of_eq 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—	arrow_mk_mem_toSet_iff CategoryTheory.Arrow.mk_eq_mk_iff
of_eq_top 📖	—	Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—	—
op_inverseImage 📖	mathematical	—	op CategoryTheory.Category.toCategoryStruct inverseImage Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
op_isomorphisms 📖	mathematical	—	op CategoryTheory.Category.toCategoryStruct isomorphisms Opposite CategoryTheory.Category.opposite	—	ext CategoryTheory.isIso_unop_iff
op_unop 📖	mathematical	—	op unop	—	—
sSup_iff 📖	mathematical	—	SupSet.sSup CategoryTheory.MorphismProperty CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra Set Set.instMembership	—	—
toSet_iSup 📖	mathematical	—	toSet iSup CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra Set.iUnion CategoryTheory.Arrow	—	Set.ext
toSet_max 📖	mathematical	—	toSet CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra Set CategoryTheory.Arrow Set.instUnion	—	—
top_apply 📖	mathematical	—	Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—
top_eq 📖	mathematical	—	Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra	—	—
unop_op 📖	mathematical	—	unop op	—	—

CategoryTheory.MorphismProperty.Respects

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toRespectsLeft 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsLeft	—	—
toRespectsRight 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsRight	—	—

CategoryTheory.MorphismProperty.RespectsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epimorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.MorphismProperty.epimorphisms	—	CategoryTheory.epi_comp CategoryTheory.IsIso.epi_of_iso CategoryTheory.Iso.isIso_hom
inverseImage 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.MorphismProperty.inverseImage	—	CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_isIso
isomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom
mk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.MorphismProperty.RespectsIso	—	—
monomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.mono_comp CategoryTheory.IsIso.mono_of_iso CategoryTheory.Iso.isIso_hom
of_respects_arrow_iso 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.MorphismProperty.RespectsIso	—	CategoryTheory.IsIso.inv_isIso CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
op 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	postcomp CategoryTheory.isIso_unop precomp
postcomp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.RespectsRight.postcomp CategoryTheory.MorphismProperty.Respects.toRespectsRight
precomp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.MorphismProperty.RespectsLeft.precomp CategoryTheory.MorphismProperty.Respects.toRespectsLeft
unop 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	postcomp CategoryTheory.isIso_op precomp

CategoryTheory.MorphismProperty.RespectsLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsLeft CategoryTheory.MorphismProperty SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	precomp
precomp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp	—	—

CategoryTheory.MorphismProperty.RespectsRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsRight CategoryTheory.MorphismProperty SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	postcomp
postcomp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp	—	—

CategoryTheory.MorphismProperty.epimorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff 📖	mathematical	—	CategoryTheory.MorphismProperty.epimorphisms CategoryTheory.Epi	—	—
infer_property 📖	mathematical	—	CategoryTheory.MorphismProperty.epimorphisms	—	—

CategoryTheory.MorphismProperty.isomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff 📖	mathematical	—	CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.IsIso	—	—
infer_property 📖	mathematical	—	CategoryTheory.MorphismProperty.isomorphisms	—	—

CategoryTheory.MorphismProperty.monomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff 📖	mathematical	—	CategoryTheory.MorphismProperty.monomorphisms CategoryTheory.Mono	—	—
infer_property 📖	mathematical	—	CategoryTheory.MorphismProperty.monomorphisms	—	—

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_app_iff_of_iso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj app	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms naturality

---

← Back to Index