Forget

📁 Source: Mathlib/CategoryTheory/ConcreteCategory/Forget.lean

Statistics

Metric	Count
Definitions hasForget₂, HasForget₂, forget₂, mk', trans, hasForget₂, instConcreteCategory, instFunLike, forget, forget₂	10
Theorems forget_map_eq_coe, forget₂_comp_apply, forget_comp, naturality_apply, hom_eq_coe, congr_arg, congr_fun, forget_obj, forget₂_comp_apply, forget₂_faithful, hom_isIso, instFaithfulForget	12
Total	22

CategoryTheory

Definitions

Name	Category	Theorems
HasForget₂ 📖	CompData	—
forget 📖	CompOp	297 math math: CommSemiRingCat.forget_obj, ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier, Types.instIsCorepresentableForgetTypeHom, ModuleCat.forget_preservesLimits, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, Presheaf.instIsLocallySurjectiveHomWhiskerRightOppositeForget, AddGrpCat.forget_grp_preserves_epi, GrpWithZero.forget_map, CommRingCat.forget_preservesLimitsOfSize, CommRingCat.forgetReflectIsos, ModuleCat.forget_preservesLimitsOfSize, FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV, instFaithfulForget, Profinite.forget_preservesLimits, AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits, TopCat.coe_of_of, CommMonCat.forget_preservesLimitsOfShape, MonCat.forget_map, MonCat.forget_reflects_isos, whiskering_linearCoyoneda, AddMonCat.forget_reflects_isos, AddMonCat.forget_preservesLimitsOfSize, Opens.mayerVietorisSquare_X₃, GrpCat.forget_reflects_isos, CondensedMod.isDiscrete_tfae, TopCat.uliftFunctorCompForgetIso_hom_app, CommGrpCat.hasLimit_iff_small_sections, yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, CommGrpCat.forget_map, MonCat.forget_preservesLimitsOfSize, yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, Types.instReflectsLimitsOfSizeForgetTypeHom, AlgCat.forget_obj, AddGrpCat.forget_preservesLimits, CommGrpCat.forget_preservesLimits, PresheafOfModules.sections_property, GrpCat.forget_isCorepresentable, MonCat.forget_preservesLimitsOfShape, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, CommRingCat.forget_obj, ModuleCat.forget_preservesEpimorphisms, AddMagmaCat.forgetReflectsIsos, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, TopCat.forget_preservesColimits, AddCommGrpCat.forget_preservesLimits, MonObj.ofRepresentableBy_one, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk, ModuleCat.forget_reflectsLimitsOfSize, AddCommGrpCat.forget_preservesLimitsOfShape, SemimoduleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, SemimoduleCat.forget_obj, ModuleCat.forget_preservesMonomorphisms, AddGrpCat.forget_grp_preserves_mono, Lat.forget_map, HopfAlgCat.forget_reflects_isos, AlgCat.forget_map, RingCat.forget_map_apply, PresheafOfModules.sectionsMap_coe, AddMonCat.forget_preservesLimitsOfShape, CommGrpCat.FilteredColimits.forget_preservesFilteredColimits, BialgCat.forget_reflects_isos, CommGrpCat.μ_forget_apply, ModuleCat.uliftFunctorForgetIso_hom_app, MonCat.instIsRightAdjointForgetMonoidHomCarrier, CommMonCat.forget_preservesLimitsOfSize, CommGrpCat.forget_commGrp_preserves_mono, TopCat.forget_preservesLimitsOfSize, AddMonCat.forget_map, Types.instFullForgetTypeHom, AddCommGrpCat.forget_commGrp_preserves_epi, AddCommMonCat.forget_preservesLimitsOfShape, CondensedMod.isDiscrete_iff_isDiscrete_forget, AddCommGrpCat.coyonedaForget_inv_app_app, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, essImage_yonedaMon, AddMagmaCat.forget_map, AddCommGrpCat.coyonedaForget_hom_app_app_hom, CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, ModuleCat.FilteredColimits.forget_preservesFilteredColimits, PartOrdEmb.Limits.CoconePt.fac_apply, PreGaloisCategory.autIsoFibers_inv_app, AddGrpCat.FilteredColimits.forget_preservesFilteredColimits, CommSemiRingCat.forgetReflectIsos, FinBddDistLat.forget_map, SemiRingCat.forget_preservesLimitsOfSize, CommMonCat.coyonedaForget_inv_app_app, AddMonCat.FilteredColimits.forget_preservesFilteredColimits, DistLat.forget_map, AddCommMonCat.forget_preservesLimits, AddGrpCat.forget_preservesLimitsOfShape, AlgCat.forget_preservesLimits, CommRingCat.forget_map, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk, CommGrpCat.forget_isCorepresentable, essImage_yonedaGrp, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, AddCommMonCat.FilteredColimits.forget_preservesFilteredColimits, TopCat.hasLimit_iff_small_sections, whiskering_linearYoneda, RingCat.FilteredColimits.forget_preservesFilteredColimits, CommMonCat.forget_map, PartOrdEmb.Limits.cocone_ι_app, AddCommGrpCat.forget_commGrp_preserves_mono, BddDistLat.forget_map, CommBialgCat.reflectsIsomorphisms_forget, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, FGModuleCat.instFiniteCarrierPiObjModuleCatOfFinite, CommSemiRingCat.forget_preservesLimits, ModuleCat.adj_homEquiv, GrpCat.forget_preservesLimits, LightCondensed.forget_map_val_app, AddMonCat.forget_isCorepresentable, Types.instPreservesLimitsOfSizeForgetTypeHom, TopCat.uliftFunctorCompForgetIso_inv_app, Types.instIsEquivalenceForgetTypeHom, whiskering_preadditiveYoneda, Stonean.forget.preservesLimits, ConcreteCategory.injective_eq_monomorphisms_iff, SemiRingCat.FilteredColimits.forget_preservesFilteredColimits, Opens.mayerVietorisSquare_X₂, Semigrp.forgetReflectsIsos, Presheaf.isLocallyInjective_forget_iff, BddOrd.forget_map, CoalgCat.forget_reflects_isos, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top, ModuleCat.forget_reflectsLimits, RingCat.forget_preservesLimitsOfSize, ModuleCat.uliftFunctorForgetIso_inv_app, CommGrpCat.forget_reflects_isos, AddGrpCat.hasLimit_iff_small_sections, PresheafOfModules.unitHomEquiv_apply_coe, Opens.coe_mayerVietorisSquare_X₁, GrpCat.hasLimit_iff_small_sections, AddCommGrpCat.μ_forget_apply, MonCat.forget_isCorepresentable, Types.instPreservesColimitsOfSizeForgetTypeHom, PresheafOfModules.freeAdjunctionUnit_app, Presheaf.isLocallySurjective_iff_whisker_forget, Preord.forget_map, Sheaf.isLocallyInjective_forget, forget_obj, LightProfinite.forget_reflectsIsomorphisms, CompHausLike.forget_reflectsIsomorphisms, CommRingCat.FilteredColimits.forget_preservesFilteredColimits, AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, SimplexCategory.instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat, ModuleCat.forget_obj, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, SemiRingCat.forgetReflectIsos, ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier, ModuleCat.FilteredColimits.forget_reflectsFilteredColimits, TopCat.hasColimit_iff_small_colimitType, AddCommGrpCat.kernelIsoKer_inv_comp_ι, AddGrpCat.forget_reflects_isos, AddGrpCat.μ_forget_apply, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, yonedaGrpObjIsoOfRepresentableBy_hom, yonedaGrpObjIsoOfRepresentableBy_inv, LinOrd.forget_map, SheafOfModules.Presentation.map_relations_I, CommSemiRingCat.FilteredColimits.forget_preservesFilteredColimits, CommAlgCat.forget_obj, PresheafOfModules.Elements.fromFreeYoneda_app_apply, SheafOfModules.Presentation.mapRelations_mapGenerators, Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomCarrier, SheafOfModules.relationsOfIsCokernelFree_I, PartOrdEmb.forget_map, TopCat.instIsLeftAdjointForgetContinuousMapCarrier, CommRingCat.forget_map_apply, CommMonCat.instIsRightAdjointForgetMonoidHomCarrier, MonCat.FilteredColimits.forget_preservesFilteredColimits, AddMonCat.forget_preservesLimits, RingCat.forgetReflectIsos, CommMonCat.forget_reflects_isos, MonObj.ofRepresentableBy_mul, GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, CommSemiRingCat.forget_map, CommGrpCat.coyonedaForget_hom_app_app_hom, CommAlgCat.forget_map, Presheaf.imageSieve_eq_sieveOfSection, CommRingCat.equalizer_ι_isLocalHom', PartOrdEmb.Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier, CondensedSet.isDiscrete_tfae, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, PresheafOfModules.sectionsMk_coe, ConcreteCategory.surjective_eq_epimorphisms_iff, CommMonCat.forget_preservesLimits, bipointedToPointedSnd_comp_forget, MagmaCat.forget_map, AlgCat.forget_preservesLimitsOfSize, Presheaf.imageSieve_whisker_forget, AddCommMonCat.coyonedaForget_inv_app_app, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, AddGrpCat.forget_preservesLimitsOfSize, GrpCat.forget_grp_preserves_epi, HasForget₂.forget_comp, TopCat.coneOfConeForget_π_app, Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, AddCommMonCat.instIsRightAdjointForgetAddMonoidHomCarrier, SemimoduleCat.forget_map, CommRingCat.equalizer_ι_isLocalHom, Limits.Concrete.small_sections_of_hasLimit, GrpCat.FilteredColimits.forget_preservesFilteredColimits, TopCat.instIsRightAdjointForgetContinuousMapCarrier, GrpCat.forget_preservesLimitsOfShape, CommSemiRingCat.forget_preservesLimitsOfSize, CommGrpCat.forget_commGrp_preserves_epi, AlgCat.forget_reflects_isos, CommBialgCat.forget_obj, TopCat.adj₂_counit, CommGrpCat.coyonedaForget_inv_app_app, SemiRingCat.forget_preservesLimits, CommMonCat.coyonedaForget_hom_app_app_hom, AddCommMonCat.forget_isCorepresentable, CommAlgCat.reflectsIsomorphisms_forget, AddCommGrpCat.forget_map, Opens.mayerVietorisSquare'_toSquare, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, PartOrdEmb.Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier, PreGaloisCategory.AutGalois.π_apply, SheafOfModules.relationsOfIsCokernelFree_s, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, AddCommMonCat.forget_preservesLimitsOfSize, RingCat.forget_preservesLimits, GrpCat.forget_map, Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomCarrier, SemiRingCat.forget_obj, PresheafOfModules.freeAdjunction_unit_app, TopCat.forget_preservesColimitsOfSize, GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberForget, CommGrpCat.forget_preservesLimitsOfSize, Types.instReflectsColimitsOfSizeForgetTypeHom, TopCat.adj₂_unit, TopCat.forget_preservesLimits, Frm.forget_map, CommBialgCat.forget_map, TopCat.adj₁_unit, GrpCat.forget_preservesLimitsOfSize, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, TopCat.adj₁_counit, CommMonCat.FilteredColimits.forget_preservesFilteredColimits, SheafOfModules.Presentation.IsFinite.finite_relations, PartOrd.forget_map, AddCommMonCat.coyonedaForget_hom_app_app_hom, MonCat.forget_preservesLimits, ModuleCat.forget_map, PresheafOfModules.sections_ext_iff, CommRingCat.forget_preservesLimits, AddGrpCat.forget_isCorepresentable, HeytAlg.forget_map, Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, SheafOfModules.pushforwardSections_coe, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, Semigrp.forget_map, AddCommGrpCat.instIsRightAdjointForgetAddMonoidHomCarrier, PartOrdEmb.Limits.instPreservesColimitForgetOrderEmbeddingCarrier, AddCommGrpCat.forget_isCorepresentable, MagmaCat.forgetReflectsIsos, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, PresheafOfModules.freeAdjunction_homEquiv, Presheaf.isLocallyInjective_forget, GrpCat.μ_forget_apply, RingCat.forget_obj, TopCat.coconeOfCoconeForget_ι_app, AddCommMonCat.forget_map, CommMonCat.forget_isCorepresentable, PresheafOfModules.freeObjDesc_app, Condensed.instAB4CondensedMod, AddCommMonCat.forget_reflects_isos, instReflectsIsomorphismsForgetTypeHom, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, ConcreteCategory.forget_map_eq_coe, SemiRingCat.forget_map, GrpCat.forget_grp_preserves_mono, CommRingCat.instIsRightAdjointForgetRingHomCarrier, FintypeCat.instFullForgetHomCarrier, AlgCat.instIsRightAdjointForgetAlgHomCarrier, CommGrpCat.forget_preservesLimitsOfShape, AddCommGrpCat.hasLimit_iff_small_sections, RingCat.forget_map, AddSemigrp.forgetReflectsIsos, AddCommGrpCat.forget_preservesLimitsOfSize, GrpCat.instIsRightAdjointForgetMonoidHomCarrier, BoolAlg.forget_map, SheafOfModules.unitHomEquiv_apply_coe, bipointedToPointedFst_comp_forget, whiskering_preadditiveCoyoneda, AddCommGrpCat.forget_reflects_isos, ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite
forget₂ 📖	CompOp	291 math math: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, PresheafOfModules.Monoidal.tensorObj_obj, AddCommGrpCat.forget₂AddGroup_preservesLimitsOfShape, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, CommRingCat.forget₂Ring_preservesLimitsOfSize, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier, ModuleCat.forget₂_reflectsLimitsOfSize, AddGrpCat.forget₂_map, CommRingCat.instFullRingCatForget₂RingHomCarrierCarrier, ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForget₂RingHomCarrierAddMonoidHomCarrier, UniformSpaceCat.completionHom_val, ModuleCat.forget₂PreservesColimitsOfSize, CommMonCat.forget₂_full, TopModuleCat.instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize, CommGrpCat.forget₂CommMon_preservesLimitsOfShape, ProfiniteGrp.ProfiniteCompletion.lift_eta, SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, CommMonCat.coe_forget₂_obj, TopCommRingCat.instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize, RingCat.forget₂AddCommGroup_preservesLimits, TwoP_swap_comp_forget_to_Bipointed, CommAlgCat.forget₂_commRingCat_obj, AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits, PresheafOfModules.Derivation.d_map, QuadraticModuleCat.forget₂_map_associator_inv, TopModuleCat.instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, SemilatInfCat_dual_comp_forget_to_partOrd, AddCommMonCat.hom_forget₂_map, CommGrpCat.FilteredColimits.forget₂Group_preservesFilteredColimits, RingCat.forget₂_map, ModuleCat.forget₂_addCommGrp_essSurj, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, ModuleCat.forget₂AddCommGroup_reflectsLimitOfShape, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk, bddOrd_dual_comp_forget_to_bipointed, CommGrpCat.forget₂Group_preservesLimit, ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Action.forget₂_preservesZeroMorphisms, AddCommGrpCat.forget₂_map, ModuleCat.HasColimit.colimitCocone_ι_app, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, QuadraticModuleCat.forget₂_map, PresheafOfModules.Derivation.postcomp_d_apply, ModuleCat.forget₂_addCommGroup_full, PresheafOfModules.Derivation.d_one, AddCommGrpCat.FilteredColimits.forget₂AddGroup_preservesFilteredColimits, bddLat_dual_comp_forget_to_lat, AddCommMonCat.forget₂AddMonPreservesLimitsOfSize, boolRingCatEquivBoolAlg_functor, CommAlgCat.forget₂_algCat_map, PresheafOfModules.Derivation.d_mul, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, ModuleCat.smul_naturality, CommGrpCat.forget₂CommMon_preservesLimitsOfSize, GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, ModuleCat.HasColimit.colimitCocone_pt_isModule, IsCommMonObj.ofRepresentableBy, CommGrpCat.forget₂Group_preservesLimits, preadditiveYoneda_obj, SemimoduleCat.forget₂_obj_moduleCat_of, Rep.standardComplex.εToSingle₀_comp_eq, AlgCat.forget₂Ring_preservesLimitsOfSize, SemiRingCat.forget₂Mon_preservesLimitsOfSize, CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier, PresheafOfModules.Monoidal.tensorObj_map_tmul, CommBialgCat.forget₂_commAlgCat_obj, IsCommMon.ofRepresentableBy, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso, UniformSpaceCat.extension_comp_coe, CommGrpCat.instFullGrpCatForget₂MonoidHomCarrierCarrier, finBddDistLat_dual_comp_forget_to_bddDistLat, CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, AddGrpCat.forget₂AddMonPreservesLimitsOfSize, TopCommRingCat.forgetToTopCatTopologicalRing, distLat_dual_comp_forget_to_Lat, RingCat.forget₂SemiRing_preservesLimitsOfSize, AddCommMonCat.forget₂_full, ShortComplex.exact_iff_of_hasForget, HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso, CommMonCat.forget₂_map_ofHom, FinBoolAlg.forgetToFinPartOrdFaithful, AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier, BialgCat.forget₂_coalgebra_obj, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, ModuleCat.forget₂AddCommGroup_preservesLimits, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk, PresheafOfModules.Derivation.congr_d, bddOrd_dual_comp_forget_to_partOrd, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, ModuleCat.forget₂_obj, SemiRingCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, AlgCat.forget₂Module_preservesLimitsOfSize, GrpCat.forget₂Mon_preservesLimits, CoalgCat.MonoidalCategory.inducingFunctorData_μIso, CoalgCat.MonoidalCategory.inducingFunctorData_εIso, AddCommMonCat.forget₂Mon_preservesLimits, whiskering_linearCoyoneda₂, reflectsIsomorphisms_forget₂, AlexDisc.forgetToTop_faithful, CommMonCat.hom_forget₂_map, BialgCat.forget₂_algebra_map, Preadditive.epi_iff_surjective, CommSemiRingCat.forget₂SemiRing_preservesLimits, Preadditive.mono_iff_injective, CommMonCat.forget₂Mon_preservesLimitsOfSize, Semigrp.forget₂_full, HopfAlgCat.forget₂_bialgebra_obj, pointedToTwoPFst_comp_forget_to_bipointed, SemilatInfCat.coe_forget_to_partOrd, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, QuadraticModuleCat.forget₂_map_associator_hom, CommRingCat.forget₂CommSemiRing_preservesLimits, AddCommGrpCat.forget₂AddGroup_preservesLimits, partOrdEmb_dual_comp_forget_to_pardOrd, ModuleCat.smulNatTrans_apply_app, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, ConcreteCategory.forget₂_preservesEpimorphisms, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, bddLat_dual_comp_forget_to_semilatSupCat, CommRingCat.forgetToRingCat_obj, AddGrpCat.forget₂_map_ofHom, AddCommGrpCat.forget₂_addGrp_map_ofHom, QuadraticModuleCat.forget₂_obj, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape, AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, ConcreteCategory.forget₂_comp_apply, bddLat_dual_comp_forget_to_semilatInfCat, PresheafOfModules.Derivation'.d_app, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, ModuleCat.FilteredColimits.forget₂AddCommGroup_preservesFilteredColimits, ModuleCat.forget₂_obj_moduleCat_of, CommAlgCat.forget₂_algCat_obj, forget₂_comp_apply, AddCommGrpCat.forget₂AddGroup_preservesLimit, boolRingCatEquivBoolAlg_inverse, ShortComplex.ShortExact.injective_f, GrpCat.forget₂_map, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, AddCommGrpCat.instFullAddGrpCatForget₂AddMonoidHomCarrierCarrier, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d, TopModuleCat.instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, ModuleCat.HasColimit.coconePointSMul_apply, AlgCat.forget₂_module_obj, AddCommGrpCat.forget₂AddGroup_preservesLimitsOfSize, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, AddCommMonCat.coe_forget₂_obj, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, ShortComplex.ShortExact.surjective_g, CommRingCat.forget₂Ring_preservesLimits, AddSemigrp.forget₂_full, ShortComplex.zero_apply, GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, BddLat.coe_forget_to_lat, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, CoalgCat.forget₂_obj, CommRingCat.FilteredColimits.forget₂Ring_preservesFilteredColimits, alexDiscEquivPreord_unitIso, ModuleCat.mkOfSMul_smul, AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForget₂AddMonoidHomCarrierCarrier, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj, CommSemiRingCat.FilteredColimits.forget₂SemiRing_preservesFilteredColimits, CommGrpCat.forget₂Group_preservesLimitsOfSize, PresheafOfModules.Derivation.d_app, AlexDisc.coe_forgetToTop, TopModuleCat.forget₂_TopCat_obj, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, BialgCat.MonoidalCategory.inducingFunctorData_μIso, GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier, Lat_dual_comp_forget_to_partOrd, PresheafOfModules.Monoidal.tensorHom_app, RingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map, ModuleCat.reflectsColimitsOfShape, finBoolAlg_dual_comp_forget_to_finBddDistLat, ModuleCat.forget₂AddCommGroup_reflectsLimitOfSize, AlexDisc.forgetToTop_full, CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, completeLat_dual_comp_forget_to_bddLat, PresheafOfModules.Derivation'.app_apply, CoalgCat.forget₂_map, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, AlgCat.forget₂Module_preservesLimits, TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, ConcreteCategory.forget₂_preservesMonomorphisms, RingCat.forget₂SemiRing_preservesLimits, HopfAlgCat.forget₂_bialgebra_map, SemiRingCat.forget₂AddCommMon_preservesLimits, CommSemiRingCat.forget₂SemiRing_preservesLimitsOfSize, BddLat.coe_forget_to_semilatSup, AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, ModuleCat.HasColimit.colimitCocone_pt_carrier, ModuleCat.forget₂_addCommGrp_additive, RingCat.forget₂AddCommGroup_preservesLimitsOfSize, AddCommMonCat.forget₂_map_ofHom, SimplexCategory.toCat_obj, AddCommGrpCat.forget₂_commMonCat_map_ofHom, TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, CommMonCat.forget₂Mon_preservesLimits, AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize, AlgCat.forget₂_module_map, FDRep.forget₂_ρ, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, BialgCat.forget₂_coalgebra_map, ModuleCat.forget₂_reflectsLimits, ModuleCat.forget₂PreservesColimitsOfShape, FinPartOrd_dual_comp_forget_to_partOrd, GrpCat.forget₂_map_ofHom, ModuleCat.forget₂AddCommGroup_reflectsLimit, AlgCat.forget₂Ring_preservesLimits, BddLat.coe_forget_to_bddOrd, BddLat.coe_forget_to_semilatInf, TopModuleCat.instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, boolAlg_dual_comp_forget_to_bddDistLat, CommGrpCat.instReflectsIsomorphismsGrpCatForget₂MonoidHomCarrierCarrier, Action.isContinuous_def, FinBoolAlg.forgetToBoolAlg_full, CommGrpCat.forget₂_grp_map_ofHom, ProfiniteGrp.diagram_map, ModuleCat.forget₂AddCommGroup_preservesLimit, bddDistLat_dual_comp_forget_to_distLat, CommGrpCat.forget₂_commMonCat_map_ofHom, FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, CommBialgCat.forget₂_commAlgCat_map, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, alexDiscEquivPreord_counitIso, SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize, whiskering_linearYoneda₂, forget₂_faithful, SemilatSupCat_dual_comp_forget_to_partOrd, CommRingCat.forgetToRingCat_map_hom, linOrd_dual_comp_forget_to_Lat, SemiRingCat.forget₂_monCat_map, ModuleCat.HasColimit.reflectsColimit, BialgCat.forget₂_algebra_obj, UniformSpaceCat.extensionHom_val, SimplexCategory.toCat_map, PresheafOfModules.germ_smul, AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, pointedToTwoPSnd_comp_forget_to_bipointed, SemilatSupCat.coe_forget_to_partOrd, partOrd_dual_comp_forget_to_preord, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Action.forget₂_linear, AlexDisc.forgetToTop_of, ModuleCat.forget₂AddCommGroupIsEquivalence, UniformSpaceCat.extension_comp_hom, CommAlgCat.forget₂_commRingCat_map, preadditiveCoyoneda_obj, BialgCat.MonoidalCategory.inducingFunctorData_εIso, RingCat.FilteredColimits.forget₂SemiRing_preservesFilteredColimits, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, GrpCat.forget₂Mon_preservesLimitsOfSize, CommGrpCat.forget₂Group_preservesLimitsOfShape, alexDiscEquivPreord_functor, CommGrpCat.forget₂_map, SemiRingCat.forget₂Mon_preservesLimits, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, CommSemiRingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier, ShortComplex.exact_iff_exact_map_forget₂, SemimoduleCat.forget₂_obj, FinBoolAlg.forgetToBoolAlgFaithful, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, SemimoduleCat.forget₂_map, ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier, TopModuleCat.hom_forget₂_TopCat_map, Action.forget₂_additive, SemiRingCat.forget₂_addCommMonCat_map, ProfiniteGrp.diagram_obj, ModuleCat.forget₂_map, AddGrpCat.forget₂Mon_preservesLimits, PreGaloisCategory.functorToAction_comp_forget₂_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_arg 📖	mathematical	—	DFunLike.coe ConcreteCategory.hom	—	—
congr_fun 📖	mathematical	—	DFunLike.coe ConcreteCategory.hom	—	—
forget_obj 📖	mathematical	—	Functor.obj types forget ToType	—	—
forget₂_comp_apply 📖	mathematical	—	DFunLike.coe Functor.obj forget₂ ConcreteCategory.hom Functor.map CategoryStruct.comp Category.toCategoryStruct	—	Functor.map_comp comp_apply
forget₂_faithful 📖	mathematical	—	Functor.Faithful forget₂	—	Eq.faithful_of_comp instFaithfulForget HasForget₂.forget_comp
hom_isIso 📖	mathematical	—	IsIso types DFunLike.coe ConcreteCategory.hom	—	Iso.isIso_hom
instFaithfulForget 📖	mathematical	—	Functor.Faithful types forget	—	ConcreteCategory.coe_ext

