EqToHom

📁 Source: Mathlib/CategoryTheory/EqToHom.lean

Statistics

Metric	Count
Definitions induced, eqToHom, eqToIso	3
Theorems induced_counitIso, induced_functor, induced_inverse_map, induced_inverse_obj, induced_unitIso, congr_hom, congr_hom_assoc, congr_inv_of_congr_hom, congr_obj, ext, ext_of_iso, hcongr_hom, hext, map_comp_heq, map_comp_heq', postcomp_map_heq, postcomp_map_heq', precomp_map_heq, eqToHom_hom, eqToHom_hom, comp_eqToHom_heq, comp_eqToHom_heq_iff, comp_eqToHom_iff, congrArg_cast_hom_left, congrArg_cast_hom_right, congrArg_mpr_hom_left, congrArg_mpr_hom_right, conj_eqToHom_iff_heq, conj_eqToHom_iff_heq', dcongr_arg, eqToHom_app, eqToHom_comp_heq, eqToHom_comp_heq_iff, eqToHom_comp_iff, eqToHom_heq_id_cod, eqToHom_heq_id_dom, eqToHom_iso_hom_naturality, eqToHom_iso_hom_naturality_assoc, eqToHom_iso_inv_naturality, eqToHom_iso_inv_naturality_assoc, eqToHom_map, eqToHom_map_comp, eqToHom_map_comp_assoc, eqToHom_naturality, eqToHom_naturality_assoc, eqToHom_op, eqToHom_refl, eqToHom_trans, eqToHom_trans_assoc, eqToHom_unop, hom, inv, eqToIso_map, eqToIso_map_trans, eqToIso_refl, eqToIso_trans, eq_conj_eqToHom, heq_comp, heq_comp_eqToHom_iff, heq_eqToHom_comp_iff, instIsIsoEqToHom, inv_eqToHom	62
Total	65

CategoryTheory

Definitions

