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	321 math math: CommSemiRingCat.forget_obj, instSmallCompMonCatForgetMonoidHomCarrierOfSmallObj, ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier, Types.instIsCorepresentableForgetTypeHom, ModuleCat.forget_preservesLimits, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, Presheaf.instIsLocallySurjectiveHomWhiskerRightOppositeForget, AddGrpCat.forget_grp_preserves_epi, GrpWithZero.forget_map, Presieve.FamilyOfElements.isCompatible_map_smul, CommRingCat.forget_preservesLimitsOfSize, CommRingCat.forgetReflectIsos, ModuleCat.forget_preservesLimitsOfSize, instSmallCompGrpCatForgetMonoidHomCarrierOfSmallObj, GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms, instFaithfulForget, Profinite.forget_preservesLimits, AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits, TopCat.coe_of_of, CommMonCat.forget_preservesLimitsOfShape, AddMonObj.ofRepresentableBy_add, MonCat.forget_map, MonCat.forget_reflects_isos, whiskering_linearCoyoneda, yonedaAddMonObjIsoOfRepresentableBy_hom_app_hom_apply, 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, TopCat.Sheaf.exact_iff_stalkFunctor_map_exact, 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, GrothendieckTopology.sheafifyCompIso_inv_eq_sheafifyLift, AlgebraicGeometry.Scheme.forgetToTop_comp_forget, 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, Rep.forget_map, 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, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, DistLat.forget_map, yonedaAddMonObjIsoOfRepresentableBy_inv_app_hom_apply, Rep.forget_obj, 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, GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, 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, 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, LightCondensed.forget_map_hom_app, 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₁, TopCat.Sheaf.IsFlasque.epi_of_shortExact, GrpCat.hasLimit_iff_small_sections, AddCommGrpCat.μ_forget_apply, MonCat.forget_isCorepresentable, Types.instPreservesColimitsOfSizeForgetTypeHom, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, PresheafOfModules.freeAdjunctionUnit_app, Presheaf.isLocallySurjective_iff_whisker_forget, Preord.forget_map, Sheaf.isLocallyInjective_forget, forget_obj, TopCat.Sheaf.sections_exact_of_left_exact, 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, 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, FintypeCat.instFullForgetHomObjFinite, Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomObjFinite, 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, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, 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, TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, AddCommMonCat.instIsRightAdjointForgetAddMonoidHomCarrier, SemimoduleCat.forget_map, essImage_yonedaAddMon, 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, 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, GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, 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, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb, HeytAlg.forget_map, Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomObjFinite, Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, SheafOfModules.pushforwardSections_coe, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, AddMonObj.ofRepresentableBy_zero, 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, Rep.reflectsIsomorphisms_forget, 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, 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	326 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, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, 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, ShortComplex.ShortExact.d_eq_zero_of_f_eq_d_apply, SemilatInfCat_dual_comp_forget_to_partOrd, Rep.preservesLimits_forget, 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, FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, bddOrd_dual_comp_forget_to_bipointed, groupHomology.π_comp_H0Iso_hom_assoc, 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, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, ModuleCat.smul_naturality, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, 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, Rep.instEpiModuleCatAppCoinvariantsMk, CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier, PresheafOfModules.Monoidal.tensorObj_map_tmul, CommBialgCat.forget₂_commAlgCat_obj, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, 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, ModuleCat.forget₂_map_homMk, distLat_dual_comp_forget_to_Lat, Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, RingCat.forget₂SemiRing_preservesLimitsOfSize, groupHomology.coinvariantsMk_comp_H0Iso_inv, 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, ShortComplex.i_cyclesMk, bddOrd_dual_comp_forget_to_partOrd, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, ModuleCat.forget₂_obj, SemiRingCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, AlgCat.forget₂Module_preservesLimitsOfSize, GrpCat.forget₂Mon_preservesLimits, CoalgCat.MonoidalCategory.inducingFunctorData_μIso, CoalgCat.MonoidalCategory.inducingFunctorData_εIso, Rep.coinvariantsFunctor_hom_ext_iff, 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, QuadraticModuleCat.forget₂_map_associator_hom, CommRingCat.forget₂CommSemiRing_preservesLimits, AddCommGrpCat.forget₂AddGroup_preservesLimits, partOrdEmb_dual_comp_forget_to_pardOrd, groupHomology.d₁₀_comp_coinvariantsMk, ModuleCat.smulNatTrans_apply_app, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, ConcreteCategory.forget₂_preservesEpimorphisms, HomologicalComplex.i_cyclesMk, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, bddLat_dual_comp_forget_to_semilatSupCat, CommRingCat.forgetToRingCat_obj, AddGrpCat.forget₂_map_ofHom, ShortComplex.ShortExact.δ_apply', 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, Rep.preservesColimits_forget, 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, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, 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, Rep.coinvariantsAdjunction_unit_app, CommRingCat.FilteredColimits.forget₂Ring_preservesFilteredColimits, Rep.coinvariantsMk_app_hom, Rep.forget₂_moduleCat_obj, 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, groupHomology.pOpcycles_comp_opcyclesIso_hom, BialgCat.MonoidalCategory.inducingFunctorData_μIso, GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier, Lat_dual_comp_forget_to_partOrd, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, PresheafOfModules.Monoidal.tensorHom_app, RingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map, Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, ModuleCat.reflectsColimitsOfShape, ModuleCat.homMk_hom_apply, finBoolAlg_dual_comp_forget_to_finBddDistLat, ModuleCat.forget₂AddCommGroup_reflectsLimitOfSize, AlexDisc.forgetToTop_full, CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, completeLat_dual_comp_forget_to_bddLat, PresheafOfModules.Derivation'.app_apply, CoalgCat.forget₂_map, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, ShortComplex.SnakeInput.δ_apply', ShortComplex.ShortExact.δ_apply, TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, Rep.forget₂_moduleCat_map, AlgCat.forget₂Module_preservesLimits, TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, Rep.instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier, 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, groupHomology.π_comp_H0Iso_hom, AddCommGrpCat.forget₂_commMonCat_map_ofHom, TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, CommMonCat.forget₂Mon_preservesLimits, AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize, groupHomology.H0π_comp_H0Iso_hom, AlgCat.forget₂_module_map, FDRep.forget₂_ρ, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, 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, PresheafOfModules.HasDifferentials.exists_universal_derivation, CommGrpCat.instReflectsIsomorphismsGrpCatForget₂MonoidHomCarrierCarrier, Action.isContinuous_def, FinBoolAlg.forgetToBoolAlg_full, CommGrpCat.forget₂_grp_map_ofHom, ProfiniteGrp.diagram_map, ModuleCat.forget₂AddCommGroup_preservesLimit, groupHomology.shortComplexH0_g, 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₂, groupHomology.d₁₀_comp_coinvariantsMk_assoc, forget₂_faithful, SemilatSupCat_dual_comp_forget_to_partOrd, groupHomology.H0π_comp_H0Iso_hom_assoc, CommRingCat.forgetToRingCat_map_hom, linOrd_dual_comp_forget_to_Lat, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, SemiRingCat.forget₂_monCat_map, ModuleCat.HasColimit.reflectsColimit, BialgCat.forget₂_algebra_obj, UniformSpaceCat.extensionHom_val, Rep.coinvariantsAdjunction_homEquiv_apply_hom, SimplexCategory.toCat_map, PresheafOfModules.germ_smul, AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier, pointedToTwoPSnd_comp_forget_to_bipointed, SemilatSupCat.coe_forget_to_partOrd, partOrd_dual_comp_forget_to_preord, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Action.forget₂_linear, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, 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, groupHomology.H0π_comp_H0Iso_hom_apply, GrpCat.forget₂Mon_preservesLimitsOfSize, CommGrpCat.forget₂Group_preservesLimitsOfShape, alexDiscEquivPreord_functor, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, CommGrpCat.forget₂_map, SemiRingCat.forget₂Mon_preservesLimits, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, CommSemiRingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier, ShortComplex.exact_iff_exact_map_forget₂, SemimoduleCat.forget₂_obj, FinBoolAlg.forgetToBoolAlgFaithful, 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	55 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, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, 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, CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map, 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, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map, TopCat.Presheaf.isGluing_iff_pairwise, Opens.mayerVietorisSquare'_toSquare, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map, CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHom, instReflectsColimitsOfSizeForgetTypeHom, CategoryTheory.Sheaf.instIsLocallyInjectiveHomImageι, CategoryTheory.Sieve.equalizer_eq_equalizerSieve, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map, CategoryTheory.Sheaf.isLocallySurjective_iff_isIso, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map, CategoryTheory.Presheaf.instIsLocallyInjectiveHomιOpposite, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CategoryTheory.Presheaf.isLocallyInjective_forget, CategoryTheory.instReflectsIsomorphismsForgetTypeHom, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map
instFunLike 📖	CompOp	125 math math: instIsCorepresentableForgetTypeHom, CategoryTheory.Presheaf.instIsLocallySurjectiveHomWhiskerRightOppositeForget, CategoryTheory.PreGaloisCategory.mulAction_def, CategoryTheory.Sheaf.instIsLocallySurjectiveHomToImage, CategoryTheory.PreGaloisCategory.action_ext_of_isGalois, TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types, CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom, CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π, Opens.mayerVietorisSquare_X₃, FunctorToFintypeCat.naturality, LightCondensed.finYoneda_map, instReflectsLimitsOfSizeForgetTypeHom, CategoryTheory.Sheaf.isLocallySurjective_iff_epi, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, CategoryTheory.Functor.imageSieve_eq_imageSieve, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, CategoryTheory.PreGaloisCategory.connected_component_unique, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, Condensed.finYoneda_map, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family, CategoryTheory.PreGaloisCategory.toAut_hom_app_apply, FintypeCat.toProfinite_map_hom_hom_apply, instFullForgetTypeHom, CategoryTheory.Limits.FintypeCat.productEquiv_apply, CondensedMod.isDiscrete_iff_isDiscrete_forget, FintypeCat.comp_apply, FintypeCat.uSwitchEquiv_naturality, FintypeCat.equivEquivIso_symm_apply_symm_apply, CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, FintypeCat.hom_ext_iff, FintypeCat.id_apply, CategoryTheory.PreGaloisCategory.functorToContAction_map, CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois, Action.FintypeCat.toEndHom_apply, CategoryTheory.PreGaloisCategory.evaluation_aut_bijective_of_isGalois, FintypeCat.toLightProfinite_map_hom_hom_apply, instPreservesLimitsOfSizeForgetTypeHom, instIsEquivalenceForgetTypeHom, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app, Opens.mayerVietorisSquare_X₂, CategoryTheory.Presheaf.isLocallyInjective_forget_iff, Opens.coe_mayerVietorisSquare_X₁, instPreservesColimitsOfSizeForgetTypeHom, FintypeCat.equivEquivIso_symm_apply_apply, hom_eq_coe, CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply, Action.FintypeCat.quotientToEndHom_mk, CategoryTheory.Sheaf.isLocallyInjective_forget, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.PreGaloisCategory.fiber_in_connected_component, FintypeCat.instFullForgetHomObjFinite, CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomObjFinite, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, CondensedSet.isDiscrete_tfae, CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber, FintypeCat.hom_apply, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi, CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, CategoryTheory.Presheaf.imageSieve_whisker_forget, Mathlib.Tactic.Elementwise.forget_hom_Type, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, CategoryTheory.PreGaloisCategory.comp_autMap_apply, CategoryTheory.Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, Action.FintypeCat.quotientToQuotientOfLE_hom_mk, CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage, CategoryTheory.Presheaf.isLocallySurjective_toPlus, FintypeCat.inv_hom_id_apply, CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map, CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois, TopCat.Presheaf.isGluing_iff_pairwise, CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber, CategoryTheory.PreGaloisCategory.autEmbedding_range, CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected, CategoryTheory.PreGaloisCategory.mulAction_naturality, Opens.mayerVietorisSquare'_toSquare, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality, CategoryTheory.Limits.FintypeCat.jointly_surjective, CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map, CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj, CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHom, FintypeCat.uSwitchEquiv_symm_naturality, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.PreGaloisCategory.endEquivAutGalois_π, instReflectsColimitsOfSizeForgetTypeHom, FintypeCat.hom_inv_id_apply, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, CategoryTheory.Sheaf.instIsLocallyInjectiveHomImageι, CategoryTheory.Sieve.equalizer_eq_equalizerSieve, CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomObjFinite, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map, CategoryTheory.Sheaf.isLocallySurjective_iff_isIso, CategoryTheory.PreGaloisCategory.exists_galois_representative, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map, CategoryTheory.Presheaf.instIsLocallyInjectiveHomιOpposite, CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app, CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CategoryTheory.Presheaf.isLocallyInjective_forget, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, FintypeCat.homMk_apply, CategoryTheory.instReflectsIsomorphismsForgetTypeHom, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map, Action.FintypeCat.ofMulAction_apply, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq

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