CategoryTheory.ConcreteCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_map_eq_coe 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.forget DFunLike.coe hom	—	—
forget₂_comp_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.forget₂ hom CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Functor.map_comp CategoryTheory.comp_apply

CategoryTheory.FullSubcategory

Definitions

Name	Category	Theorems
hasForget₂ 📖	CompOp	7 math math: FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG

CategoryTheory.HasForget₂

Definitions

Name	Category	Theorems
forget₂ 📖	CompOp	17 math math: BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, HeytAlg.hasForgetToLat_forget₂_map, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, BoolAlg.hasForgetToBoolRing_forget₂_map, HeytAlg.hasForgetToLat_forget₂_obj_str, HeytAlg.hasForgetToLat_forget₂_obj_carrier, BoolAlg.hasForgetToHeytAlg_forget₂_map, CommRingCat.commMon_forget₂_obj_coe, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, BoolRing.hasForgetToBoolAlg_forget₂_map, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, forget_comp, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, CommRingCat.commMon_forget₂_map, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str
mk' 📖	CompOp	—
trans 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_comp 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.types forget₂ CategoryTheory.forget	—	—

CategoryTheory.InducedCategory

Definitions

Name	Category	Theorems
hasForget₂ 📖	CompOp	—

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
naturality_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.ConcreteCategory.hom app CategoryTheory.Functor.map	—	CategoryTheory.Functor.map_comp CategoryTheory.Functor.congr_map naturality