Name	Category	Theorems
eqToHom 📖	CompOp	490 math math: AlgebraicGeometry.Γ_map_morphismRestrict, CostructuredArrow.homMk'_id, HomologicalComplex.eqToHom_f, Grothendieck.base_eqToHom, Limits.limitConeOfUnique_cone_π, Pi.eqToEquivalenceFunctorIso_hom, IsHomLift.eqToHom_domain_lift_id, FundamentalGroupoid.eqToHom_eq, PreZeroHypercover.inv_hom_h₀, Limits.Bicone.π_of_isColimit, Functor.OfSequence.congr_f, Grothendieck.ιCompMap_hom_app_fiber, GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, Limits.Cotrident.ofCocone_ι, AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc, Bicategory.eqToHomTransIso_refl_left, AlgebraicGeometry.Scheme.app_eq, AlgebraicTopology.NormalizedMooreComplex.obj_d, Limits.colimit.eqToHom_comp_ι_assoc, Limits.Cone.ofTrident_π, AlgebraicGeometry.StructureSheaf.comap_id, StrictlyUnitaryLaxFunctorCore.map₂_leftUnitor, eqToHom_comp_homOfLE_op, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, CatEnriched.id_hComp, MonoidalCategory.whiskerLeft_eqToHom, StructuredArrow.homMk'_comp, Cat.associator_hom_app, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ, StrictPseudofunctorCore.map₂_left_unitor, AlgebraicGeometry.Scheme.Opens.topIso_inv, Limits.biproduct.ι_π_assoc, FundamentalGroupoid.conj_eqToHom_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, Limits.biproduct.whiskerEquiv_inv, IsHomLift.comp_eqToHom_lift_iff, MorphismProperty.Comma.eqToHom_left, Limits.FormalCoproduct.isoOfComponents_inv_φ, eqToHom_iso_hom_naturality_assoc, AlgebraicGeometry.Scheme.inv_app, Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app, CostructuredArrow.mkPrecomp_id, eqToHom_map_comp, Limits.diagramIsoParallelFamily_inv_app, Limits.Cocone.ofCotrident_ι, Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos_assoc, Cat.Hom₂.eqToHom_toNatTrans, Functor.Fiber.fiberInclusionCompIsoConst_inv_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, Limits.FormalCoproduct.pullbackCone_fst_φ, Limits.Cofork.ofCocone_ι, Pretriangulated.Triangle.eqToHom_hom₂, IsHomLift.eqToHom_comp_lift, ComposableArrows.mk₁_eqToHom_comp, StrictPseudofunctorCore.map₂_associator, ObjectProperty.eqToHom_hom, IsHomLift.commSq, eqToIso.hom, AlgebraicGeometry.Scheme.congr_app, congrArg_cast_hom_right, AugmentedSimplexCategory.eqToHom_toOrderHom, Comma.eqToHom_left, Bicategory.rightUnitor_inv_congr, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', Limits.Sigma.ι_π_assoc, TopCat.Presheaf.pushforwardToOfIso_app, Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, eqToHom_heq_id_cod, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, Cat.leftUnitor_hom_app, Bicategory.associator_eqToHom_hom_assoc, Grothendieck.isoMk_inv_fiber, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, nerve.homEquiv_apply, AlgebraicGeometry.Scheme.eqToHom_c_app, Limits.FormalCoproduct.hom_ext_iff, MonoidalCategory.eqToHom_whiskerRight, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, Bicategory.InducedBicategory.eqToHom_hom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, Subgroupoid.IsWide.eqToHom_mem, Under.mapCongr_inv_app, eqToHom_map, DifferentialObject.eqToHom_f, homOfLE_comp_eqToHom, CostructuredArrow.homMk'_mk_id, Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, Idempotents.Karoubi.eqToHom_f, AlgebraicGeometry.Scheme.Hom.appLE_map', isPullback_of_cofan_isVanKampen, Pretriangulated.Triangle.eqToHom_hom₃, FreeMonoidalCategory.normalize_naturality, IsHomLift.lift_comp_eqToHom, eqToHom_app, TopologicalSpace.Opens.mapId_hom_app, Grothendieck.id_fiber, TopologicalSpace.Opens.mapComp_hom_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, Functor.congr_hom_assoc, Pretriangulated.Triangle.eqToHom_hom₁, AlgebraicGeometry.Scheme.Hom.congr_app, shiftFunctorAdd_zero_add_hom_app, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.kerAdjunction_unit_app, Limits.Pi.ι_π, StrictlyUnitaryPseudofunctorCore.map₂_left_unitor, Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_inv, homOfLE_op_comp_eqToHom_assoc, Cat.HasLimits.homDiagram_map, TopCat.Presheaf.pushforwardEq_hom_app, ShiftMkCore.add_zero_hom_app, Functor.congr_hom, Cat.associator_inv_app, OverPresheafAux.YonedaCollection.map₂_snd, Cat.rightUnitor_hom_app, Under.eqToHom_right, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, SmallObject.SuccStruct.prop.arrowIso_inv_right, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, Grothendieck.comp_fiber, Subgroupoid.mem_discrete_iff, Grothendieck.map_map, Under.mapId_inv, CatEnrichedOrdinary.hComp_id, Grothendieck.ιCompMap_inv_app_fiber, conj_eqToHom_iff_heq', MulEquiv.toSingleObjEquiv_unitIso_hom, Limits.diagramIsoParallelPair_hom_app, StructuredArrow.homMk'_mk_comp, AlgebraicGeometry.liftCoborder_app, ComposableArrows.mk₁_comp_eqToHom, heq_comp_eqToHom_iff, Bicategory.associator_eqToHom_inv, HomologicalComplex.d_comp_eqToHom, Limits.SequentialProduct.functorMap_commSq_aux, OverPresheafAux.counitForward_val_snd, PrelaxFunctor.map₂_eqToHom, SmallObject.SuccStruct.Iteration.subsingleton.MapEq.w, Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg_assoc, AlgebraicGeometry.PresheafedSpace.stalkMap.congr, Limits.limitBiconeOfUnique_bicone_π, Pi.evalCompEqToEquivalenceFunctor_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app, Limits.limitBiconeOfUnique_isBilimit_isColimit, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, Subgroupoid.mem_map_iff, StructuredArrow.eqToHom_right, eqToHom_iso_inv_naturality, eqToHom_comp_heq_iff, Over.eqToHom_left, Presieve.ofArrows_surj, cokernel.π_unop, Discrete.productEquiv_counitIso_hom_app, Grothendieck.fiber_eqToHom, TopologicalSpace.Opens.mapIso_inv_app, Grothendieck.eqToHom_eq, PreZeroHypercover.Hom.ext'_iff, IsHomLift.fac', TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app, SmallObject.SuccStruct.prop.arrowIso_hom_right, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, eqToHom_map_comp_assoc, Limits.limit.π_comp_eqToHom_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app, Bicategory.eqToHomTransIso_refl_right, CatEnriched.hComp_assoc, Limits.limit.π_comp_eqToHom, Pseudofunctor.CoGrothendieck.Hom.congr, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, FreeBicategory.preinclusion_map₂, MulEquiv.toSingleObjEquiv_counitIso_hom, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality, Cat.HasLimits.limit_π_homDiagram_eqToHom, AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc, TopologicalSpace.Opens.overEquivalence_unitIso_hom_app_left, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', Limits.Fork.ofCone_π, eqToHom_comp_heq, StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom, SimplexCategory.eqToHom_toOrderHom, eqToHom_refl, Presieve.ofArrows.eq_eqToHom_comp_hom_idx, Subgroupoid.mem_ker_iff, cokernel.π_op, comp_eqToHom_heq_iff, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, Mat_.isoBiproductEmbedding_hom, StructuredArrow.mkPostcomp_comp, StrictPseudofunctorCore.map₂_right_unitor, Under.mapCongr_hom_app, Limits.Sigma.eqToHom_comp_ι_assoc, PreZeroHypercover.inv_hom_h₀_assoc, Comma.eqToHom_right, AlgebraicGeometry.Scheme.Hom.app_invApp', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, kernel.ι_unop, ShiftMkCore.assoc_inv_app_assoc, instIsIsoEqToHom, MulEquiv.toSingleObjEquiv_unitIso_inv, Limits.Sigma.ι_π, eq_conj_eqToHom, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, Limits.Cocone.ofCofork_ι, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, Limits.FormalCoproduct.cochainComplexFunctor_obj_d, Bicategory.associator_eqToHom_inv_assoc, FreeMonoidalCategory.inclusion_map, ChainComplex.mk'_congr_succ'_d, Subgroupoid.Map.arrows_iff, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, IsHomLift.lift_eqToHom_comp_iff, StructuredArrow.homMk'_id, Under.mapComp_hom, CatEnrichedOrdinary.id_hComp, Equivalence.induced_inverse_map, Presieve.FamilyOfElements.singletonEquiv_symm_apply, TopologicalSpace.Opens.mapId_inv_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, MulEquiv.toSingleObjEquiv_counitIso_inv, Bicategory.whiskerRight_congr, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, Limits.Bicone.ofLimitCone_ι, Bicategory.whiskerLeft_eqToHom, Bicategory.associator_hom_congr, Idempotents.karoubiCochainComplexEquivalence_counitIso_hom, Functor.toOplaxFunctor_mapComp, TopologicalSpace.Opens.overEquivalence_counitIso_inv_app, AlgebraicGeometry.Scheme.map_basicOpen, TopologicalSpace.Opens.adjunction_counit_map_functor, Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app, CatEnrichedOrdinary.id_eq_eqToHom, Limits.Pi.π_comp_eqToHom_assoc, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc, TopologicalSpace.Opens.overEquivalence_unitIso_inv_app_left, PreZeroHypercover.hom_inv_h₀_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, TopologicalSpace.Opens.adjunction_counit_app_self, Bicategory.congr_whiskerLeft, eqToHom_comp_homOfLE, Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, Bicategory.associator_eqToHom_hom, ShiftMkCore.add_zero_inv_app, IsHomLift.lift_eqToHom_comp, Functor.eqToHom_proj, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, SmallObject.SuccStruct.prop.fac_assoc, eqToHom_op, CostructuredArrow.homMk'_mk_comp, Limits.limitBiconeOfUnique_isBilimit_isLimit, Limits.Pi.whiskerEquiv_hom, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, Limits.Trident.ofCone_π, AlgebraicGeometry.morphismRestrict_appTop, GradedObject.comapEq_hom_app, Limits.Pi.ι_π_assoc, Equivalence.induced_unitIso, germ_skyscraperPresheafStalkOfSpecializes_hom_assoc, congrArg_mpr_hom_left, StrictPseudofunctorPreCore.map₂_whisker_right, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, FreeBicategory.normalize_naturality, HomOrthogonal.matrixDecomposition_apply, IsHomLift.id_lift_eqToHom_domain, MorphismProperty.ContainsIdentities.eqToHom, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, Limits.biproduct.π_comp_eqToHom_assoc, Limits.diagramIsoParallelFamily_hom_app, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, shiftFunctorAdd_add_zero_inv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, Discrete.productEquiv_counitIso_inv_app, LocallyDiscrete.eqToHom_toLoc, IsHomLift.lift_comp_eqToHom_iff, HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, Limits.limitConeOfUnique_isLimit_lift, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, Presieve.ofArrows.hom_idx, Under.mapId_hom, SimplexCategoryGenRel.eq_or_len_le_of_P_δ, Cat.rightUnitor_inv_app, Pseudofunctor.Grothendieck.Hom.ext_iff, OverPresheafAux.YonedaCollection.mk_snd, inv_eqToHom, AlgebraicTopology.DoldKan.hσ'_eq, AlgebraicGeometry.Scheme.Hom.map_appLE', SmallObject.SuccStruct.prop.fac, GradedObject.eqToHom_proj, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, Limits.biproduct.eqToHom_comp_ι_assoc, Pseudofunctor.Grothendieck.Hom.congr, Limits.biproduct.π_comp_eqToHom, Limits.Bicone.ι_π, IsHomLift.id_lift_eqToHom_codomain, eqToHom_down, Pi.evalCompEqToEquivalenceFunctor_inv, PreZeroHypercover.hom_inv_h₀, AlgebraicGeometry.Spec.map_eqToHom, Limits.Cone.ofFork_π, Pi.eqToEquivalenceFunctorIso_inv, shiftFunctorAdd_add_zero_hom_app, homOfLE_op_comp_eqToHom, HomologicalComplex.eqToHom_comp_d, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, Bicategory.eqToHom_whiskerRight, Localization.Construction.WhiskeringLeftEquivalence.unitIso_inv, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, AlgebraicGeometry.SheafedSpace.id_hom_c, Limits.Pi.π_comp_eqToHom, AlgebraicGeometry.Scheme.Hom.appIso_hom, Limits.colimit.eqToHom_comp_ι, comp_eqToHom_iff, Mat_.isoBiproductEmbedding_inv, congrArg_cast_hom_left, StrictPseudofunctorPreCore.map₂_whisker_left, kernel.ι_op, Limits.Bicone.ofColimitCocone_π, Limits.Sigma.eqToHom_comp_ι, Bicategory.associator_inv_congr, Localization.Construction.WhiskeringLeftEquivalence.counitIso_inv, AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc, SmallObject.SuccStruct.Iteration.congr_map, AlgebraicGeometry.Scheme.Opens.ι_app_self, TopologicalSpace.Opens.mapComp_inv_app, ShiftMkCore.zero_add_hom_app, Idempotents.karoubiChainComplexEquivalence_counitIso_inv, Limits.biproduct.ι_π, ChainComplex.mk_congr_succ_d₂, HomologicalComplex.d_eqToHom_assoc, CatEnrichedOrdinary.hComp_assoc, CostructuredArrow.homMk'_comp, AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicTopology.DoldKan.N₂_obj_X_d, AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_assoc, InducedCategory.eqToHom_hom, Limits.Sigma.whiskerEquiv_inv, Subobject.arrow_congr, TopologicalSpace.Opens.mapIso_hom_app, Limits.biproduct.eqToHom_comp_ι, CostructuredArrow.eqToHom_left, Arrow.arrow_mk_comp_eqToHom, FundamentalGroupoid.conj_eqToHom, AlgebraicGeometry.PresheafedSpace.congr_app, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, Under.mapComp_inv, StrictlyUnitaryLaxFunctorCore.map₂_rightUnitor, NatTrans.congr, Bicategory.leftUnitor_hom_congr, Subgroupoid.mem_im_iff, Cat.HasLimits.limitConeLift_toFunctor, Functor.toOplaxFunctor_mapId, Mat_.id_apply, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_assoc, Grothendieck.map_map_fiber, skyscraperPresheafCoconeOfSpecializes_ι_app, AlgebraicGeometry.SheafedSpace.id_c, StrictlyUnitaryLaxFunctor.mk'_mapId, SSet.OneTruncation₂.nerveHomEquiv_apply, eqToHom_iso_inv_naturality_assoc, CatEnriched.eqToHom_hComp_eqToHom, CatEnrichedOrdinary.eqToHom_hComp_eqToHom, StrictlyUnitaryPseudofunctorCore.map₂_right_unitor, Discrete.sumEquiv_functor_map, MorphismProperty.Comma.eqToHom_right, ShiftMkCore.assoc_hom_app, eqToHom_trans_assoc, Limits.SequentialProduct.cone_π_app, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, GradedObject.eqToHom_apply, eqToHom_comp_iff, AlgebraicGeometry.SheafedSpace.congr_hom_app, StrictlyUnitaryLaxFunctor.mapIdIso_inv, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, eqToHom_comp_homOfLE_op_assoc, HomOrthogonal.matrixDecomposition_symm_apply, GradedObject.comapEq_inv_app, HomOrthogonal.matrixDecompositionAddEquiv_apply, conj_eqToHom_iff_heq, Functor.toOplaxFunctor'_mapComp, homOfLE_comp_eqToHom_assoc, Mat_.id_def, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, IsHomLift.comp_eqToHom_lift, Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_hom, Limits.colimitCoconeOfUnique_cocone_ι, Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom, Limits.SequentialProduct.functorMap_commSq_succ, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, IsHomLift.eqToHom_comp_lift_iff, congrArg_mpr_hom_right, TopCat.Presheaf.toPushforwardOfIso_app, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, SkyscraperPresheafFunctor.map'_app, AlgebraicGeometry.morphismRestrict_app, comp_eqToHom_heq, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, OverPresheafAux.YonedaCollection.map₁_snd, AlgebraicGeometry.Scheme.Opens.topIso_hom, CostructuredArrow.mkPrecomp_comp, TopologicalSpace.Opens.overEquivalence_counitIso_hom_app, AlgebraicGeometry.SheafedSpace.congr_app, PreZeroHypercover.isoMk_inv_h₀, IsHomLift.eqToHom_codomain_lift_id, Grothendieck.congr, eqToHom_naturality, Bicategory.InducedBicategory.mkHom_eqToHom, Limits.biproduct.whiskerEquiv_hom_eq_lift, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, Limits.limitBiconeOfUnique_bicone_ι, Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg, Limits.colimitCoconeOfUnique_isColimit_desc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, ShiftMkCore.zero_add_inv_app, OverPresheafAux.map_mkPrecomp_eqToHom, HomologicalComplex.d_eqToHom, Discrete.productEquiv_functor_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', Limits.diagramIsoParallelPair_inv_app, eqToHom_iso_hom_naturality, FunctorToTypes.eqToHom_map_comp_apply, Bicategory.leftUnitor_inv_congr, Bicategory.rightUnitor_hom_congr, eqToHom_unop, Discrete.productEquiv_inverse_map, Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom, CatEnriched.hComp_id, Functor.Fiber.fiberInclusionCompIsoConst_hom_app, Cat.leftUnitor_inv_app, CatEnrichedOrdinary.Hom.base_eqToHom, eqToHom_trans, AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity, AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op, Arrow.arrow_mk_eqToHom_comp, eqToHom_heq_id_dom, AlgebraicGeometry.Scheme.Hom.eqToHom_app, eqToHom_naturality_assoc, Grothendieck.transportIso_hom_fiber, StructuredArrow.homMk'_mk_id, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, Pseudofunctor.CoGrothendieck.Hom.ext_iff, AlgebraicGeometry.IsOpenImmersion.lift_app, eqToIso.inv, germ_skyscraperPresheafStalkOfSpecializes_hom, ContinuousMap.Homotopy.hcast_def, shiftFunctorAdd_zero_add_inv_app, StructuredArrow.mkPostcomp_id, Limits.FormalCoproduct.pullbackCone_snd_φ, Functor.toOplaxFunctor'_mapId, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point, Cat.eqToHom_app, skyscraperPresheaf_map, ShiftMkCore.assoc_hom_app_assoc, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, Grothendieck.ι_map, Idempotents.karoubiChainComplexEquivalence_counitIso_hom, ShiftMkCore.assoc_inv_app, Equivalence.induced_counitIso, heq_eqToHom_comp_iff, Limits.SequentialProduct.functorMap_commSq, dcongr_arg, IsHomLift.fac, Arrow.mk_eq_mk_iff, eqToHom_comp_homOfLE_assoc, Limits.FormalCoproduct.hom_ext_iff', Limits.Bicone.ι_of_isLimit
eqToIso 📖	CompOp	47 math math: AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, eqToIso_map, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, MonoOver.mapIso_unitIso, eqToIso.hom, StrictPseudofunctor.mk''_mapId, MonoOver.mapIso_counitIso, Discrete.equivalence_unitIso, eqToIso_trans, StrictlyUnitaryPseudofunctor.mk'_mapId, eqToIso_map_trans, AsSmall.equiv_unitIso, AsSmall.equiv_counitIso, StrictPseudofunctor.mk'_mapComp, Functor.toPseudoFunctor_mapComp, TopologicalSpace.Opens.mapMapIso_unitIso, Bicategory.Strict.rightUnitor_eqToIso, StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso, AlgebraicGeometry.Scheme.Hom.comp_appIso, OrderIso.equivalence_counitIso, AlgebraicGeometry.Scheme.Hom.id_appIso, GrothendieckTopology.overMapPullbackCongr_eq_eqToIso, eqToIso_refl, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, TransfiniteCompositionOfShape.ofOrderIso_isoBot, Equivalence.induced_unitIso, Discrete.equivalence_counitIso, Subobject.lowerEquivalence_counitIso, Cat.Hom.toNatIso_rightUnitor, Functor.toPseudoFunctor_mapId, SheafOfModules.Presentation.of_isIso_relations, Subobject.lowerEquivalence_unitIso, Subfunctor.equivalenceMonoOver_unitIso, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, StrictPseudofunctor.mapComp_eq_eqToIso, Functor.toPseudoFunctor'_mapId, Functor.toPseudoFunctor'_mapComp, StrictPseudofunctor.mk''_mapComp, StrictPseudofunctor.mk'_mapId, TopologicalSpace.Opens.mapMapIso_counitIso, PrelaxFunctor.map₂Iso_eqToIso, Bicategory.Strict.leftUnitor_eqToIso, Types.monoOverEquivalenceSet_counitIso, OrderIso.equivalence_unitIso, Bicategory.Strict.associator_eqToIso, eqToIso.inv, Equivalence.induced_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_eqToHom_heq 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	conj_eqToHom_iff_heq' eqToHom_refl Category.id_comp
comp_eqToHom_heq_iff 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	comp_eqToHom_heq
comp_eqToHom_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	Category.assoc eqToHom_trans Category.comp_id eq_whisker
congrArg_cast_hom_left 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	Category.id_comp
congrArg_cast_hom_right 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	Category.comp_id
congrArg_mpr_hom_left 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	Category.id_comp
congrArg_mpr_hom_right 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	Category.comp_id
conj_eqToHom_iff_heq 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom Quiver.Hom CategoryStruct.toQuiver	—	Category.comp_id Category.id_comp
conj_eqToHom_iff_heq' 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom Quiver.Hom CategoryStruct.toQuiver	—	conj_eqToHom_iff_heq
dcongr_arg 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	Category.comp_id Category.id_comp
eqToHom_app 📖	mathematical	—	NatTrans.app eqToHom Functor Category.toCategoryStruct Functor.category Functor.obj Functor.congr_obj	—	Functor.congr_obj
eqToHom_comp_heq 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	conj_eqToHom_iff_heq eqToHom_refl Category.comp_id
eqToHom_comp_heq_iff 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	eqToHom_comp_heq
eqToHom_comp_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	eqToHom_trans_assoc Category.id_comp
eqToHom_heq_id_cod 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct eqToHom CategoryStruct.id	—	—
eqToHom_heq_id_dom 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct eqToHom CategoryStruct.id	—	—
eqToHom_iso_hom_naturality 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Iso.hom eqToHom	—	Category.comp_id Category.id_comp
eqToHom_iso_hom_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Iso.hom eqToHom	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_iso_hom_naturality
eqToHom_iso_inv_naturality 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Iso.inv eqToHom	—	Category.comp_id Category.id_comp
eqToHom_iso_inv_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Iso.inv eqToHom	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_iso_inv_naturality
eqToHom_map 📖	mathematical	—	Functor.map eqToHom Category.toCategoryStruct Functor.obj	—	Functor.map_id
eqToHom_map_comp 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.map eqToHom	—	Functor.map_id Category.comp_id
eqToHom_map_comp_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.map eqToHom	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_map_comp
eqToHom_naturality 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	Category.comp_id Category.id_comp
eqToHom_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_naturality
eqToHom_op 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct eqToHom Opposite CategoryStruct.opposite Opposite.op	—	—
eqToHom_refl 📖	mathematical	—	eqToHom CategoryStruct.id	—	—
eqToHom_trans 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	Category.comp_id
eqToHom_trans_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_trans
eqToHom_unop 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct eqToHom Opposite CategoryStruct.opposite Opposite.unop	—	—
eqToIso_map 📖	mathematical	—	Functor.mapIso eqToIso Functor.obj	—	Iso.ext Functor.mapIso_refl
eqToIso_map_trans 📖	mathematical	—	Iso.trans Functor.obj Functor.mapIso eqToIso	—	Functor.mapIso_refl Iso.trans_refl
eqToIso_refl 📖	mathematical	—	eqToIso Iso.refl	—	—
eqToIso_trans 📖	mathematical	—	Iso.trans eqToIso	—	Iso.ext eqToHom_trans
eq_conj_eqToHom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct eqToHom	—	Category.comp_id Category.id_comp
heq_comp 📖	mathematical	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	CategoryStruct.comp	—	—
heq_comp_eqToHom_iff 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	comp_eqToHom_heq
heq_eqToHom_comp_iff 📖	mathematical	—	Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp eqToHom	—	eqToHom_comp_heq
instIsIsoEqToHom 📖	mathematical	—	IsIso eqToHom Category.toCategoryStruct	—	Iso.isIso_hom
inv_eqToHom 📖	mathematical	—	inv eqToHom Category.toCategoryStruct instIsIsoEqToHom	—	instIsIsoEqToHom IsIso.inv_id

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
induced 📖	CompOp	5 math math: induced_inverse_map, induced_unitIso, induced_inverse_obj, induced_functor, induced_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induced_counitIso 📖	mathematical	—	counitIso CategoryTheory.InducedCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.InducedCategory.instCategory induced CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp Equiv.symm CategoryTheory.InducedCategory.homMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.inducedFunctor CategoryTheory.Functor.id CategoryTheory.eqToIso CategoryTheory.Functor.obj	—	—
induced_functor 📖	mathematical	—	functor CategoryTheory.InducedCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.InducedCategory.instCategory induced CategoryTheory.inducedFunctor	—	—
induced_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.InducedCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.InducedCategory.instCategory inverse induced CategoryTheory.InducedCategory.homMk Equiv.symm CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—
induced_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.InducedCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.InducedCategory.instCategory inverse induced Equiv.symm	—	—
induced_unitIso 📖	mathematical	—	unitIso CategoryTheory.InducedCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.InducedCategory.instCategory induced CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.inducedFunctor Equiv.symm CategoryTheory.InducedCategory.homMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.eqToIso CategoryTheory.Functor.obj	—	—

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_hom 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.eqToHom congr_obj	—	congr_obj CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
congr_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map CategoryTheory.eqToHom congr_obj	—	congr_obj CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' congr_hom
congr_inv_of_congr_hom 📖	mathematical	obj map CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	CategoryTheory.Iso.inv	—	map_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.IsIso.Iso.inv_hom map_inv CategoryTheory.IsIso.comp_isIso CategoryTheory.instIsIsoEqToHom CategoryTheory.inv.congr_simp CategoryTheory.IsIso.inv_comp CategoryTheory.inv_eqToHom CategoryTheory.Category.assoc
congr_obj 📖	mathematical	—	obj	—	—
ext 📖	—	obj	—	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
ext_of_iso 📖	—	obj	—	—	ext CategoryTheory.cancel_mono CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.NatTrans.naturality CategoryTheory.Category.assoc CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl CategoryTheory.Category.comp_id
hcongr_hom 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj map	—	—
hext 📖	—	obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct map	—	—	ext CategoryTheory.conj_eqToHom_iff_heq
map_comp_heq 📖	mathematical	obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct map	CategoryTheory.CategoryStruct.comp	—	map_comp
map_comp_heq' 📖	mathematical	obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct map	CategoryTheory.CategoryStruct.comp	—	hext
postcomp_map_heq 📖	mathematical	obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct map	comp	—	—
postcomp_map_heq' 📖	mathematical	obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct map	comp	—	hext
precomp_map_heq 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj map	comp	—	—

CategoryTheory.InducedCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqToHom_hom 📖	mathematical	—	Hom.hom CategoryTheory.eqToHom CategoryTheory.InducedCategory CategoryTheory.Category.toCategoryStruct instCategory	—	—

CategoryTheory.ObjectProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqToHom_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom FullSubcategory FullSubcategory.obj CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct FullSubcategory.category	—	—

CategoryTheory.eqToIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.eqToIso CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—
inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.eqToIso CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index