CategoryTheory.Types

Definitions

Name	Category	Theorems
instConcreteCategory 📖	CompOp	48 math math: instIsCorepresentableForgetTypeHom, CategoryTheory.Presheaf.instIsLocallySurjectiveHomWhiskerRightOppositeForget, CategoryTheory.Sheaf.instIsLocallySurjectiveHomToImage, TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types, CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom, Opens.mayerVietorisSquare_X₃, instReflectsLimitsOfSizeForgetTypeHom, CategoryTheory.Sheaf.isLocallySurjective_iff_epi, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, CategoryTheory.Functor.imageSieve_eq_imageSieve, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, instFullForgetTypeHom, CondensedMod.isDiscrete_iff_isDiscrete_forget, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, instPreservesLimitsOfSizeForgetTypeHom, instIsEquivalenceForgetTypeHom, Opens.mayerVietorisSquare_X₂, CategoryTheory.Presheaf.isLocallyInjective_forget_iff, Opens.coe_mayerVietorisSquare_X₁, instPreservesColimitsOfSizeForgetTypeHom, hom_eq_coe, CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.Sheaf.isLocallyInjective_forget, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CondensedSet.isDiscrete_tfae, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, CategoryTheory.Presheaf.imageSieve_whisker_forget, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, CategoryTheory.Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage, CategoryTheory.Presheaf.isLocallySurjective_toPlus, CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify, TopCat.Presheaf.isGluing_iff_pairwise, Opens.mayerVietorisSquare'_toSquare, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHom, instReflectsColimitsOfSizeForgetTypeHom, CategoryTheory.Sheaf.instIsLocallyInjectiveHomImageι, CategoryTheory.Sieve.equalizer_eq_equalizerSieve, CategoryTheory.Sheaf.isLocallySurjective_iff_isIso, CategoryTheory.Presheaf.instIsLocallyInjectiveHomιOpposite, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CategoryTheory.Presheaf.isLocallyInjective_forget, CategoryTheory.instReflectsIsomorphismsForgetTypeHom
instFunLike 📖	CompOp	49 math math: instIsCorepresentableForgetTypeHom, CategoryTheory.Presheaf.instIsLocallySurjectiveHomWhiskerRightOppositeForget, CategoryTheory.Sheaf.instIsLocallySurjectiveHomToImage, TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types, CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom, Opens.mayerVietorisSquare_X₃, instReflectsLimitsOfSizeForgetTypeHom, CategoryTheory.Sheaf.isLocallySurjective_iff_epi, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, CategoryTheory.Functor.imageSieve_eq_imageSieve, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, instFullForgetTypeHom, CondensedMod.isDiscrete_iff_isDiscrete_forget, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, instPreservesLimitsOfSizeForgetTypeHom, instIsEquivalenceForgetTypeHom, Opens.mayerVietorisSquare_X₂, CategoryTheory.Presheaf.isLocallyInjective_forget_iff, Opens.coe_mayerVietorisSquare_X₁, instPreservesColimitsOfSizeForgetTypeHom, hom_eq_coe, CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.Sheaf.isLocallyInjective_forget, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CondensedSet.isDiscrete_tfae, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, CategoryTheory.Presheaf.imageSieve_whisker_forget, Mathlib.Tactic.Elementwise.forget_hom_Type, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, CategoryTheory.Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage, CategoryTheory.Presheaf.isLocallySurjective_toPlus, CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify, TopCat.Presheaf.isGluing_iff_pairwise, Opens.mayerVietorisSquare'_toSquare, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHom, instReflectsColimitsOfSizeForgetTypeHom, CategoryTheory.Sheaf.instIsLocallyInjectiveHomImageι, CategoryTheory.Sieve.equalizer_eq_equalizerSieve, CategoryTheory.Sheaf.isLocallySurjective_iff_isIso, CategoryTheory.Presheaf.instIsLocallyInjectiveHomιOpposite, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CategoryTheory.Presheaf.isLocallyInjective_forget, CategoryTheory.instReflectsIsomorphismsForgetTypeHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_eq_coe 📖	mathematical	—	CategoryTheory.ConcreteCategory.hom CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	—

---

← Back to Index