FullSubcategory

📁 Source: Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

Statistics

Metric	Count
Definitions FullSubcategory, category, obj, fullyFaithfulι, fullyFaithfulιOfLE, homMk, isoMk, liftCompιIso, liftCompιOfLEIso, ι, ιOfLE, ιOfLECompιIso	12
Theorems comp_def, comp_hom, comp_hom_assoc, ext, ext_iff, id_def, id_hom, property, faithful_ι, faithful_ιOfLE, full_ι, full_ιOfLE, homMk_hom, homMk_surjective, hom_ext, hom_ext_iff, instFaithfulFullSubcategoryLift, instFullFullSubcategoryLift, isoHom_inv_id_hom, isoHom_inv_id_hom_assoc, isoInv_hom_id_hom, isoInv_hom_id_hom_assoc, isoMk_hom, isoMk_inv, lift_map, lift_obj_obj, prop_ι_obj, ιOfLE_map, ιOfLE_obj_obj, ι_map, ι_obj, ι_obj_lift_map, ι_obj_lift_obj	33
Total	45

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
FullSubcategory 📖	CompData	598 math math: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val, preservesEpimorphisms_ι_of_isNormalMonoCategory, CategoryTheory.isSeparating_iff_epi, isoMk_hom, CategoryTheory.LeftExactFunctor.ofExact_map, ColimitOfShape.toCostructuredArrow_obj, SimplexCategory.Truncated.δ₂_two_comp_σ₂_one_assoc, CategoryTheory.Equivalence.congrFullSubcategory_inverse, instCommShiftHomFunctorLiftCompιIso, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom, LinearMap.id_fgModuleCat_comp, CategoryTheory.eval_app, CategoryTheory.ExactFunctor.forget_map, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_down, CategoryTheory.locallySmall_fullSubcategory, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom, CategoryTheory.LeftExactFunctor.forget_map, FGModuleCat.hom_hom_id, CategoryTheory.Functor.fullSubcategoryInclusionLinear, rightUnitor_def, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app, HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_hom_app, Condensed.hom_ext_iff, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_hom, FullSubcategory.comp_hom_assoc, FDRep.endRingEquiv_symm_comp_ρ, CategoryTheory.MonoOver.isIso_left_iff_subobjectMk_eq, CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj_obj, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero, CondensedSet.topCatAdjunctionUnit_hom_app_apply, CategoryTheory.Functor.sheafPushforwardContinuous_map_hom_app, lift_obj_obj, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom_hom, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv_hom, tStructure_isGE_iff, SheafOfModules.forgetToSheafModuleCat_map_hom, tensorUnit_obj, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm_assoc, topEquivalence_counitIso, CondensedSet.hom_naturality_apply, CategoryTheory.typeEquiv_functor_map_hom_app, lift_map, CategoryTheory.sheafificationNatIso_hom_app_hom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj, CategoryTheory.instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι, SimplexCategory.Truncated.Hom.tr_comp, CategoryTheory.Functor.fullSubcategoryInclusion_additive, full_ιOfLE, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_hom, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_hom_app, CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, LinearMap.comp_id_fgModuleCat, CategoryTheory.constantCommuteCompose_hom_app_val, CategoryTheory.Equivalence.congrFullSubcategory_counitIso, eqToHom_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, TopCat.Sheaf.pushforward_map, CochainComplex.Plus.mono_iff, CategoryTheory.Sheaf.adjunction_unit_app_hom, SSet.Truncated.Edge.CompStruct.d₂, SSet.Truncated.liftOfStrictSegal.hδ'₂, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom, SimplexCategory.Truncated.δ₂_one_comp_σ₂_one, tensorHom_def, CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac', AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_hom, CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom, SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two_assoc, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, faithful_ι, isoHom_inv_id_hom, Condensed.epi_iff_surjective_on_stonean, CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_hom_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val, isCoseparating_iff_mono, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, CategoryTheory.RightExactFunctor.whiskeringLeft_map_app, CategoryTheory.MonoOver.mkArrowIso_hom_hom_left, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_hom_app, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_app, ι_η, CategoryTheory.Adjunction.sheafPushforwardContinuous_unit_app_hom_app, TopCat.Sheaf.id_app, CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app, CategoryTheory.MonoOver.isIso_hom_left_iff_subobjectMk_eq, CategoryTheory.RightExactFunctor.whiskeringRight_map_app, Condensed.id_hom, CategoryTheory.OrthogonalReflection.isRightAdjoint_ι, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRel, full_ι, fullSubcategoryCongr_inverse, CategoryTheory.AdditiveFunctor.ofLeftExact_map, CategoryTheory.RightExactFunctor.ofExact_map_hom, CategoryTheory.IsCofiltered.small_fullSubcategory_cofilteredClosure, CategoryTheory.LeftExactFunctor.whiskeringRight_map_app, FGModuleCat.hom_comp, CategoryTheory.MorphismProperty.FunctorsInverting.id_hom, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom, CategoryTheory.Functor.IsCoverDense.sheafIso_hom_hom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv_hom, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm, SimplexCategory.Truncated.Hom.tr_comp', CategoryTheory.Sheaf.imageι_hom, ι_map, instAdditiveFullSubcategoryShiftFunctor, LightCondensed.comp_hom, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map, CategoryTheory.AdditiveFunctor.ofRightExact_map, CategoryTheory.AdditiveFunctor.ofExact_map, fullSubcategoryCongr_unitIso, homMk_zero, CategoryTheory.sheafBotEquivalence_inverse_map_hom, FGModuleCat.FGModuleCatEvaluation_apply, CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app, FintypeCat.comp_hom, topEquivalence_unitIso, CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow, IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms, SSet.Truncated.spine_map_subinterval, CategoryTheory.RightExactFunctor.forget_map, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app_assoc, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app, instFullFullSubcategoryLift, FintypeCat.incl_map, CategoryTheory.Functor.essImage_ι_comp, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app, CategoryTheory.Functor.IsCoverDense.sheafIso_inv_hom, hasLimit_parallelPair_comp_ι, CategoryTheory.plusPlusSheaf_map_hom, CategoryTheory.presheaf_mono_of_mono, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero_assoc, HomotopicalAlgebra.instIsMultiplicativeFullSubcategoryWeakEquivalences, CategoryTheory.IsFiltered.instIsFilteredOrEmptyFullSubcategoryFilteredClosure, topCatToSheafCompHausLike_map_hom_app, ι_ε, SheafOfModules.restrictScalars_obj_val, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_app, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom, CategoryTheory.isCoseparating_iff_mono, CondensedMod.epi_iff_surjective_on_stonean, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app, FGModuleCat.hom_id, CategoryTheory.Localization.whiskeringLeftFunctor'_eq, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val, CategoryTheory.Sheaf.χ_hom, CategoryTheory.Functor.partialRightAdjointHomEquiv_map, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, CompHausLike.LocallyConstant.counit_app_hom_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom, CategoryTheory.instMonoFunctorOppositeHomFullSubcategoryIsSheafOfHasWeakSheafifyOfSheaf, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj_obj, FullSubcategory.comp_def, CondensedSet.epi_iff_surjective_on_stonean, SSet.Truncated.StrictSegal.spine_δ_arrow_lt, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_obj, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map, CategoryTheory.Sheaf.toImage_hom, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_symm_apply, CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app, CategoryTheory.Sheaf.image_obj, CategoryTheory.equivYoneda'_hom_hom, CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ_assoc, CategoryTheory.Functor.toEssImage_map_hom, TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective, CategoryTheory.Functor.mapContAction_map, CategoryTheory.typeEquiv_counitIso_hom_app_hom_app, FDRep.hom_hom_action_ρ, IsConservativeFamilyOfPoints.over, CategoryTheory.instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, CategoryTheory.ExactFunctor.whiskeringLeft_map_app, CategoryTheory.essentiallySmall_fullSubcategory_mem, CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_hom_app, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom, SSet.Truncated.spine_map_vertex, CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_hom_app, CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono, ι_obj, CategoryTheory.IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, FGModuleCat.FGModuleCatCoevaluation_apply_one, CategoryTheory.LeftExactFunctor.ofExact_map_hom, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step, TopCat.Presheaf.stalk_mono_of_mono, TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective, CompHausLike.LocallyConstant.functor_map_hom, CategoryTheory.Functor.mapGrpFunctor_map_app, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', SSet.Truncated.Edge.src_eq, CategoryTheory.Limits.hasLimit_of_closedUnderLimits, CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj_obj, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app, instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, instMonoidalLinearFullSubcategory, CategoryTheory.ExactFunctor.whiskeringLeft_obj_map, Condensed.comp_val, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, CondensedMod.hom_naturality_apply, HomotopicalAlgebra.instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences, CategoryTheory.Equivalence.congrFullSubcategory_unitIso, TannakaDuality.FiniteGroup.equivApp_inv, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_map_hom, tensorObj_obj, SSet.Truncated.StrictSegal.spine_δ_arrow_gt, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map, TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective, Condensed.epi_iff_locallySurjective_on_compHaus, CategoryTheory.Sheaf.adjunction_counit_app_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, LightCondensed.forget_map_hom_app, CategoryTheory.IsCofiltered.instIsCofilteredOrEmptyFullSubcategoryCofilteredClosure, CategoryTheory.MonoOver.w, CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom_assoc, IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type, CategoryTheory.Sheaf.ΓObjEquivSections_naturality_symm, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Sheaf.isLocallyInjective_iff_injective, TannakaDuality.FiniteGroup.equivApp_hom, ι_δ, isSeparating_iff_epi, TopCat.Sheaf.comp_app, CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, instSmallFullSubcategoryOfSmall, TopCat.Sheaf.IsFlasque.epi_of_shortExact, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π_assoc, SimplexCategory.Truncated.Hom.tr_id, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_hom_app, ihom_obj, CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits, fullSubcategoryCongr_counitIso, HomotopicalAlgebra.instWeakEquivalenceMapFullSubcategoryι, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_hom, SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two, CompHausLike.LocallyConstant.adjunction_left_triangle, CategoryTheory.extensiveTopology.isLocallySurjective_iff, TopCat.Sheaf.sections_exact_of_left_exact, CategoryTheory.Sheaf.truth_hom, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_assoc, AlgebraicGeometry.AffineScheme.forgetToScheme_map, SheafOfModules.restrictScalars_map_val, CategoryTheory.sheafificationNatIso_inv_app_hom, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc, IsStrongGenerator.extremalEpi_coproductFrom, instIsTriangulatedFullSubcategoryι, instHasCokernelsFullSubcategoryOfIsClosedUnderCokernels, IsCoseparating.mono_productTo, CategoryTheory.ExactFunctor.whiskeringRight_obj_obj_obj, SSet.Truncated.liftOfStrictSegal.hσ'₀, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map_comp, hasColimit_parallelPair_comp_ι, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_functor, SSet.Truncated.StrictSegal.spineToSimplex_vertex, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, CategoryTheory.typeEquiv_counitIso_inv_app_hom_app, SSet.Truncated.StrictSegal.spine_δ_vertex_ge, instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1, CategoryTheory.typeEquiv_inverse_map, CategoryTheory.AdditiveFunctor.forget_map, SheafOfModules.pushforward_map_val, SSet.Truncated.StrictSegal.spineToSimplex_edge, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, initial_ι, SSet.Truncated.spine_arrow, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom, CategoryTheory.Abelian.Preradical.isIso_toColon_hom_left_app_iff, SSet.Truncated.liftOfStrictSegal.hδ'₁, SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero, LightCondSet.topCatAdjunctionUnit_hom_app_apply, FGModuleCat.Iso.conj_eq_conj, FullSubcategory.id_def, CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_hom_app, CategoryTheory.Sheaf.adjunction_unit_app_val, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, ihom_map, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, SimplexCategory.Truncated.Hom.ext_iff, SSet.Truncated.Edge.mk'_edge, preservesMonomorphisms_ι_of_isNormalEpiCategory, CategoryTheory.RightExactFunctor.ofExact_map, IsStrongGenerator.isDense_colimitsCardinalClosure_ι, Alexandrov.lowerCone_π_app, isoHom_inv_id_hom_assoc, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app, SSet.Truncated.StrictSegal.spineToSimplex_arrow, FGModuleCat.hom_hom_comp, LightCondensed.hom_ext_iff, CategoryTheory.sheafificationIso_inv_hom, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc, CategoryTheory.MonoOver.isIso_iff_isIso_hom_left, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app, preservesCokernels_ι, HomotopicalAlgebra.BifibrantObject.homRel_iff_leftHomotopyRel, whiskerLeft_def, SSet.Truncated.spine_vertex, CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, FGModuleCat.hom_ext_iff, tStructure_isLE_iff, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, FintypeCat.comp_hom_assoc, CategoryTheory.IsFiltered.instEssentiallySmallFullSubcategoryFilteredClosure, LightCondSet.hom_naturality_apply, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv', instIsEquivalenceFullSubcategoryIsoClosureιOfLE, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, ι_μ, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, PresheafOfModules.sheafifyMap_val, IsConservativeFamilyOfPoints.jointlyFaithful, SSet.Truncated.Edge.id_edge, SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero, ι_map_top, whiskerRight_def, CategoryTheory.ExactFunctor.whiskeringRight_map_app, CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_hom_app, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, FintypeCat.hom_apply, leftUnitor_def, SSet.Truncated.Path.arrow_src, CategoryTheory.sheafCompose_map_hom, CategoryTheory.MonoOver.inf_map_app, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app_assoc, CategoryTheory.sheafificationIso_hom_hom, CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure, CategoryTheory.MonoOver.mkArrowIso_inv_hom_left, CategoryTheory.instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction, HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans_app, LightCondMod.hom_naturality_apply, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom_hom, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv', ColimitOfShape.toCostructuredArrow_map, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, prop_ι_obj, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply, CategoryTheory.Functor.essImage.liftFunctorCompIso_inv_app, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, CategoryTheory.MonoOver.w_assoc, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, instHasZeroObjectFullSubcategoryOfContainsZero, CategoryTheory.MonoOver.lift_map_hom, SSet.Truncated.StrictSegal.spine_δ_arrow_eq, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right_assoc, SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero_assoc, homMk_surjective, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso, SSet.Truncated.Path₁.arrow_tgt, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_hom_app, associator_def, SheafOfModules.toSheaf_map_hom, instMonoidalPreadditiveFullSubcategory, CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom, IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, ιOfLE_map, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom_hom, SSet.Truncated.StrictSegal.spineToSimplex_interval, CategoryTheory.Functor.mapCommGrpFunctor_map, SimplexCategory.Truncated.δ₂_one_comp_σ₂_one_assoc, CondensedMod.epi_iff_locallySurjective_on_compHaus, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app, SimplexCategory.Truncated.Hom.tr_comp_assoc, isoMk_inv, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app, SSet.Truncated.Path.arrow_tgt, CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_hom_app, CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp_assoc, zero_hom, Alexandrov.lowerCone_pt, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val, CategoryTheory.Functor.instAdditiveFullSubcategoryLift, fullSubcategoryCongr_functor, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.Equivalence.sheafCongr.functor_map_hom_app, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app, CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι, TopCat.Sheaf.eq_app_of_locally_eq, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, isFiltered_costructuredArrow_colimitsCardinalClosure_ι, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_hom_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_hom_app, SSet.Truncated.liftOfStrictSegal.hδ'₀, preservesKernels_ι, FullSubcategory.comp_hom, CategoryTheory.sheafificationAdjunction_counit_app_val, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp, ιOfLE_ε, FDRep.of_ρ, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app, exists_equivalence_iff, FGModuleCat.FGModuleCatEvaluation_apply', CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_hom_app, CategoryTheory.Equivalence.congrFullSubcategory_functor, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, LightCondSet.topCatAdjunctionUnit_hom_app, instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, SSet.OneTruncation₂.nerveHomEquiv_apply, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val_assoc, CategoryTheory.Sheaf.Hom.add_app, instIsTriangulatedFullSubcategory, HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans_app, AlgebraicGeometry.tilde.toOpen_map_app_assoc, CategoryTheory.constantCommuteCompose_hom_app_hom, ιOfLE_obj_obj, CategoryTheory.Functor.toEssImageCompι_inv_app, CategoryTheory.Sheaf.adjunction_counit_app_hom, ι_obj_lift_map, LightCondensed.id_val, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj_obj, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, SSet.Truncated.liftOfStrictSegal.hσ'₁, SSet.Truncated.Edge.CompStruct.d₀, hom_ext_iff, CategoryTheory.Sheaf.hom_ext_iff, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, Condensed.comp_hom, CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_hom_app, CategoryTheory.Functor.toEssImageCompι_hom_app, instHasFiniteProductsFullSubcategoryOfIsClosedUnderFiniteProducts, instFaithfulFullSubcategoryLift, CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_hom_app, CategoryTheory.GrothendieckTopology.yoneda_map_hom, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map, CondensedSet.toTopCatMap_hom_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc, ι_obj_lift_obj, LimitOfShape.toStructuredArrow_obj, LightCondensed.comp_val, LightCondensed.id_hom, CategoryTheory.sheafBotEquivalence_counitIso, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, CategoryTheory.AdditiveFunctor.ofExact_map_hom, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, SSet.Truncated.Path₁.arrow_src, CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι, SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero_assoc, LightCondensed.underlying_map, CategoryTheory.subterminalInclusion_map, SSet.Truncated.Edge.CompStruct.d₁, faithful_ιOfLE, Condensed.underlying_map, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, LimitOfShape.toStructuredArrow_map, CategoryTheory.Adjunction.sheafPushforwardContinuous_counit_app_hom_app, SimplexCategory.Truncated.δ₂_two_comp_σ₂_one, SSet.OneTruncation₂.id_edge, CategoryTheory.MorphismProperty.isCardinalAccessible_ι_isLocal, topEquivalence_inverse, CategoryTheory.GrothendieckTopology.map_yonedaEquiv, CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft_hom, CategoryTheory.coherentTopology.isLocallySurjective_iff, CategoryTheory.Sheaf.ΓObjEquivSections_naturality, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, topEquivalence_functor, LightCondSet.toTopCatMap_hom_apply, HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel, CondensedSet.epi_iff_locallySurjective_on_compHaus, CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_hom_app, CategoryTheory.IsCofiltered.instEssentiallySmallFullSubcategoryCofilteredClosure, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, CategoryTheory.GrothendieckTopology.uliftYoneda_map_hom_app_down, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm, CategoryTheory.ExactFunctor.whiskeringRight_obj_map, CategoryTheory.Functor.essImage.liftFunctor_map, TannakaDuality.FiniteGroup.ofRightFDRep_hom, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, CondensedSet.topCatAdjunctionUnit_hom_app, isoInv_hom_id_hom_assoc, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, TopCat.Sheaf.isLocallySurjective_iff_epi, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map, SSet.Truncated.StrictSegal.spine_δ_vertex_lt, SimplexCategory.Truncated.Hom.tr_comp'_assoc, IsSeparating.epi_coproductFrom, CategoryTheory.Functor.EssImageSubcategory.lift_def, ιOfLE_η, FGModuleCat.Iso.conj_hom_eq_conj, isEquivalence_ιOfLE_iff, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, CategoryTheory.Sheaf.ΓRes_naturality, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app, CategoryTheory.Limits.hasColimit_of_closedUnderColimits, CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom, homMk_hom, ιOfLE_μ, CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_hom_app, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, CategoryTheory.equivYoneda'_inv_hom, ContAction.res_map, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right, Condensed.id_val, TopCat.Presheaf.mono_iff_stalk_mono, FDRep.hom_action_ρ, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_app, CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_hom_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val, CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply, SheafOfModules.pushforward_obj_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom, CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom_hom, ιOfLE_δ, instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CategoryTheory.Functor.essImage_ext_iff, instHasKernelsFullSubcategoryOfIsClosedUnderKernels, Alexandrov.projSup_map, ihom_map_hom, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, isoInv_hom_id_hom, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one, CategoryTheory.Functor.partialRightAdjointHomEquiv_map_comp, FDRep.endRingEquiv_comp_ρ, FullSubcategory.id_hom, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom, HomotopicalAlgebra.instWeakEquivalenceHomFullSubcategory, IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms, CategoryTheory.GrothendieckTopology.yonedaEquiv_apply, instHasFiniteCoproductsFullSubcategoryOfIsClosedUnderFiniteCoproducts, SSet.Truncated.Edge.CompStruct.idCompId_simplex, CategoryTheory.MorphismProperty.isLocallyPresentable_isLocal, CategoryTheory.AdditiveFunctor.ofRightExact_map_hom, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app, HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel, CategoryTheory.yoneda'_map_hom, CategoryTheory.Equivalence.sheafCongr.inverse_map_hom_app, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_inverse, essSurj_ιOfLE_iff, isTriangulated_lift, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj_obj, CategoryTheory.RightExactFunctor.whiskeringRight_obj_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app, SSet.Truncated.Edge.tgt_eq, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom, CategoryTheory.MonoOver.isIso_iff_isIso_left, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map, CategoryTheory.Sheaf.isTerminalTerminal_from_hom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv_hom, CategoryTheory.MonoOver.instIsIsoLeftDiscretePUnitHomFullSubcategoryOverIsMono, CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_hom_app, CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext_iff, AlgebraicGeometry.tilde.toOpen_map_app
fullyFaithfulι 📖	CompOp	2 math math: CategoryTheory.Equivalence.congrFullSubcategory_counitIso, CategoryTheory.Equivalence.congrFullSubcategory_unitIso
fullyFaithfulιOfLE 📖	CompOp	—
homMk 📖	CompOp	47 math math: isoMk_hom, CategoryTheory.Functor.EssImageSubcategory.associator_inv_def, CategoryTheory.Functor.EssImageSubcategory.associator_hom_def, lift_map, tensorHom_def, CategoryTheory.Functor.mapContActionCongr_inv, CategoryTheory.RightExactFunctor.whiskeringLeft_map_app, CategoryTheory.RightExactFunctor.whiskeringRight_map_app, CategoryTheory.Functor.mapContActionCongr_hom, CategoryTheory.LeftExactFunctor.whiskeringRight_map_app, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map, homMk_zero, CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.PreGaloisCategory.functorToContAction_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.Functor.mapContAction_map, CategoryTheory.ExactFunctor.whiskeringLeft_map_app, ContAction.resCongr_hom, CategoryTheory.ExactFunctor.whiskeringLeft_obj_map, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, whiskerLeft_def, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, whiskerRight_def, CategoryTheory.ExactFunctor.whiskeringRight_map_app, ColimitOfShape.toCostructuredArrow_map, homMk_surjective, ContAction.resCongr_inv, ιOfLE_map, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, isoMk_inv, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, LimitOfShape.toStructuredArrow_map, CategoryTheory.ExactFunctor.whiskeringRight_obj_map, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map, CategoryTheory.Functor.EssImageSubcategory.lift_def, homMk_hom, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, ContAction.res_map, Alexandrov.projSup_map, CategoryTheory.RightExactFunctor.whiskeringRight_obj_map
isoMk 📖	CompOp	9 math math: isoMk_hom, rightUnitor_def, CategoryTheory.Functor.mapContActionCongr_inv, CategoryTheory.Functor.mapContActionCongr_hom, ContAction.resCongr_hom, leftUnitor_def, ContAction.resCongr_inv, associator_def, isoMk_inv
liftCompιIso 📖	CompOp	1 math math: instCommShiftHomFunctorLiftCompιIso
liftCompιOfLEIso 📖	CompOp	—
ι 📖	CompOp	68 math math: preservesEpimorphisms_ι_of_isNormalMonoCategory, CategoryTheory.isSeparating_iff_epi, ColimitOfShape.toCostructuredArrow_obj, CategoryTheory.Equivalence.congrFullSubcategory_inverse, instCommShiftHomFunctorLiftCompιIso, CategoryTheory.Functor.fullSubcategoryInclusionLinear, topEquivalence_counitIso, CategoryTheory.instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι, CategoryTheory.Functor.fullSubcategoryInclusion_additive, CategoryTheory.Equivalence.congrFullSubcategory_counitIso, CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal, CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor, faithful_ι, isCoseparating_iff_mono, ι_η, CategoryTheory.OrthogonalReflection.isRightAdjoint_ι, full_ι, ι_map, CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow, CategoryTheory.Functor.essImage_ι_comp, CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality, hasLimit_parallelPair_comp_ι, ι_ε, CategoryTheory.isCoseparating_iff_mono, ι_obj, CategoryTheory.IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Equivalence.congrFullSubcategory_unitIso, ι_δ, isSeparating_iff_epi, HomotopicalAlgebra.instWeakEquivalenceMapFullSubcategoryι, IsStrongGenerator.extremalEpi_coproductFrom, instIsTriangulatedFullSubcategoryι, IsCoseparating.mono_productTo, hasColimit_parallelPair_comp_ι, initial_ι, preservesMonomorphisms_ι_of_isNormalEpiCategory, IsStrongGenerator.isDense_colimitsCardinalClosure_ι, Alexandrov.lowerCone_π_app, preservesCokernels_ι, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, ι_μ, ι_map_top, CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι, ColimitOfShape.toCostructuredArrow_map, prop_ι_obj, CategoryTheory.equivEssImageOfReflective_inverse, Alexandrov.lowerCone_pt, CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι, isFiltered_costructuredArrow_colimitsCardinalClosure_ι, preservesKernels_ι, CategoryTheory.Equivalence.congrFullSubcategory_functor, CategoryTheory.Functor.toEssImageCompι_inv_app, ι_obj_lift_map, CategoryTheory.Functor.toEssImageCompι_hom_app, ι_obj_lift_obj, LimitOfShape.toStructuredArrow_obj, CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι, CategoryTheory.equivEssImageOfReflective_counitIso, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, LimitOfShape.toStructuredArrow_map, CategoryTheory.MorphismProperty.isCardinalAccessible_ι_isLocal, CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι, topEquivalence_functor, IsSeparating.epi_coproductFrom, isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι, CategoryTheory.Functor.essImage_ext_iff
ιOfLE 📖	CompOp	14 math math: full_ιOfLE, fullSubcategoryCongr_inverse, fullSubcategoryCongr_counitIso, instIsEquivalenceFullSubcategoryIsoClosureιOfLE, ιOfLE_map, fullSubcategoryCongr_functor, ιOfLE_ε, ιOfLE_obj_obj, faithful_ιOfLE, ιOfLE_η, isEquivalence_ιOfLE_iff, ιOfLE_μ, ιOfLE_δ, essSurj_ιOfLE_iff
ιOfLECompιIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful_ι 📖	mathematical	—	CategoryTheory.Functor.Faithful FullSubcategory FullSubcategory.category ι	—	CategoryTheory.Functor.FullyFaithful.faithful
faithful_ιOfLE 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.Functor.Faithful FullSubcategory FullSubcategory.category ιOfLE	—	CategoryTheory.Functor.FullyFaithful.faithful
full_ι 📖	mathematical	—	CategoryTheory.Functor.Full FullSubcategory FullSubcategory.category ι	—	CategoryTheory.Functor.FullyFaithful.full
full_ιOfLE 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.Functor.Full FullSubcategory FullSubcategory.category ιOfLE	—	CategoryTheory.Functor.FullyFaithful.full
homMk_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom FullSubcategory FullSubcategory.obj homMk	—	—
homMk_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FullSubcategory.obj FullSubcategory FullSubcategory.category homMk	—	—
hom_ext 📖	—	CategoryTheory.InducedCategory.Hom.hom FullSubcategory FullSubcategory.obj	—	—	CategoryTheory.InducedCategory.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom FullSubcategory FullSubcategory.obj	—	hom_ext
instFaithfulFullSubcategoryLift 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.Faithful FullSubcategory FullSubcategory.category lift	—	CategoryTheory.Functor.Faithful.of_comp_iso
instFullFullSubcategoryLift 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.Full FullSubcategory FullSubcategory.category lift	—	CategoryTheory.Functor.Full.of_comp_faithful_iso faithful_ι
isoHom_inv_id_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom FullSubcategory CategoryTheory.Iso.hom FullSubcategory.category CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.congr_map CategoryTheory.Iso.hom_inv_id
isoHom_inv_id_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom FullSubcategory CategoryTheory.Iso.hom FullSubcategory.category CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoHom_inv_id_hom
isoInv_hom_id_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom FullSubcategory CategoryTheory.Iso.inv FullSubcategory.category CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.congr_map CategoryTheory.Iso.inv_hom_id
isoInv_hom_id_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom FullSubcategory CategoryTheory.Iso.inv FullSubcategory.category CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' isoInv_hom_id_hom
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom FullSubcategory FullSubcategory.category isoMk homMk FullSubcategory.obj	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv FullSubcategory FullSubcategory.category isoMk homMk FullSubcategory.obj	—	—
lift_map 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.map FullSubcategory FullSubcategory.category lift homMk CategoryTheory.Functor.obj	—	—
lift_obj_obj 📖	mathematical	CategoryTheory.Functor.obj	FullSubcategory.obj CategoryTheory.Functor.obj FullSubcategory FullSubcategory.category lift	—	—
prop_ι_obj 📖	mathematical	—	CategoryTheory.Functor.obj FullSubcategory FullSubcategory.category ι	—	FullSubcategory.property
ιOfLE_map 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.Functor.map FullSubcategory FullSubcategory.category ιOfLE homMk FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom	—	—
ιOfLE_obj_obj 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	FullSubcategory.obj CategoryTheory.Functor.obj FullSubcategory FullSubcategory.category ιOfLE	—	—
ι_map 📖	mathematical	—	CategoryTheory.Functor.map FullSubcategory FullSubcategory.category ι CategoryTheory.InducedCategory.Hom.hom FullSubcategory.obj	—	—
ι_obj 📖	mathematical	—	CategoryTheory.Functor.obj FullSubcategory FullSubcategory.category ι FullSubcategory.obj	—	—
ι_obj_lift_map 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.map FullSubcategory FullSubcategory.category ι CategoryTheory.Functor.obj lift	—	—
ι_obj_lift_obj 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.obj FullSubcategory FullSubcategory.category ι lift	—	—

CategoryTheory.ObjectProperty.FullSubcategory

Definitions

Name	Category	Theorems
category 📖	CompOp	1537 math math: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val, SSet.OneTruncation₂.nerveEquiv_apply, CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, Condensed.finYoneda_obj, CategoryTheory.ObjectProperty.preservesEpimorphisms_ι_of_isNormalMonoCategory, CategoryTheory.isSeparating_iff_epi, CategoryTheory.ObjectProperty.isoMk_hom, CategoryTheory.GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso, CategoryTheory.LeftExactFunctor.ofExact_map, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, CategoryTheory.sheafBotEquivalence_functor, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, HomotopicalAlgebra.BifibrantObject.weakEquivalence_homMk_iff, SheafOfModules.pushforward_assoc, CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, instFaithfulFGAlgCatUliftFunctor, CategoryTheory.PreGaloisCategory.instT2SpaceAutFunctorFintypeCat, CategoryTheory.PreGaloisCategory.mulAction_def, CategoryTheory.Subobject.factors_iff, CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm, CategoryTheory.isIso_sheafificationAdjunction_counit, CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_obj, CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff, CategoryTheory.Functor.sheafPushforwardContinuousIso_inv, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem, SimplexCategory.Truncated.δ₂_two_comp_σ₂_one_assoc, LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, CategoryTheory.Equivalence.congrFullSubcategory_inverse, CategoryTheory.PreGaloisCategory.action_ext_of_isGalois, instEssentiallySmallFGAlgCat, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, CategoryTheory.ObjectProperty.instCommShiftHomFunctorLiftCompιIso, SSet.Truncated.tensor_map_apply_snd, HomotopicalAlgebra.BifibrantObject.inverts_iff_factors, SSet.oneTruncation₂_obj, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_obj_obj, instEssentiallySmallFGModuleCat, CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, CategoryTheory.equivEssImageOfReflective_unitIso, LightCondensed.ihomPoints_apply, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom, LinearMap.id_fgModuleCat_comp, CategoryTheory.ExactFunctor.forget_map, CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous, CategoryTheory.PreGaloisCategory.instContinuousSMulAutFintypeCatObjObjFinite, FDRep.char_tensor, CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂, CategoryTheory.Equivalence.sheafCongr_functor, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_down, HomotopicalAlgebra.CofibrantObject.homRel_equivalence_of_isFibrant_tgt, CategoryTheory.MonoOver.congr_unitIso, CompHausLike.LocallyConstant.functor_obj_obj, CategoryTheory.locallySmall_fullSubcategory, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom, CategoryTheory.LeftExactFunctor.forget_map, Profinite.Extend.cocone_pt, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, FGModuleCat.hom_hom_id, SSet.Truncated.sk.full, CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_map, CategoryTheory.MonoOver.mapIso_functor, SSet.Truncated.HomotopyCategory.descOfTruncation_comp, HomotopicalAlgebra.BifibrantObject.instLocallySmallHoCat, CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso, CategoryTheory.Limits.FintypeCat.hasFiniteColimits, CategoryTheory.Functor.fullSubcategoryInclusionLinear, CategoryTheory.ObjectProperty.rightUnitor_def, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app, SSet.Truncated.mapHomotopyCategory_homMk, HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_hom_app, CategoryTheory.Sheaf.instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, SSet.oneTruncation₂_map, FintypeCat.instFiniteIso, instFullFintypeCatProfiniteToProfinite, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply, SheafOfModules.pushforwardNatIso_inv, CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatDiscretePEmpty, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_hom, Profinite.Extend.functorOp_map, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms, comp_hom_assoc, FDRep.endRingEquiv_symm_comp_ρ, CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected, CategoryTheory.Sheaf.toImage_ι_assoc, CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj_obj, FintypeCat.uSwitch_map_uSwitch_map, CategoryTheory.GrothendieckTopology.overMapPullback_comp_id, SSet.Truncated.Path.mk₂_arrow, HomotopicalAlgebra.FibrantObject.homMk_homMk, FintypeCat.instFaithfulIncl, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, CategoryTheory.Functor.sheafPullbackConstruction.instPreservesFiniteLimitsSheafSheafPullback, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero, CategoryTheory.PreGaloisCategory.autEmbedding_injective, SSet.OneTruncation₂.nerveHomEquiv_id, CategoryTheory.MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, FGModuleCat.instHasColimitsOfShapeOfFinCategory, CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget, HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, CategoryTheory.nerve.functorOfNerveMap_map, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, CategoryTheory.Functor.EssImageSubcategory.associator_inv_def, CategoryTheory.Sheaf.isPullback_χ_truth, CategoryTheory.Functor.sheafPushforwardContinuous_map_hom_app, SSet.Truncated.StrictSegal.spine_spineToSimplex, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj, CategoryTheory.MonoOver.instIsRightAdjointOverForget, HomotopicalAlgebra.BifibrantObject.homMk_id, CategoryTheory.ObjectProperty.lift_obj_obj, CategoryTheory.Sheaf.classifier_χ, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom_hom, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, LightCondensed.finYoneda_obj, LightCondensed.isoFinYoneda_inv_app, CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_map, CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, TannakaDuality.FiniteGroup.forget_obj, CondensedMod.isDiscrete_tfae, CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq, CategoryTheory.instFullSheafSheafComposeOfFaithful, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv_hom, CategoryTheory.ObjectProperty.tStructure_isGE_iff, SheafOfModules.forgetToSheafModuleCat_map_hom, CategoryTheory.ObjectProperty.tensorUnit_obj, CategoryTheory.ObjectProperty.topEquivalence_counitIso, SSet.Truncated.sk_coreflective, FunctorToFintypeCat.naturality, CategoryTheory.PreGaloisCategory.toAutMulEquiv_isHomeomorph, Profinite.Extend.cone_π_app, CompHausLike.LocallyConstant.adjunction_counit, CategoryTheory.Functor.EssImageSubcategory.associator_hom_def, CategoryTheory.typeEquiv_functor_map_hom_app, CategoryTheory.ObjectProperty.lift_map, CategoryTheory.sheafificationNatIso_hom_app_hom, SSet.Truncated.Edge.map_fst, instFaithfulFintypeCatLightProfiniteToLightProfinite, CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos, CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply, LightCondensed.finYoneda_map, CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj, CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeUliftYoneda, CategoryTheory.instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι, SimplexCategory.Truncated.Hom.tr_comp, FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.Functor.Faithful.toEssImage, CategoryTheory.Functor.fullSubcategoryInclusion_additive, CategoryTheory.ObjectProperty.full_ιOfLE, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_sub_apply, CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite, CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCat, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CategoryTheory.MonoOver.isoMk_inv, CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app, Condensed.discrete_map, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_hom, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_hom_app, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, CategoryTheory.SimplicialObject.Truncated.cosk.full, CategoryTheory.MonoOver.mapIso_unitIso, LinearMap.comp_id_fgModuleCat, CategoryTheory.constantCommuteCompose_hom_app_val, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply, CategoryTheory.Equivalence.congrFullSubcategory_counitIso, CategoryTheory.ObjectProperty.eqToHom_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected, HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, CategoryTheory.Sheaf.isLocallySurjective_comp, FintypeCat.equivEquivIso_apply_hom, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, FintypeCat.instFiniteHom, CochainComplex.Plus.mono_iff, CategoryTheory.Sheaf.adjunction_unit_app_hom, SSet.Truncated.Edge.CompStruct.d₂, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, HomotopicalAlgebra.CofibrantObject.homMk_homMk, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesQuotientsByFiniteGroups, SSet.Truncated.liftOfStrictSegal.hδ'₂, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_obj, CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_obj_obj, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom, SimplexCategory.Truncated.δ₂_one_comp_σ₂_one, CategoryTheory.SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, CategoryTheory.ObjectProperty.tensorHom_def, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsMonomorphismsFintypeCat, CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply, HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism_functor, CategoryTheory.Sheaf.isLocallySurjective_iff_epi, CategoryTheory.Functor.mapContActionCongr_inv, CategoryTheory.AdditiveFunctor.ofExact_obj_fst, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac', CategoryTheory.PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat, CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_hom, LightCondensed.discrete_map, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, SSet.Truncated.Path.map_arrow, CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom, HomotopicalAlgebra.FibrantObject.toHoCat_map_eq_iff, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two_assoc, CategoryTheory.MonoOver.mapIso_counitIso, CategoryTheory.sheafToPresheaf_μ, CategoryTheory.SimplicialObject.Truncated.cosk.faithful, instIsEquivalenceFGModuleCatUlift, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.ObjectProperty.faithful_ι, CategoryTheory.ObjectProperty.isoHom_inv_id_hom, CategoryTheory.Presheaf.isLocallyInjective_presheafToSheaf_map_iff, CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_hom_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality, CategoryTheory.instEpiSheafTypeToImage, LightProfinite.Extend.cocone_ι_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val, HomotopicalAlgebra.FibrantObject.weakEquivalence_toHoCat_map_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, CategoryTheory.ObjectProperty.isCoseparating_iff_mono, Condensed.lanPresheafExt_inv, CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom, Types.monoOverEquivalenceSet_inverse_map, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, SSet.Truncated.StrictSegal.spineToSimplex_spine, CategoryTheory.RightExactFunctor.whiskeringLeft_map_app, CategoryTheory.Sheaf.mem_essImage_of_isConstant, CategoryTheory.MonoOver.mkArrowIso_hom_hom_left, SSet.Edge.ofTruncated_edge, CategoryTheory.ExactFunctor.forget_obj, CategoryTheory.LeftExactFunctor.forget_obj, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_hom_app, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, CategoryTheory.hasLimitsEssentiallySmallSite, CategoryTheory.Functor.mapContActionComp_inv, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, CategoryTheory.Functor.mapGrpFunctor_obj, CategoryTheory.MonoOver.map_obj_left, CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum, instFaithfulFintypeCatProfiniteToProfinite, CategoryTheory.ObjectProperty.ι_η, CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_obj, CategoryTheory.Adjunction.sheafPushforwardContinuous_unit_app_hom_app, HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompFibrantObjectιFibrantObjectWeakEquivalences, CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout, SSet.Truncated.HomotopyCategory₂.mk_surjective, CategoryTheory.RightExactFunctor.whiskeringRight_map_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality', CategoryTheory.Sheaf.instHasColimitsOfShape, CategoryTheory.Functor.sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify, CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj, CategoryTheory.PreGaloisCategory.connected_component_unique, CategoryTheory.OrthogonalReflection.isRightAdjoint_ι, CategoryTheory.Functor.mapContActionCongr_hom, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj, CategoryTheory.Functor.OneHypercoverDenseData.essSurj, CategoryTheory.essentiallySmall_monoOver, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app, lightDiagramToLightProfinite_obj, CategoryTheory.Functor.mapCommGrpFunctor_obj, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map, SSet.Truncated.Edge.CompStruct.tensor_simplex_snd, CategoryTheory.ObjectProperty.full_ι, HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, CategoryTheory.ObjectProperty.fullSubcategoryCongr_inverse, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.MonoOver.pullback_obj_arrow, CategoryTheory.AdditiveFunctor.ofLeftExact_map, CategoryTheory.RightExactFunctor.ofExact_map_hom, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, CategoryTheory.Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant, CategoryTheory.LeftExactFunctor.whiskeringRight_map_app, FGModuleCat.hom_comp, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, Profinite.Extend.functorOp_obj, CategoryTheory.Functor.IsCoverDense.sheafIso_hom_hom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv_hom, SimplexCategory.Truncated.Hom.tr_comp', CategoryTheory.ObjectProperty.ι_map, CategoryTheory.ObjectProperty.instAdditiveFullSubcategoryShiftFunctor, CategoryTheory.HasSheafify.isLeftExact, HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj, CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp_assoc, Condensed.finYoneda_map, FDRep.instFiniteDimensionalHom, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map, CategoryTheory.AdditiveFunctor.ofRightExact_map, SSet.Truncated.Edge.id_tensor_id, HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality', CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions, CategoryTheory.AdditiveFunctor.ofExact_map, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks, CategoryTheory.PreGaloisCategory.toAut_hom_app_apply, ContAction.resEquiv_inverse, FintypeCat.toProfinite_map_hom_hom_apply, CategoryTheory.ObjectProperty.fullSubcategoryCongr_unitIso, CategoryTheory.ObjectProperty.homMk_zero, CategoryTheory.Functor.IsCoverDense.faithful_sheafPushforwardContinuous, CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans, CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_X, CategoryTheory.Sheaf.toImage_ι, CategoryTheory.Limits.FintypeCat.productEquiv_apply, CategoryTheory.sheafBotEquivalence_inverse_map_hom, CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, CategoryTheory.PreGaloisCategory.obj_discreteTopology, FintypeCat.comp_apply, FGModuleCat.FGModuleCatEvaluation_apply, HomotopicalAlgebra.BifibrantObject.instCongruenceHomRel, FintypeCat.uSwitchEquiv_naturality, CategoryTheory.instFaithfulDecomposedDecomposedTo, CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app, CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction, FintypeCat.equivEquivIso_symm_apply_symm_apply, CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected, CategoryTheory.Limits.FintypeCat.hasFiniteLimits, CategoryTheory.ObjectProperty.topEquivalence_unitIso, CategoryTheory.instFullDecomposedDecomposedTo, CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow, CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, SSet.Truncated.spine_map_subinterval, CategoryTheory.RightExactFunctor.forget_map, CategoryTheory.typeEquiv_inverse_obj, CategoryTheory.Functor.EssImageSubcategory.tensor_obj, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app, CategoryTheory.Sheaf.epi_of_isLocallySurjective', CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.ObjectProperty.instFullFullSubcategoryLift, CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver, FintypeCat.incl_map, CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf, CategoryTheory.Sheaf.ΓHomEquiv_naturality_left, CategoryTheory.Sheaf.classifier_truth, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left, FintypeCat.hom_ext_iff, CategoryTheory.Functor.essImage_ι_comp, CategoryTheory.Sheaf.classifier_Ω₀, SheafOfModules.pushforwardComp_inv_app_val_app, CategoryTheory.Sheaf.instHasSubobjectClassifierTypeOfEssentiallySmall, CategoryTheory.Functor.IsCoverDense.sheafIso_inv_hom, CategoryTheory.Sheaf.isConstant_iff_forget, CategoryTheory.ObjectProperty.hasLimit_parallelPair_comp_ι, CategoryTheory.Functor.OneHypercoverDenseData.isEquivalence, CategoryTheory.instHasImagesSheafType, CategoryTheory.Sheaf.hasFilteredColimitsOfSize, CategoryTheory.plusPlusSheaf_map_hom, HomotopicalAlgebra.CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, FintypeCat.Skeleton.instIsEquivalenceIncl, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero_assoc, HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, CategoryTheory.GrothendieckTopology.instFullSheafTypeUliftYoneda, HomotopicalAlgebra.instIsMultiplicativeFullSubcategoryWeakEquivalences, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, CategoryTheory.IsFiltered.instIsFilteredOrEmptyFullSubcategoryFilteredClosure, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_map, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.transitive_of_isGalois, TannakaDuality.FiniteGroup.sumSMulInv_apply, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj, FintypeCat.id_apply, SheafOfModules.pushforwardNatTrans_id, topCatToSheafCompHausLike_map_hom_app, CategoryTheory.PreGaloisCategory.functorToContAction_map, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans, CategoryTheory.ObjectProperty.ι_ε, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_app, instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf, CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringRight, FGModuleCat.instFiniteHom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left, CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply, SSet.Truncated.liftOfStrictSegal.naturalityProperty_eq_top, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj, CategoryTheory.GrothendieckTopology.W_adj_unit_app, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom, CategoryTheory.MonoOver.image_map, CategoryTheory.Sheaf.instHasFunctorialFactorizationLocallySurjectiveLocallyInjective, CategoryTheory.decomposedEquiv_functor, CategoryTheory.isCoseparating_iff_mono, CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.Sheaf.isLocallySurjective_iff_epi', HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjι, CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_map, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, CategoryTheory.AdditiveFunctor.forget_obj_of, HomotopicalAlgebra.FibrantObject.localizerMorphism_functor, FDRep.average_char_eq_finrank_invariants, CategoryTheory.typeEquiv_unitIso_hom_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app, FGModuleCat.hom_id, CategoryTheory.AdditiveFunctor.forget_obj, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, CategoryTheory.Sheaf.classifier_Ω, SSet.Truncated.HomotopyCategory.mk_surjective, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, CategoryTheory.Sheaf.instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply, CompHausLike.LocallyConstant.counit_app_hom_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom, HomotopicalAlgebra.FibrantObject.instFullHoCatToHoCat, HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj_obj, comp_def, CategoryTheory.PreGaloisCategory.toAutHomeo_apply, SSet.Truncated.StrictSegal.spine_δ_arrow_lt, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_obj, CategoryTheory.Equivalence.mapContAction_functor, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompιWeakEquivalences, CategoryTheory.Subobject.inf_eq_map_pullback', CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, CategoryTheory.SheafOfTypes.finitary_extensive, CategoryTheory.Sheaf.instIsGrothendieckAbelian, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_symm_apply, HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app, CategoryTheory.Sheaf.natTransΓRes_app, CochainComplex.Plus.instHasFiniteLimits, CategoryTheory.PreGaloisCategory.exists_lift_of_continuous, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality', CategoryTheory.equivYoneda'_hom_hom, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CochainComplex.Plus.instHasTwoOutOfThreePropertyQuasiIso, CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal_hom, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois, SheafOfModules.Presentation.quasicoherentData_presentation, CategoryTheory.Functor.toEssImage_map_hom, CategoryTheory.Functor.partialRightAdjoint_obj, SSet.Truncated.id_app, CategoryTheory.PreGaloisCategory.instIsPretransitiveObjFiniteObjFintypeCatOfIsConnected, CategoryTheory.Functor.mapContAction_map, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left, CategoryTheory.typeEquiv_counitIso_hom_app_hom_app, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply, CategoryTheory.monoOver_terminal_to_subterminals_comp, FDRep.hom_hom_action_ρ, Action.FintypeCat.toEndHom_apply, CategoryTheory.instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompCofibrantObjectιCofibrantObjectWeakEquivalences, CategoryTheory.ExactFunctor.whiskeringLeft_map_app, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, FintypeCat.equivEquivIso_apply_inv, CategoryTheory.essentiallySmall_fullSubcategory_mem, CategoryTheory.PreGaloisCategory.toAut_isHomeomorph, CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, CategoryTheory.GrothendieckTopology.overMapPullback_assoc_assoc, CategoryTheory.Sheaf.isSheaf_of_isLimit, ContAction.resCongr_hom, CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_hom_app, CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom, CategoryTheory.MonoOver.image_obj, SSet.Truncated.spine_map_vertex, CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_hom_app, CategoryTheory.Sheaf.instHasFiniteColimits, CategoryTheory.sheafToPresheaf_δ, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono, CategoryTheory.ObjectProperty.ι_obj, CategoryTheory.IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι, CategoryTheory.ObjectProperty.SerreClassLocalization.instFaithfulExactFunctorWhiskeringLeft, CategoryTheory.typeEquiv_unitIso_inv_app, CategoryTheory.MonoOver.lift_obj_arrow, CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, Condensed.isColimitLocallyConstantPresheaf_desc_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map, FGModuleCat.FGModuleCatCoevaluation_apply_one, CategoryTheory.isRegularEpiCategory_sheaf, CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected, HomotopicalAlgebra.CofibrantObject.instFullHoCatToHoCat, CategoryTheory.LeftExactFunctor.ofExact_map_hom, CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft_obj_obj, CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_obj, CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat, CategoryTheory.equivEssImageOfReflective_functor, CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp, PresheafOfModules.sheafification_map, CategoryTheory.PreGaloisCategory.evaluation_aut_bijective_of_isGalois, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app, HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective, SSet.Truncated.Edge.map_associator_hom, CategoryTheory.PreGaloisCategory.nonempty_fiber_pi_of_nonempty_of_finite, LightProfinite.Extend.functor_map, CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app, CompHausLike.LocallyConstant.functor_map_hom, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf, SheafOfModules.pullback_comp_id, CategoryTheory.Functor.mapGrpFunctor_map_app, HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', CategoryTheory.sheafBotEquivalence_unitIso, CategoryTheory.PreGaloisCategory.instIsFundamentalGroupAutFunctorFintypeCat, SSet.Truncated.Edge.src_eq, SSet.Truncated.rightExtensionInclusion_right_as, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, CategoryTheory.Limits.hasLimit_of_closedUnderLimits, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesTerminalObjects, FintypeCat.isSkeleton, CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj_obj, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right, CategoryTheory.MonoOver.map_obj_arrow, HomotopicalAlgebra.FibrantObject.toHoCat_map_eq, CategoryTheory.ObjectProperty.instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, SimplexCategory.Truncated.morphismProperty_eq_top, CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory, LightCondensed.isoLocallyConstantOfIsColimit_inv, CategoryTheory.ExactFunctor.whiskeringLeft_obj_map, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zero_apply, ContAction.res_obj_obj, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_add_apply, FintypeCat.toLightProfinite_map_hom_hom_apply, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, CategoryTheory.SimplicialObject.Truncated.sk.full, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, HomotopicalAlgebra.instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, CategoryTheory.Equivalence.congrFullSubcategory_unitIso, TannakaDuality.FiniteGroup.equivApp_inv, CategoryTheory.decomposedTo_map, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_map_hom, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, CategoryTheory.ObjectProperty.tensorObj_obj, SSet.Truncated.StrictSegal.spine_δ_arrow_gt, CategoryTheory.isSheaf_pointwiseColimit, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map, TannakaDuality.FiniteGroup.forget_map, CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive, HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, topCatToSheafCompHausLike_obj, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CategoryTheory.Subobject.lower_comm, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app, CategoryTheory.Sheaf.adjunction_counit_app_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, CategoryTheory.SheafOfTypes.adhesive, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_obj, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_obj, SSet.Truncated.StrictSegal.spineInjective, LightCondensed.forget_map_hom_app, CategoryTheory.IsCofiltered.instIsCofilteredOrEmptyFullSubcategoryCofilteredClosure, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite, CategoryTheory.Sheaf.isSeparating, CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map, CategoryTheory.MonoOver.hasFiniteLimits, CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_inverse, FGModuleCat.ihom_obj, CategoryTheory.Sheaf.ΓObjEquivSections_naturality_symm, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, Condensed.isoLocallyConstantOfIsColimit_inv, CategoryTheory.Sheaf.mono_of_isLocallyInjective, CategoryTheory.regularTopology.parallelPair_pullback_initial, TannakaDuality.FiniteGroup.equivApp_hom, FDRep.char_linHom, CategoryTheory.ObjectProperty.ι_δ, CategoryTheory.PreGaloisCategory.FibreFunctor.end_isIso, CategoryTheory.Sheaf.classifier_χ₀, HomotopicalAlgebra.CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_obj, CategoryTheory.SimplicialObject.isCoskeletal_iff, CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_obj, CategoryTheory.Sheaf.ΓRes_map_assoc, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.ObjectProperty.isSeparating_iff_epi, CategoryTheory.PreGaloisCategory.continuousSMul_aut_fiber, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, Condensed.lanPresheafNatIso_hom_app, CategoryTheory.isEventuallyConstant_of_isArtinianObject, CategoryTheory.Sheaf.ab5ofSize, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, CategoryTheory.Sheaf.ΓObjEquivHom_naturality_symm, fintypeToFinBoolAlgOp_map, HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj_hom_ext, SheafOfModules.toSheaf_obj_obj, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π_assoc, ContAction.resComp_hom, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf, CategoryTheory.Abelian.Preradical.isRadical_iff_isIso, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app, HomotopicalAlgebra.FibrantObject.instIsFibrantObjι, CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f, SSet.Truncated.Edge.map_whiskerLeft, Profinite.Extend.functor_obj, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, CategoryTheory.Sheaf.hasSeparator, CategoryTheory.instFaithfulSheafSheafCompose, CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso, SheafOfModules.conjugateEquiv_pullbackComp_inv, SimplexCategory.Truncated.Hom.tr_id, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_hom_app, CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono, CategoryTheory.Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf, SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, CategoryTheory.ObjectProperty.ihom_obj, SSet.Truncated.Edge.map_snd, CategoryTheory.SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, FintypeCat.equivEquivIso_symm_apply_apply, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, CategoryTheory.plusPlusSheaf_obj_obj, CategoryTheory.PreGaloisCategory.FiberFunctor.instFaithfulFintypeCat, FGModuleRepr.instIsEquivalenceFGModuleCatEmbed, CategoryTheory.instEssSurjDecomposedDecomposedTo, FGModuleCat.instHasFiniteColimits, CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits, CategoryTheory.ObjectProperty.fullSubcategoryCongr_counitIso, CategoryTheory.Presheaf.isSheaf_iff_isLimit, CategoryTheory.sheafComposeNatTrans_app_uniq, HomotopicalAlgebra.instWeakEquivalenceMapFullSubcategoryι, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_hom, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse, CategoryTheory.Sheaf.instHasFiniteLimits, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, SSet.Truncated.Edge.exists_of_simplex, SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply, SSet.Truncated.Edge.map_id, Action.FintypeCat.quotientToEndHom_mk, CategoryTheory.MonoOver.forget_obj_left, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_map, CategoryTheory.instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify, CompHausLike.LocallyConstant.adjunction_left_triangle, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply, HomotopicalAlgebra.FibrantObject.instIsStableUnderPrecompHomRel, CategoryTheory.Subobject.instIsEquivalenceMonoOverRepresentative, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj_hom_ext, CategoryTheory.SimplicialObject.Truncated.trunc_obj_map, CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit, CategoryTheory.PreGaloisCategory.aut_discreteTopology, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', CategoryTheory.Sheaf.isLocallyInjective_forget, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, SheafOfModules.pullback_id_comp, CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers, SSet.Truncated.hoFunctor₂_naturality, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply, CategoryTheory.instReflectsIsomorphismsSheafSheafCompose, CategoryTheory.sheafificationNatIso_inv_app_hom, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected, CategoryTheory.ObjectProperty.IsStrongGenerator.extremalEpi_coproductFrom, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as, CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryι, CategoryTheory.ObjectProperty.instHasCokernelsFullSubcategoryOfIsClosedUnderCokernels, CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, CategoryTheory.Sheaf.coneΓ_pt, CategoryTheory.ObjectProperty.IsCoseparating.mono_productTo, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, CategoryTheory.ExactFunctor.whiskeringRight_obj_obj_obj, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_nsmul_apply, SSet.Truncated.liftOfStrictSegal.hσ'₀, CategoryTheory.ObjectProperty.hasColimit_parallelPair_comp_ι, CategoryTheory.IsGrothendieckAbelian.mono_of_isColimit_monoOver, CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_functor, SSet.Truncated.StrictSegal.spineToSimplex_vertex, CategoryTheory.Functor.partialRightAdjoint_map, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_map_down, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app', CategoryTheory.SheafOfTypes.balanced, Types.monoOverEquivalenceSet_functor_map, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, SimplexCategory.Truncated.initial_inclusion, HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompιWeakEquivalences, CategoryTheory.preservesFiniteLimits_presheafToSheaf, CategoryTheory.typeEquiv_counitIso_inv_app_hom_app, HomotopicalAlgebra.BifibrantObject.instIsStableUnderPostcompHomRel, SSet.Truncated.StrictSegal.spine_δ_vertex_ge, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_neg_apply, CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1, CategoryTheory.typeEquiv_inverse_map, CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteLimits, HomotopicalAlgebra.FibrantObject.weakEquivalence_homMk_iff, CategoryTheory.AdditiveFunctor.forget_map, SheafOfModules.pushforward_map_val, FintypeCat.instIsEquivalenceUSwitch, SSet.Truncated.StrictSegal.spineToSimplex_edge, ContAction.resEquiv_functor, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, CategoryTheory.GrothendieckTopology.Point.instIsLeftAdjointSheafSheafFiber, FDRep.instHasKernels, CategoryTheory.ObjectProperty.initial_ι, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_eq_eqToIso, SSet.Truncated.spine_arrow, CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj, SheafOfModules.pushforwardComp_hom_app_val_app, SSet.Truncated.liftOfStrictSegal.hδ'₁, FintypeCat.Skeleton.instEssSurjIncl, FintypeCat.homMk_eq_id_iff, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero, FGModuleCat.Iso.conj_eq_conj, id_def, CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_hom_app, CategoryTheory.Sheaf.adjunction_unit_app_val, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, CategoryTheory.ObjectProperty.ihom_map, CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map, SSet.Truncated.Edge.mk'_edge, CategoryTheory.ObjectProperty.preservesMonomorphisms_ι_of_isNormalEpiCategory, LightProfinite.Extend.functorOp_map, CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj, CategoryTheory.RightExactFunctor.ofExact_map, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_obj, CategoryTheory.LeftExactFunctor.ofExact_obj, CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι, Alexandrov.lowerCone_π_app, CategoryTheory.ObjectProperty.isoHom_inv_id_hom_assoc, instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf, instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app, Types.monoOverEquivalenceSet_functor_obj, CategoryTheory.MonoOver.hasLimitsOfShape, HomotopicalAlgebra.FibrantObject.homRel_equivalence_of_isCofibrant_src, SSet.Truncated.comp_app_assoc, SSet.Truncated.Edge.map_tensorHom, CategoryTheory.instIsEquivalenceDecomposedDecomposedTo, CategoryTheory.PreGaloisCategory.functorToAction_map, SSet.Truncated.StrictSegal.spineToSimplex_arrow, CategoryTheory.MonoOver.congr_functor, SSet.Truncated.rightExtensionInclusion_left, FGModuleCat.hom_hom_comp, CategoryTheory.sheafificationIso_inv_hom, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc, AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux, CategoryTheory.Equivalence.sheafCongr_counitIso, CategoryTheory.MonoOver.isIso_iff_isIso_hom_left, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app, FDRep.instInjectiveOfNeZeroCastCard, CategoryTheory.ObjectProperty.preservesCokernels_ι, AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf, CategoryTheory.MonoOver.congr_inverse, CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_map, CategoryTheory.ObjectProperty.whiskerLeft_def, FDRep.char_one, SSet.Truncated.spine_vertex, CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, CategoryTheory.GrothendieckTopology.preservesLimitsOfSize_yoneda, CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.ObjectProperty.tStructure_isLE_iff, CategoryTheory.PreGaloisCategory.fiber_in_connected_component, CategoryTheory.MonoOver.isoMk_hom, CategoryTheory.SimplicialObject.Truncated.trunc_map_app, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, CategoryTheory.Sheaf.ΓObjEquivHom_naturality, CategoryTheory.IsFiltered.instEssentiallySmallFullSubcategoryFilteredClosure, CategoryTheory.Sheaf.ΓRes_map, SheafOfModules.pushforwardCongr_symm, CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app, SSet.Truncated.mapHomotopyCategory_obj, FintypeCat.instFullForgetHomObjFinite, CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomObjFinite, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv', TannakaDuality.FiniteGroup.sumSMulInv_single_id, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right, CategoryTheory.ObjectProperty.instIsEquivalenceFullSubcategoryIsoClosureιOfLE, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, SSet.Truncated.Edge.map_edge, CategoryTheory.ObjectProperty.ι_μ, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, SSet.Truncated.Edge.id_edge, SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero, HomotopicalAlgebra.FibrantObject.homMk_homMk_assoc, CondensedSet.isDiscrete_tfae, FintypeCat.instFullIncl, CategoryTheory.ObjectProperty.ι_map_top, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isModule_smul_apply, FDRep.simple_iff_end_is_rank_one, CategoryTheory.ObjectProperty.whiskerRight_def, CategoryTheory.ExactFunctor.whiskeringRight_map_app, HomotopicalAlgebra.BifibrantObject.homMk_homMk, CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_hom_app, CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber, CategoryTheory.sheafBotEquivalence_inverse_obj_obj, CategoryTheory.Subobject.lowerEquivalence_counitIso, HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι, FintypeCat.hom_apply, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj, CategoryTheory.ObjectProperty.leftUnitor_def, CategoryTheory.Sheaf.instHasLimitsOfShape, CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso, CategoryTheory.GrothendieckTopology.overMapPullback_comp_id_assoc, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, CategoryTheory.Functor.partialLeftAdjoint_obj, CategoryTheory.MonoOver.lift_obj_obj, CategoryTheory.plusPlusSheaf_preservesZeroMorphisms, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi, SSet.Truncated.Path.arrow_src, CategoryTheory.coherentTopology.epi_π_app_zero_of_epi, CategoryTheory.Sheaf.instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, CategoryTheory.Sheaf.isConstant_iff_mem_essImage, CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits, HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceCofibrantObjectWeakEquivalencesιCofibrantObjectLocalizerMorphism, CategoryTheory.sheafCompose_map_hom, CochainComplex.Plus.instHasFiniteColimits, SSet.Truncated.liftOfStrictSegal_app_0, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality, CategoryTheory.MonoOver.inf_map_app, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.continuous_smul, CategoryTheory.MonoOver.isThin, CategoryTheory.sheafificationAdjunction_unit_app, HomotopicalAlgebra.FibrantObject.instHasQuotientWeakEquivalencesHomRel, CategoryTheory.sheafificationIso_hom_hom, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, FintypeCat.Skeleton.instFullIncl, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zsmul_apply, CategoryTheory.MonoOver.mkArrowIso_inv_hom_left, FintypeCat.Skeleton.incl_mk_nat_card, CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_id, CategoryTheory.instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences, CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf, HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans_app, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom_hom, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv', CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_map, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, CategoryTheory.ObjectProperty.prop_ι_obj, SheafOfModules.pullback_assoc, SSet.horn.spineId_vertex_coe, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesFiniteCoproducts, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply, HomotopicalAlgebra.CofibrantObject.localizerMorphism_functor, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite, instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1, CategoryTheory.Functor.essImage.liftFunctorCompIso_inv_app, CategoryTheory.PreGaloisCategory.endEquivAutGalois_mul, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.presheafToSheaf_additive, HomotopicalAlgebra.CofibrantObject.instIsStableUnderPrecompHomRel, CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive, HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism_functor, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, SSet.Truncated.tensor_map_apply_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj, SSet.horn.spineId_arrow_coe, CategoryTheory.Sheaf.Hom.epi_of_presheaf_epi, CategoryTheory.ObjectProperty.instHasZeroObjectFullSubcategoryOfContainsZero, FGModuleCat.instHasLimitsOfShapeOfFinCategory, CategoryTheory.MonoOver.pullback_obj_left, CategoryTheory.Sheaf.isLocallyInjective_sheafToPresheaf_map_iff, CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension, CategoryTheory.Functor.sheafPullbackConstruction.preservesFiniteLimits, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left, FGModuleCat.instFullUlift, instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf, CategoryTheory.Subobject.lowerEquivalence_unitIso, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, Profinite.Extend.functorOp_final, CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction, SSet.Truncated.Edge.tensor_edge, CategoryTheory.Sheaf.isConstant_iff_of_equivalence, CategoryTheory.Sheaf.hasExactColimitsOfShape, instPreservesLimitsOfShapeSheafTypeUliftYoneda, CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app, CategoryTheory.Sheaf.instHasFiniteCoproducts, CategoryTheory.PreGaloisCategory.comp_autMap_apply, instFullFGAlgCatUliftFunctor, CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, SSet.Truncated.Path.map_vertex, CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty, CategoryTheory.PreGaloisCategory.has_decomp_quotients, SSet.Truncated.cosk.faithful, CategoryTheory.MonoOver.lift_map_hom, HomotopicalAlgebra.FibrantObject.toHoCat_obj_surjective, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightCondensed.lanPresheafNatIso_hom_app, CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda, CategoryTheory.Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget, SSet.Truncated.StrictSegal.spine_δ_arrow_eq, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right_assoc, SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero_assoc, SSet.Truncated.spine_surjective, LinearEquiv.toFGModuleCatIso_hom, CategoryTheory.PreGaloisCategory.autEmbedding_apply, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', CategoryTheory.Sheaf.cohomologyFunctor_obj, CategoryTheory.Sheaf.mono_of_injective, CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.SimplicialObject.Truncated.cosk_reflective, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, SSet.Subcomplex.liftPath_arrow_coe, CategoryTheory.ObjectProperty.homMk_surjective, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_map, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_obj, SSet.Truncated.HomotopyCategory.BinaryProduct.square, CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory, Action.FintypeCat.quotientToQuotientOfLE_hom_mk, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, LightProfinite.Extend.cocone_pt, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_map, CategoryTheory.Sheaf.epi_of_isLocallySurjective, HomotopicalAlgebra.BifibrantObject.instIsStableUnderPrecompHomRel, CategoryTheory.sheafToPresheaf_η, FGModuleCat.tensorObj_obj, FGModuleCat.tensorUnit_obj, CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois, SSet.Truncated.Path₁.arrow_tgt, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_hom_app, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, ContAction.resCongr_inv, HomotopicalAlgebra.CofibrantObject.factorsThroughLocalization, FintypeCat.inv_hom_id_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, CategoryTheory.ObjectProperty.associator_def, SheafOfModules.toSheaf_map_hom, CategoryTheory.ObjectProperty.instMonoidalPreadditiveFullSubcategory, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, CategoryTheory.ObjectProperty.ιOfLE_map, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom_hom, FGModuleCat.instHasFiniteLimits, CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, CategoryTheory.Sheaf.instHasColimitsOfSize, SSet.Truncated.StrictSegal.spineToSimplex_interval, SSet.Truncated.hom_ext_iff, CategoryTheory.Functor.mapCommGrpFunctor_map, SimplexCategory.Truncated.δ₂_one_comp_σ₂_one_assoc, SheafOfModules.pushforwardNatTrans_app_val_app, Profinite.Extend.cocone_ι_app, CategoryTheory.GrothendieckTopology.W_iff, CategoryTheory.equivEssImageOfReflective_inverse, CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction, instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite, HomotopicalAlgebra.CofibrantObject.homMk_homMk_assoc, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app, SimplexCategory.Truncated.Hom.tr_comp_assoc, CategoryTheory.Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical, CategoryTheory.MonoOver.forget_obj_hom, CategoryTheory.Functor.sheafPushforwardContinuousIso_hom, HomotopicalAlgebra.BifibrantObject.homMk_homMk_assoc, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, CategoryTheory.ObjectProperty.isoMk_inv, SSet.Truncated.Path.arrow_tgt, CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_hom_app, CategoryTheory.RightExactFunctor.ofExact_obj, CategoryTheory.ObjectProperty.zero_hom, Alexandrov.lowerCone_pt, CategoryTheory.SimplicialObject.Truncated.sk_coreflective, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val, CategoryTheory.Functor.instAdditiveFullSubcategoryLift, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, SSet.Truncated.trunc_spine, CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right, CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.Equivalence.sheafCongr.functor_map_hom_app, CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp, CategoryTheory.GrothendieckTopology.Point.instIsRightAdjointSheafSkyscraperSheafFunctor, CategoryTheory.Sheaf.isSeparator, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber, Condensed.isoFinYoneda_hom_app, CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι, CategoryTheory.PreGaloisCategory.autEmbedding_range, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, CategoryTheory.ObjectProperty.isFiltered_costructuredArrow_colimitsCardinalClosure_ι, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_hom_app, Profinite.Extend.cone_pt, CategoryTheory.SimplicialObject.Truncated.sk.faithful, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_hom_app, lightDiagramToLightProfinite_map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, CategoryTheory.Sheaf.isLocallyBijective_iff_isIso, Types.monoOverEquivalenceSet_inverse_obj, SSet.Truncated.liftOfStrictSegal_app_1, SSet.Truncated.liftOfStrictSegal.hδ'₀, CategoryTheory.instIsConstantObjSheafSheafCompose, CategoryTheory.ObjectProperty.preservesKernels_ι, CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify, SSet.Truncated.cosk.full, FDRep.forget₂_ρ, CategoryTheory.MonoOver.hasLimit, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity, CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected, CategoryTheory.sheafToPresheaf_ε, comp_hom, CategoryTheory.ExactFunctor.forget_obj_of, SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, CategoryTheory.PreGaloisCategory.mulAction_naturality, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, CategoryTheory.sheafificationAdjunction_counit_app_val, FDRep.char_orthonormal, CategoryTheory.preservesLimitsOfShape_presheafToSheaf, LightCondensed.lanPresheafExt_inv, Condensed.lanPresheafExt_hom, CategoryTheory.Equivalence.mapContAction_inverse, SSet.Subcomplex.liftPath_vertex_coe, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp, CategoryTheory.MonoOver.instMonoHomDiscretePUnitObjOverForget, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp, CategoryTheory.instIsConnectedComponent, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, CategoryTheory.hasColimitsEssentiallySmallSite, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, CategoryTheory.Functor.essImage.liftFunctor_obj, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, SheafOfModules.pushforward_comp_id, CategoryTheory.Functor.mapContActionComp_hom, CategoryTheory.Equivalence.sheafCongr_inverse, SSet.Truncated.cosk_reflective, CategoryTheory.ObjectProperty.ιOfLE_ε, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, CategoryTheory.inclusion_comp_decomposedTo, FDRep.Iso.conj_ρ, CategoryTheory.Limits.FintypeCat.jointly_surjective, FDRep.of_ρ, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight_hom, CategoryTheory.GrothendieckTopology.overMapPullback_id_comp_assoc, SheafOfModules.forgetToSheafModuleCat_obj_obj, CategoryTheory.MonoOver.inf_obj, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CategoryTheory.constantSheafAdj_counit_w, CategoryTheory.sheafCompose_id, CategoryTheory.ObjectProperty.exists_equivalence_iff, instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf, CompHausLike.LocallyConstant.unit_app, CategoryTheory.PreGaloisCategory.exists_lift_of_mono, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, FDRep.char_dual, CategoryTheory.typeEquiv_functor_obj_obj_map, FGModuleCat.FGModuleCatEvaluation_apply', SSet.Truncated.Path.mk₂_vertex, LightProfinite.Extend.functor_initial, HomotopicalAlgebra.FibrantObject.homMk_id, AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty, CategoryTheory.yoneda'_comp, Types.monoOverEquivalenceSet_unitIso, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_hom_app, SSet.Truncated.IsStrictSegal.spine_bijective, CategoryTheory.Equivalence.fullyFaithfulToEssImage, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map, CategoryTheory.Equivalence.congrFullSubcategory_functor, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, CategoryTheory.ObjectProperty.instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj, CategoryTheory.typeEquiv_functor_obj_obj_obj, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, SSet.OneTruncation₂.nerveHomEquiv_apply, FintypeCat.uSwitchEquiv_symm_naturality, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois, FintypeCat.homMk_eq_comp_iff, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val_assoc, HomotopicalAlgebra.CofibrantObject.instHasQuotientWeakEquivalencesHomRel, SheafOfModules.conjugateEquiv_pullbackId_hom, CategoryTheory.Sheaf.Hom.add_app, CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategory, CategoryTheory.PreGaloisCategory.endEquivAutGalois_π, HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans_app, CategoryTheory.Sheaf.hasLimitsOfSize, CategoryTheory.PreGaloisCategory.instIsTopologicalGroupAutFunctorFintypeCat, CategoryTheory.constantCommuteCompose_hom_app_hom, SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, CategoryTheory.ObjectProperty.ιOfLE_obj_obj, CategoryTheory.Functor.toEssImageCompι_inv_app, SSet.Truncated.Edge.CompStruct.exists_of_simplex, CategoryTheory.Functor.EssSurj.toEssImage, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_map, CategoryTheory.Sheaf.adjunction_counit_app_hom, CategoryTheory.ObjectProperty.ι_obj_lift_map, CategoryTheory.sheafToPresheaf_isRightAdjoint, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj_obj, CategoryTheory.Subobject.representative_coe, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, CategoryTheory.MonoOver.full_map, CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, SSet.Truncated.liftOfStrictSegal.hσ'₁, SSet.Truncated.Edge.CompStruct.d₀, FintypeCat.hom_inv_id_apply, CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_inv_app, SSet.Truncated.Edge.map_whiskerRight, SSet.Truncated.comp_app, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, HomotopicalAlgebra.FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_hom_app, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, CategoryTheory.Functor.toEssImageCompι_hom_app, SSet.Truncated.Edge.CompStruct.map_simplex, CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj, CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, CategoryTheory.ObjectProperty.instHasFiniteProductsFullSubcategoryOfIsClosedUnderFiniteProducts, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, SSet.truncation_spine, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompιWeakEquivalences, CategoryTheory.decomposedTo_obj, CategoryTheory.MonoOver.mapIso_inverse, CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift, HomotopicalAlgebra.CofibrantObject.exists_bifibrant, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left_assoc, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map, CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_hom_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId, CategoryTheory.instAdditiveAdditiveFunctorFunctorForget, CategoryTheory.GrothendieckTopology.yoneda_map_hom, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, SSet.OneTruncation₂.map_obj, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp, CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup, CategoryTheory.RightExactFunctor.forget_obj_of, HomotopicalAlgebra.FibrantObject.factorsThroughLocalization, CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify, SheafOfModules.pushforwardNatTrans_app_val_app_apply, SSet.Truncated.HomotopyCategory.homToNerveMk_comp, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CategoryTheory.MonoOver.congr_counitIso, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_obj_map, CategoryTheory.ObjectProperty.SerreClassLocalization.instFullExactFunctorWhiskeringLeft, CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso, CategoryTheory.instIsRegularEpiCategorySheafTypeOfHasSheafify, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, FDRep.instProjectiveOfNeZeroCastCard, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, CategoryTheory.sheafCompose_obj_obj, SheafOfModules.pushforward_id_comp, CategoryTheory.Subobject.lowerEquivalence_inverse, CategoryTheory.Subobject.lowerEquivalence_functor, CategoryTheory.ObjectProperty.ι_obj_lift_obj, CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_obj, SSet.Truncated.rightExtensionInclusion_hom_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, CategoryTheory.Abelian.Radical.isZero, CategoryTheory.sheafBotEquivalence_counitIso, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_d, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb, CategoryTheory.AdditiveFunctor.ofExact_map_hom, CategoryTheory.nerve.functorOfNerveMap_obj, HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjι, CategoryTheory.GrothendieckTopology.W_eq_W_range_sheafToPresheaf_obj, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, CategoryTheory.PreGaloisCategory.toAut_bijective, SSet.Truncated.Path₁.arrow_src, CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomObjFinite, CategoryTheory.sheafification_reflective, CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply, CategoryTheory.Subobject.thinSkeleton_mk_representative_eq_self, CategoryTheory.Functor.isEquivalence_of_isOneHypercoverDense, CategoryTheory.equivEssImageOfReflective_counitIso, SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero_assoc, HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceFibrantObjectWeakEquivalencesιFibrantObjectLocalizerMorphism, CategoryTheory.Limits.FintypeCat.instFiniteObjCompFintypeCatIncl, SSet.Truncated.Edge.CompStruct.d₁, CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois, CategoryTheory.ObjectProperty.faithful_ιOfLE, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_map, CategoryTheory.Adjunction.sheafPushforwardContinuous_counit_app_hom_app, SimplexCategory.Truncated.δ₂_two_comp_σ₂_one, SSet.OneTruncation₂.id_edge, FintypeCat.incl_obj, CategoryTheory.GrothendieckTopology.yoneda_obj_obj, SSet.Edge.toTruncated_id, CategoryTheory.MorphismProperty.isCardinalAccessible_ι_isLocal, HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution_functor, CategoryTheory.ObjectProperty.topEquivalence_inverse, CategoryTheory.GrothendieckTopology.map_yonedaEquiv, CategoryTheory.Sheaf.isLocallySurjective_iff_isIso, CategoryTheory.GrothendieckTopology.overMapPullback_assoc, CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft_hom, CategoryTheory.Abelian.Preradical.isIso_toColon_iff, SSet.Truncated.sk.faithful, CategoryTheory.Sheaf.ΓObjEquivSections_naturality, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, CategoryTheory.ObjectProperty.topEquivalence_functor, CategoryTheory.PreGaloisCategory.exists_galois_representative, FDRep.scalar_product_char_eq_finrank_equivariant, CategoryTheory.Functor.toEssImage_obj_obj, CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_hom_app, LightCondensed.lanPresheafExt_hom, CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app, CategoryTheory.constantSheafAdj_counit_app, CategoryTheory.IsCofiltered.instEssentiallySmallFullSubcategoryCofilteredClosure, FGModuleCat.instFaithfulUlift, CategoryTheory.GrothendieckTopology.uliftYoneda_map_hom_app_down, HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution_functor, CategoryTheory.sheafSectionsNatIsoEvaluation_hom_app, SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat, CategoryTheory.isEventuallyConstant_of_isNoetherianObject, CategoryTheory.GrothendieckTopology.overMapPullback_id_comp, CategoryTheory.ExactFunctor.whiskeringRight_obj_map, CategoryTheory.Functor.essImage.liftFunctor_map, SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, CategoryTheory.MonoOver.faithful_exists, TannakaDuality.FiniteGroup.ofRightFDRep_hom, CategoryTheory.isNoetherianObject_iff_isEventuallyConstant, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, Types.monoOverEquivalenceSet_counitIso, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map, CategoryTheory.ObjectProperty.isoInv_hom_id_hom_assoc, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map, Condensed.isoFinYoneda_inv_app, SSet.Truncated.StrictSegal.spine_δ_vertex_lt, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj, SimplexCategory.Truncated.Hom.tr_comp'_assoc, CategoryTheory.ObjectProperty.IsSeparating.epi_coproductFrom, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, CategoryTheory.instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify, fintypeToFinBoolAlgOp_obj, CategoryTheory.Functor.EssImageSubcategory.lift_def, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, CategoryTheory.ObjectProperty.ιOfLE_η, FGModuleCat.Iso.conj_hom_eq_conj, CategoryTheory.PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat, CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.isArtinianObject_iff_isEventuallyConstant, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map, CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf, CategoryTheory.ObjectProperty.isEquivalence_ιOfLE_iff, CategoryTheory.MonoOver.faithful_map, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, CategoryTheory.Sheaf.ΓRes_naturality, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app, CategoryTheory.MonoOver.lift_comm, Profinite.Extend.functor_initial, CategoryTheory.Limits.hasColimit_of_closedUnderColimits, CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom, SheafOfModules.pushforwardNatIso_hom, CategoryTheory.ObjectProperty.ιOfLE_μ, CategoryTheory.Functor.mapContAction_obj_obj, CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_hom_app, CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, CategoryTheory.Equivalence.sheafCongr_unitIso, CategoryTheory.MonoOver.hasLimitsOfSize, HomotopicalAlgebra.FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, CategoryTheory.subterminals_to_monoOver_terminal_comp_forget, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteColimitsSheafSheafFiber, LinearEquiv.toFGModuleCatIso_inv, HomotopicalAlgebra.CofibrantObject.homMk_id, CategoryTheory.ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι, ContAction.resComp_inv, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val, TannakaDuality.FiniteGroup.equivHom_surjective, CategoryTheory.PreGaloisCategory.toAut_injective_of_non_trivial, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, CategoryTheory.equivYoneda'_inv_hom, Profinite.Extend.functor_map, TannakaDuality.FiniteGroup.equivHom_injective, ContAction.res_map, CategoryTheory.Functor.IsDenseSubsite.full_sheafPushforwardContinuous, CategoryTheory.Subobject.representative_arrow, FDRep.hom_action_ρ, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, SimplexCategory.Truncated.initial_incl, Condensed.locallyConstantIsoFinYoneda_hom_app, CategoryTheory.Functor.Full.toEssImage, FDRep.dualTensorIsoLinHom_hom_hom, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π, CategoryTheory.RightExactFunctor.forget_obj, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv, SSet.StrictSegal.isRightKanExtension, FintypeCat.instFiniteAut, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_app, SSet.Truncated.IsStrictSegal.segal, HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat, CategoryTheory.sheafSectionsNatIsoEvaluation_inv_app, CategoryTheory.Sheaf.IsConstant.mem_essImage, CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_hom_app, instFullFintypeCatLightProfiniteToLightProfinite, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val, CategoryTheory.yoneda'_obj_obj, CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply, SheafOfModules.pushforward_obj_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, FintypeCat.homMk_apply, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app, HomotopicalAlgebra.CofibrantObject.instIsStableUnderPostcompHomRel, SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc, CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatOfFinCategory, instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf, FintypeCat.Skeleton.instFaithfulIncl, CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected, instPreservesLimitsOfShapeSheafTypeYoneda, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom_hom, CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂, CategoryTheory.Sheaf.instHasFiniteProducts, CategoryTheory.ObjectProperty.ιOfLE_δ, HomotopicalAlgebra.CofibrantObject.weakEquivalence_homMk_iff, CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CategoryTheory.Functor.essImage_ext_iff, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis, CategoryTheory.ObjectProperty.instHasKernelsFullSubcategoryOfIsClosedUnderKernels, Alexandrov.projSup_map, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso, CategoryTheory.ObjectProperty.ihom_map_hom, LightProfinite.Extend.functorOp_final, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, Condensed.lanPresheafIso_hom, Condensed.discrete_obj, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.ObjectProperty.isoInv_hom_id_hom, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one, SSet.Truncated.spine_injective, FDRep.endRingEquiv_comp_ρ, id_hom, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom, CategoryTheory.FintypeCat.Action.isConnected_of_transitive, CategoryTheory.sheafComposeNatTrans_fac, CategoryTheory.GaloisCategory.hasFiberFunctor, CategoryTheory.PreGaloisCategory.functorToAction_full, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms, CategoryTheory.GrothendieckTopology.yonedaEquiv_apply, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app, HomotopicalAlgebra.FibrantObject.instIsStableUnderPostcompHomRel, HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, CategoryTheory.Limits.FintypeCat.nonempty_pi_of_nonempty, TannakaDuality.FiniteGroup.equivHom_apply, CategoryTheory.ObjectProperty.instHasFiniteCoproductsFullSubcategoryOfIsClosedUnderFiniteCoproducts, SSet.Edge.toTruncated_edge, SSet.Truncated.Edge.CompStruct.idCompId_simplex, CochainComplex.Plus.instIsStableUnderRetractsQuasiIso, CategoryTheory.MorphismProperty.isLocallyPresentable_isLocal, FDRep.simple_iff_char_is_norm_one, CategoryTheory.AdditiveFunctor.ofRightExact_map_hom, CategoryTheory.yoneda'_map_hom, CategoryTheory.Equivalence.sheafCongr.inverse_map_hom_app, CategoryTheory.PreGaloisCategory.toAut_continuous, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right, CompHausLike.LocallyConstant.adjunction_unit, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding, Profinite.exists_hom, Action.FintypeCat.toEndHom_trivial_of_mem, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_inverse, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, CategoryTheory.PreGaloisCategory.instContinuousInvAutFunctorFintypeCat, CategoryTheory.Functor.IsDenseSubsite.faithful_sheafPushforwardContinuous, CategoryTheory.ObjectProperty.essSurj_ιOfLE_iff, CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff, CategoryTheory.ObjectProperty.isTriangulated_lift, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj_obj, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, SheafOfModules.pushforwardNatTrans_comp, CategoryTheory.RightExactFunctor.whiskeringRight_obj_map, HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq, CategoryTheory.Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app, SSet.Truncated.Edge.tgt_eq, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom, CategoryTheory.MonoOver.isIso_iff_isIso_left, CategoryTheory.LeftExactFunctor.forget_obj_of, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, CategoryTheory.instMonoSheafTypeImageι, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map, CategoryTheory.Sheaf.isTerminalTerminal_from_hom, CategoryTheory.Functor.IsCoverDense.full_sheafPushforwardContinuous, Action.FintypeCat.ofMulAction_apply, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv_hom, CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, SSet.Truncated.StrictSegal.spineToSimplex_map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact, FDRep.finrank_hom_simple_simple, CategoryTheory.ObjectProperty.SerreClassLocalization.essImage_whiskeringLeft, FGModuleCat.instIsIsoCoimageImageComparison, CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_hom_app, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology, CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed, CategoryTheory.essentiallySmall_monoOver_iff_small_subobject, CategoryTheory.sheafCompose_comp, HomotopicalAlgebra.BifibrantObject.instIsFibrantObjι, CategoryTheory.Functor.partialLeftAdjoint_map, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
obj 📖	CompOp	1065 math math: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val, CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, CategoryTheory.ObjectProperty.isoMk_hom, CategoryTheory.LeftExactFunctor.ofExact_map, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, SheafOfModules.instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, CategoryTheory.PreGaloisCategory.mulAction_def, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm, CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm, CategoryTheory.instIsCardinalPresentableObjIsCardinalPresentable, CategoryTheory.PreGaloisCategory.action_ext_of_isGalois, TopCat.Sheaf.interUnionPullbackCone_snd, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_obj_obj, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, CategoryTheory.MonoOver.mk_coe, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_id, LightCondensed.ihomPoints_apply, Condensed.instPreservesFiniteProductsOppositeStoneanObjFunctorIsSheafCoherentTopology, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom, LinearMap.id_fgModuleCat_comp, CategoryTheory.eval_app, CategoryTheory.ExactFunctor.forget_map, CategoryTheory.PreGaloisCategory.instContinuousSMulAutFintypeCatObjObjFinite, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_down, CategoryTheory.MonoOver.congr_unitIso, CompHausLike.LocallyConstant.functor_obj_obj, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom, CategoryTheory.LeftExactFunctor.forget_map, AlgebraicGeometry.StructureSheaf.comap_id, PresheafOfModules.instIsLocallySurjectiveToSheafify, FGModuleCat.hom_hom_id, CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_map, condensedSetToTopCat_obj_carrier, CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso, AlgebraicGeometry.StructureSheaf.const_mul_rev, CategoryTheory.ObjectProperty.rightUnitor_def, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteObjFunctorIsSheafCoherentTopology, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app, HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty, CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_hom_app, Condensed.hom_ext_iff, CategoryTheory.ran_isSheaf_of_isCocontinuous, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply, AlgebraicGeometry.StructureSheaf.comap_comp, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply, HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects, PresheafOfModules.Sheafify.add_smul, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_hom, CategoryTheory.instAdditiveObjFunctorAdditiveFunctor, comp_hom_assoc, CategoryTheory.MonoOver.mk_obj, FDRep.endRingEquiv_symm_comp_ρ, CategoryTheory.MonoOver.isIso_left_iff_subobjectMk_eq, CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected, CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj_obj, FintypeCat.uSwitch_map_uSwitch_map, AlgebraicGeometry.StructureSheaf.const_self, LightCondensed.ihomPoints_symm_comp, CondensedSet.topCatAdjunctionUnit_hom_app_apply, AlgebraicGeometry.Proj.pow_apply, CategoryTheory.Sieve.ofArrows_category', AlgebraicGeometry.Spec_presheaf, CategoryTheory.Functor.EssImageSubcategory.associator_inv_def, CategoryTheory.Functor.sheafPushforwardContinuous_map_hom_app, LightCondSet.continuous_coinducingCoprod, CategoryTheory.ObjectProperty.lift_obj_obj, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom_hom, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_map, CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq, SheafOfModules.evaluationPreservesLimit, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv_hom, CategoryTheory.ObjectProperty.tStructure_isGE_iff, SheafOfModules.forgetToSheafModuleCat_map_hom, AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.StructureSheaf.comap_id', CategoryTheory.ObjectProperty.tensorUnit_obj, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm_assoc, CondensedSet.hom_naturality_apply, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_obj, FunctorToFintypeCat.naturality, CategoryTheory.Functor.EssImageSubcategory.associator_hom_def, CategoryTheory.typeEquiv_functor_map_hom_app, CategoryTheory.sheafificationNatIso_hom_app_hom, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm_assoc, CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply, SheafOfModules.inl_freeSumIso_hom, LightCondensed.finYoneda_map, CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj, FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, AlgebraicGeometry.StructureSheaf.const_add, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_sub_apply, CategoryTheory.MonoOver.isoMk_inv, PresheafOfModules.toSheafify_app_apply', CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_hom, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_hom_app, CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CategoryTheory.instAdditiveObjFunctorAdditiveFunctor_1, AlgebraicGeometry.structureSheafInType.mul_apply, LinearMap.comp_id_fgModuleCat, CategoryTheory.constantCommuteCompose_hom_app_val, AlgebraicGeometry.StructureSheaf.exists_const, CategoryTheory.ObjectProperty.eqToHom_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected, TopCat.Sheaf.pushforward_map, FintypeCat.equivEquivIso_apply_hom, CategoryTheory.Functor.IsCoverDense.isoOver_hom_app, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier, SheafOfModules.inr_freeSumIso_hom, smoothSheaf.ι_evalHom_apply, CochainComplex.Plus.mono_iff, CategoryTheory.Sheaf.adjunction_unit_app_hom, Condensed.instPreservesFiniteProductsOppositeProfiniteObjFunctorIsSheafCoherentTopology, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_obj, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_obj_obj, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom, CategoryTheory.ObjectProperty.tensorHom_def, AlgebraicGeometry.Scheme.LocalRepresentability.isRepresentable, CategoryTheory.Functor.mapContActionCongr_inv, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', CategoryTheory.AdditiveFunctor.ofExact_obj_fst, TopCat.Sheaf.interUnionPullbackCone_fst, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac', AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_hom, SheafOfModules.evaluationPreservesLimitsOfShape, CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.ObjectProperty.isoHom_inv_id_hom, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc, AlgebraicGeometry.Proj.one_apply, AlgebraicGeometry.AffineScheme.mk_obj, Condensed.epi_iff_surjective_on_stonean, CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_hom_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, FGModuleCat.instFiniteHomModuleCatObjIsFG, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val, CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_comp, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map, CategoryTheory.RightExactFunctor.whiskeringLeft_map_app, CategoryTheory.MonoOver.mkArrowIso_hom_hom_left, CategoryTheory.ExactFunctor.forget_obj, CategoryTheory.LeftExactFunctor.forget_obj, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_hom_app, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm_assoc, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_app, CategoryTheory.Functor.IsCoverDense.Types.appHom_valid_glue, PresheafOfModules.toPresheaf_map_toSheafify, CategoryTheory.Functor.mapGrpFunctor_obj, CategoryTheory.MonoOver.map_obj_left, CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum, CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_obj, CategoryTheory.Adjunction.sheafPushforwardContinuous_unit_app_hom_app, TopCat.Sheaf.id_app, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app, CategoryTheory.MonoOver.isIso_hom_left_iff_subobjectMk_eq, AlgebraicGeometry.StructureSheaf.comap_const, CategoryTheory.RightExactFunctor.whiskeringRight_map_app, Condensed.id_hom, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality', PresheafOfModules.Sheafify.map_smul_eq, CategoryTheory.Sieve.ofArrows_category, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_of_sheaf, AlgebraicGeometry.Proj.sub_apply, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_assoc, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def, CategoryTheory.PreGaloisCategory.connected_component_unique, CategoryTheory.Functor.mapContActionCongr_hom, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, Condensed.isSheafStonean, PresheafOfModules.instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app, CategoryTheory.Functor.mapCommGrpFunctor_obj, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map, smoothSheaf.ι_evalHom_assoc, HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRel, CategoryTheory.Functor.IsCoverDense.sheafHom_eq, AlgebraicGeometry.StructureSheaf.comap_apply, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.AdditiveFunctor.ofLeftExact_map, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition, CategoryTheory.RightExactFunctor.ofExact_map_hom, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map, CategoryTheory.LeftExactFunctor.whiskeringRight_map_app, FGModuleCat.hom_comp, SheafOfModules.evaluationPreservesLimitsOfSize, CategoryTheory.MorphismProperty.FunctorsInverting.id_hom, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, CategoryTheory.Functor.IsCoverDense.sheafIso_hom_hom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv_hom, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm, SimplexCategory.Truncated.Hom.tr_comp', CategoryTheory.Sheaf.terminal_obj, CategoryTheory.Sheaf.imageι_hom, CategoryTheory.ObjectProperty.ι_map, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj, LightCondensed.comp_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj, Condensed.finYoneda_map, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map, CategoryTheory.AdditiveFunctor.ofRightExact_map, instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality', AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, CategoryTheory.AdditiveFunctor.ofExact_map, CategoryTheory.PreGaloisCategory.toAut_hom_app_apply, AlgebraicGeometry.Scheme.ΓSpecIso_inv, FintypeCat.toProfinite_map_hom_hom_apply, CategoryTheory.ObjectProperty.homMk_zero, CategoryTheory.Sheaf.tensorProd_isSheaf, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction_assoc, SheafOfModules.isSheaf, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π_assoc, CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_X, CategoryTheory.Limits.FintypeCat.productEquiv_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', property, CategoryTheory.sheafBotEquivalence_inverse_map_hom, CategoryTheory.PreGaloisCategory.obj_discreteTopology, FintypeCat.comp_apply, FGModuleCat.FGModuleCatEvaluation_apply, FintypeCat.uSwitchEquiv_naturality, LightCondensed.ofSheafLightProfinite_obj, CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app, FintypeCat.comp_hom, FintypeCat.equivEquivIso_symm_apply_symm_apply, CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms, CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.RightExactFunctor.forget_map, CategoryTheory.typeEquiv_inverse_obj, CategoryTheory.Functor.EssImageSubcategory.tensor_obj, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app_assoc, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver, FintypeCat.incl_map, CategoryTheory.Sheaf.ΓHomEquiv_naturality_left, FintypeCat.hom_ext_iff, SheafOfModules.pushforwardComp_inv_app_val_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app, CategoryTheory.Functor.IsCoverDense.sheafIso_inv_hom, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_map_assoc, CategoryTheory.plusPlusSheaf_map_hom, TopCat.Sheaf.extend_hom_app, CategoryTheory.presheaf_mono_of_mono, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_map, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.transitive_of_isGalois, TannakaDuality.FiniteGroup.sumSMulInv_apply, FintypeCat.id_apply, topCatToSheafCompHausLike_map_hom_app, CategoryTheory.PreGaloisCategory.functorToContAction_map, SheafOfModules.restrictScalars_obj_val, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_app, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left, CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply, instFiniteCarrier, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso_inv_naturality, CondensedMod.epi_iff_surjective_on_stonean, FDRep.average_char_eq_finrank_invariants, CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp, FGModuleCat.hom_id, AlgebraicGeometry.Spec.map_appLE, CategoryTheory.AdditiveFunctor.forget_obj, CategoryTheory.Localization.whiskeringLeftFunctor'_eq, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val, CategoryTheory.Sheaf.χ_hom, CategoryTheory.Functor.partialRightAdjointHomEquiv_map, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply, CompHausLike.LocallyConstant.counit_app_hom_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom, CategoryTheory.instMonoFunctorOppositeHomFullSubcategoryIsSheafOfHasWeakSheafifyOfSheaf, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj_obj, comp_def, CondensedSet.epi_iff_surjective_on_stonean, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_obj, CategoryTheory.Subobject.inf_eq_map_pullback', CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_assoc, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map, CategoryTheory.Sheaf.toImage_hom, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_symm_apply, HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_mapPreimage, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality', CategoryTheory.Sheaf.image_obj, CategoryTheory.equivYoneda'_hom_hom, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois, CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward, CategoryTheory.Functor.IsCoverDense.presheafIso_hom_app, CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ_assoc, CategoryTheory.Functor.toEssImage_map_hom, TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective, CategoryTheory.PreGaloisCategory.instIsPretransitiveObjFiniteObjFintypeCatOfIsConnected, AlgebraicGeometry.StructureSheaf.const_mul_cancel, CategoryTheory.Functor.mapContAction_map, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left, CategoryTheory.typeEquiv_counitIso_hom_app_hom_app, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map, CategoryTheory.Functor.instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, FDRep.hom_hom_action_ρ, Action.FintypeCat.toEndHom_apply, FGModuleCat.FGModuleCatDual_obj, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, SheafOfModules.pushforwardCongr_hom_app_val_app, CategoryTheory.ExactFunctor.whiskeringLeft_map_app, FintypeCat.equivEquivIso_apply_inv, ContAction.resCongr_hom, CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_hom_app, CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom, SSet.Truncated.spine_map_vertex, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_hom_app, CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono, CategoryTheory.ObjectProperty.ι_obj, TopCat.Sheaf.existsUnique_gluing, FGModuleCat.obj_carrier, CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, FGModuleCat.FGModuleCatCoevaluation_apply_one, FintypeCatDiscrete.instDiscreteTopologyObjFinite, CategoryTheory.LeftExactFunctor.ofExact_map_hom, CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft_obj_obj, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_obj, CategoryTheory.PreGaloisCategory.evaluation_aut_bijective_of_isGalois, CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app, TopCat.Presheaf.stalk_mono_of_mono, CategoryTheory.PreGaloisCategory.nonempty_fiber_pi_of_nonempty_of_finite, TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective, TopCat.Sheaf.interUnionPullbackConeLift_right, CompHausLike.LocallyConstant.functor_map_hom, CategoryTheory.Functor.mapGrpFunctor_map_app, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', AlgebraicGeometry.StructureSheaf.const_one, CategoryTheory.MonoOver.bot_left, CategoryTheory.Presieve.ofArrows_category, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj_obj, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right, CategoryTheory.MonoOver.map_obj_arrow, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app, CategoryTheory.ExactFunctor.whiskeringLeft_obj_map, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zero_apply, ContAction.res_obj_obj, Condensed.comp_val, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_add_apply, CondensedMod.hom_naturality_apply, FintypeCat.toLightProfinite_map_hom_hom_apply, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, TopCat.toSheafCompHausLike_obj_obj, AlgebraicGeometry.StructureSheaf.smul_const, TannakaDuality.FiniteGroup.equivApp_inv, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_map_hom, CategoryTheory.ObjectProperty.tensorObj_obj, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom, TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective, Condensed.epi_iff_locallySurjective_on_compHaus, CategoryTheory.Functor.op_comp_isSheaf_of_types, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app, CategoryTheory.Sheaf.adjunction_counit_app_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, SheafOfModules.id_val, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction, CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_obj, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_obj, LightCondensed.forget_map_hom_app, CategoryTheory.MonoOver.w, CategoryTheory.MonoOver.bot_arrow_eq_zero, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteObjFinite, CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom_assoc, CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict, CategoryTheory.Sheaf.cond, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map, FGModuleCat.ihom_obj, TopCat.Sheaf.existsUnique_gluing', CategoryTheory.Sheaf.ΓObjEquivSections_naturality_symm, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_mapPreimage_assoc, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Sheaf.isLocallyInjective_iff_injective, TannakaDuality.FiniteGroup.equivApp_hom, FDRep.char_linHom, CategoryTheory.Pseudofunctor.isStackFor_iff, AlgebraicGeometry.StructureSheaf.const_zero, FintypeCat.discreteTopology, CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_obj, CategoryTheory.Sheaf.ΓRes_map_assoc, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.PreGaloisCategory.continuousSMul_aut_fiber, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible, TopCat.Sheaf.comp_app, CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, TopCat.Sheaf.IsFlasque.epi_of_shortExact, fintypeToFinBoolAlgOp_map, LightCondensed.forget_obj_obj_map, SheafOfModules.toSheaf_obj_obj, SheafOfModules.pushforwardCongr_inv_app_val_app, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π_assoc, CategoryTheory.Functor.IsCoverDense.Types.appIso_inv, PresheafOfModules.Sheafify.smul_add, CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom_assoc, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_hom_app, CategoryTheory.ObjectProperty.ihom_obj, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, SheafOfModules.inl_freeSumIso_hom_assoc, FintypeCat.equivEquivIso_symm_apply_apply, CategoryTheory.plusPlusSheaf_obj_obj, CategoryTheory.MonoOver.mk'_coe', CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_hom, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected, CategoryTheory.MonoOver.mono, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply, Action.FintypeCat.quotientToEndHom_mk, CategoryTheory.MonoOver.forget_obj_left, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_map, CompHausLike.LocallyConstant.adjunction_left_triangle, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, CategoryTheory.extensiveTopology.isLocallySurjective_iff, TopCat.Sheaf.pushforward_obj_val, SheafOfModules.fullyFaithfulForget_preimage_val, TopCat.Sheaf.sections_exact_of_left_exact, CategoryTheory.Sheaf.truth_hom, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_assoc, AlgebraicGeometry.AffineScheme.forgetToScheme_map, SheafOfModules.restrictScalars_map_val, CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply, CategoryTheory.sheafificationNatIso_inv_app_hom, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc, CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected, CategoryTheory.Sheaf.coneΓ_pt, CategoryTheory.ExactFunctor.whiskeringRight_obj_obj_obj, CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_nsmul_apply, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map_comp, CategoryTheory.instIsIsoAppUnitReflectorAdjunctionObjEssImage, CondensedSet.continuous_coinducingCoprod, AlgebraicGeometry.Proj.zero_apply, AlgebraicGeometry.isAffine_affineScheme, CategoryTheory.Functor.IsCoverDense.Types.presheafIso_inv_app, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_map_down, Types.monoOverEquivalenceSet_functor_map, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, AlgebraicGeometry.StructureSheaf.const_algebraMap, CategoryTheory.typeEquiv_counitIso_inv_app_hom_app, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_neg_apply, SheafOfModules.inr_freeSumIso_hom_assoc, CategoryTheory.typeEquiv_inverse_map, CategoryTheory.AdditiveFunctor.forget_map, SheafOfModules.pushforward_map_val, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom, CategoryTheory.Abelian.Preradical.isIso_toColon_hom_left_app_iff, SheafOfModules.pushforwardComp_hom_app_val_app, CategoryTheory.instPreservesFiniteLimitsObjFunctorLeftExactFunctor, FintypeCat.homMk_eq_id_iff, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_V, SheafOfModules.unit_val, LightCondSet.topCatAdjunctionUnit_hom_app_apply, SheafOfModules.Presentation.map_relations_I, FGModuleCat.Iso.conj_eq_conj, id_def, CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_hom_app, CategoryTheory.Sheaf.adjunction_unit_app_val, CategoryTheory.ObjectProperty.ihom_map, TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective, CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective, SimplexCategory.Truncated.Hom.ext_iff, TopCat.Sheaf.interUnionPullbackConeLift_left, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj, CategoryTheory.RightExactFunctor.ofExact_map, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_obj, CategoryTheory.LeftExactFunctor.ofExact_obj, CategoryTheory.ObjectProperty.isoHom_inv_id_hom_assoc, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app, Types.monoOverEquivalenceSet_functor_obj, SheafOfModules.Presentation.mapRelations_mapGenerators, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, FGModuleCat.hom_hom_comp, LightCondensed.hom_ext_iff, CategoryTheory.sheafificationIso_inv_hom, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc, AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk_val, CategoryTheory.MonoOver.isIso_iff_isIso_hom_left, PresheafOfModules.instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app, SheafOfModules.relationsOfIsCokernelFree_I, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_f, HomotopicalAlgebra.BifibrantObject.homRel_iff_leftHomotopyRel, AlgebraicGeometry.structureSheafInType.add_apply, CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_map, CategoryTheory.ObjectProperty.whiskerLeft_def, FDRep.char_one, LightCondensed.underlying_obj, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility, CategoryTheory.Sheaf.Ω_obj, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, CategoryTheory.Functor.IsCoverDense.Types.naturality_apply, FGModuleCat.hom_ext_iff, CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.ObjectProperty.tStructure_isLE_iff, CategoryTheory.PreGaloisCategory.fiber_in_connected_component, CategoryTheory.MonoOver.isoMk_hom, CategoryTheory.Sheaf.coneΓ_π_app, ext_iff, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition, TopCat.subsheafToTypes_obj, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, FintypeCat.comp_hom_assoc, CategoryTheory.Sheaf.ΓRes_map, CategoryTheory.Functor.instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined, LightCondSet.hom_naturality_apply, FintypeCat.instFullForgetHomObjFinite, CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomObjFinite, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv', TannakaDuality.FiniteGroup.sumSMulInv_single_id, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, SheafOfModules.add_val, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem_of_small, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, AlgebraicGeometry.Proj.add_apply, PresheafOfModules.sheafifyMap_val, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isModule_smul_apply, CategoryTheory.ObjectProperty.whiskerRight_def, AlgebraicGeometry.stalkMap_toStalk_apply, CategoryTheory.ExactFunctor.whiskeringRight_map_app, PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_hom_app, CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber, CategoryTheory.sheafBotEquivalence_inverse_obj_obj, HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, FintypeCat.hom_apply, CategoryTheory.ObjectProperty.leftUnitor_def, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, CategoryTheory.MonoOver.lift_obj_obj, CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi, CategoryTheory.Functor.IsCoverDense.presheafIso_inv, CategoryTheory.Mat.comp_apply, CategoryTheory.sheafCompose_map_hom, AlgebraicGeometry.StructureSheaf.comapₗ_const, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality, CategoryTheory.MonoOver.inf_map_app, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.continuous_smul, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app_assoc, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map_assoc, CategoryTheory.sheafificationIso_hom_hom, AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc, AlgebraicGeometry.StructureSheaf.res_apply, LightCondensed.equalizerCondition, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zsmul_apply, CategoryTheory.MonoOver.mkArrowIso_inv_hom_left, FintypeCat.Skeleton.incl_mk_nat_card, CategoryTheory.instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction, HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans_app, LightCondMod.hom_naturality_apply, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom_hom, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv', SheafOfModules.unitToPushforwardObjUnit_val_app_apply, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply, CategoryTheory.CompatiblePreserving.apply_map, SheafOfModules.forget_map, CategoryTheory.Functor.essImage.liftFunctorCompIso_inv_app, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, CategoryTheory.MonoOver.w_assoc, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive, LightCondensed.ihomPoints_symm_apply, CategoryTheory.LeftExactFunctor.of_fst, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, SheafOfModules.forgetPreservesLimitsOfSize, CategoryTheory.MorphismProperty.FunctorsInverting.ext_iff, CategoryTheory.MonoOver.pullback_obj_left, SheafOfModules.instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, AlgebraicGeometry.StructureSheaf.algebraMap_germ, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff, CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app, CategoryTheory.PreGaloisCategory.comp_autMap_apply, CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction, CategoryTheory.MonoOver.lift_map_hom, CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom, CategoryTheory.AdditiveFunctor.of_obj, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right_assoc, AlgebraicGeometry.StructureSheaf.const_mul_cancel', CategoryTheory.Functor.IsCoverDense.homOver_app, LinearEquiv.toFGModuleCatIso_hom, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType, lightCondSetToTopCat_obj_carrier, SheafOfModules.Finite.forgetPreservesFiniteLimits, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, SheafOfModules.forget_obj, CategoryTheory.ObjectProperty.homMk_surjective, CategoryTheory.Functor.IsCoverDense.Types.presheafIso_hom_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_map, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_obj, Action.FintypeCat.quotientToQuotientOfLE_hom_mk, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, SheafOfModules.comp_val_assoc, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_map, LightCondensed.ihom_map_val_app, FGModuleCat.tensorObj_obj, FGModuleCat.tensorUnit_obj, CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois, TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_hom_app, CategoryTheory.RightExactFunctor.of_fst, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_of_eq, AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, ContAction.resCongr_inv, FintypeCat.inv_hom_id_apply, FintypeCat.instFiniteObj, CategoryTheory.ObjectProperty.associator_def, SheafOfModules.toSheaf_map_hom, CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom, HomotopicalAlgebra.FibrantObject.instIsFibrantObjFibrantObjects, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, CategoryTheory.ObjectProperty.ιOfLE_map, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom_hom, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext_iff, CategoryTheory.Functor.mapCommGrpFunctor_map, SheafOfModules.pushforwardNatTrans_app_val_app, CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois, PresheafOfModules.Sheafify.one_smul, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, CondensedMod.epi_iff_locallySurjective_on_compHaus, CategoryTheory.instPreservesFiniteColimitsObjFunctorRightExactFunctor, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app, CategoryTheory.sheafOver_obj, CategoryTheory.Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical, AlgebraicGeometry.ΓSpec.toSpecΓ_of, CategoryTheory.Functor.IsCoverDense.Types.presheafHom_app, AlgebraicGeometry.StructureSheaf.toOpen_germ, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality, CategoryTheory.ObjectProperty.isoMk_inv, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app, CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_hom_app, CategoryTheory.RightExactFunctor.ofExact_obj, CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp_assoc, CategoryTheory.ObjectProperty.zero_hom, CategoryTheory.Mat.comp_def, TopCat.toSheafCompHausLike_obj_map, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.Equivalence.sheafCongr.functor_map_hom_app, CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber, CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_comp_assoc, TopCat.Sheaf.eq_app_of_locally_eq, CategoryTheory.PreGaloisCategory.autEmbedding_range, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_hom_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_hom_app, FGModuleCat.FGModuleCatDual_coe, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, CategoryTheory.Functor.IsCoverDense.isoOver_inv_app, SheafOfModules.instReflectsIsomorphismsPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, smoothSheaf.ι_evalHom, FDRep.forget₂_ρ, CategoryTheory.Mat.id_apply, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_restriction, CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpen, comp_hom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const, CategoryTheory.PreGaloisCategory.mulAction_naturality, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, CategoryTheory.sheafificationAdjunction_counit_app_val, AlgebraicGeometry.StructureSheaf.res_const, instFiniteTypeCarrierObjCommAlgCat, CategoryTheory.Functor.op_comp_isSheaf, FGModuleCat.instFiniteCarrier, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality, SheafOfModules.relationsOfIsCokernelFree_s, FDRep.Iso.conj_ρ, CategoryTheory.Limits.FintypeCat.jointly_surjective, CategoryTheory.Pseudofunctor.sheafHom_obj, FDRep.of_ρ, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight_hom, SheafOfModules.forgetToSheafModuleCat_obj_obj, CategoryTheory.MonoOver.inf_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app, CategoryTheory.constantSheafAdj_counit_w, CategoryTheory.MonoOver.top_left, FDRep.char_dual, CategoryTheory.typeEquiv_functor_obj_obj_map, HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects, FGModuleCat.FGModuleCatEvaluation_apply', CategoryTheory.CompatiblePreserving.compatible, Types.monoOverEquivalenceSet_unitIso, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_hom_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, LightCondSet.topCatAdjunctionUnit_hom_app, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso_inv_naturality_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj, CategoryTheory.typeEquiv_functor_obj_obj_obj, FintypeCat.uSwitchEquiv_symm_naturality, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois, FintypeCat.homMk_eq_comp_iff, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, AlgebraicGeometry.StructureSheaf.comap_basicOpen, Condensed.underlying_obj, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val_assoc, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, CategoryTheory.Sheaf.Hom.add_app, CategoryTheory.PreGaloisCategory.endEquivAutGalois_π, HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans_app, CategoryTheory.ExactFunctor.of_fst, AlgebraicGeometry.tilde.toOpen_map_app_assoc, CategoryTheory.instPreservesFiniteColimitsObjFunctorExactFunctor, CategoryTheory.constantCommuteCompose_hom_app_hom, CategoryTheory.Functor.IsDenseSubsite.map_eq_of_eq, CategoryTheory.ObjectProperty.ιOfLE_obj_obj, CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation, AlgebraicGeometry.AffineScheme.forgetToScheme_obj, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_map, CategoryTheory.Sheaf.adjunction_counit_app_hom, LightCondensed.id_val, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj_obj, CategoryTheory.Subobject.representative_coe, LightCondensed.ofSheafForgetLightProfinite_obj, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, PresheafOfModules.Sheafify.zero_smul, FintypeCat.hom_inv_id_apply, CategoryTheory.ObjectProperty.hom_ext_iff, CategoryTheory.Sheaf.hom_ext_iff, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj, CategoryTheory.instPreservesFiniteProductsOppositeObjFunctorIsSheafExtensiveTopology, CategoryTheory.AdditiveFunctor.of_fst, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, Condensed.comp_hom, CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_hom_app, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left, FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, CategoryTheory.decomposedTo_obj, CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left_assoc, CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_hom_app, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t, SheafOfModules.forgetPreservesLimitsOfShape, CategoryTheory.GrothendieckTopology.yoneda_map_hom, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, SheafOfModules.Presentation.IsFinite.finite_relations, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp, SheafOfModules.pushforwardNatTrans_app_val_app_apply, CategoryTheory.MonoOver.congr_counitIso, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, SheafOfModules.comp_val, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_obj_map, CategoryTheory.Functor.IsContinuous.op_comp_isSheaf_of_types, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, CondensedSet.toTopCatMap_hom_apply, AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, CategoryTheory.sheafCompose_obj_obj, CategoryTheory.Functor.IsCoverDense.Types.appIso_hom, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc, LightCondensed.comp_val, LightCondensed.id_hom, CategoryTheory.Abelian.Radical.isZero, CategoryTheory.sheafBotEquivalence_counitIso, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_d, CategoryTheory.AdditiveFunctor.ofExact_map_hom, PresheafOfModules.instIsLocallyInjectiveToSheafify, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, CategoryTheory.subterminalInclusion_obj, CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomObjFinite, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply, TopCat.Sheaf.eq_of_locally_eq_iff, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_map, CategoryTheory.equivEssImageOfReflective_counitIso, LightCondensed.underlying_map, CategoryTheory.subterminalInclusion_map, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app, Condensed.underlying_map, CategoryTheory.Adjunction.sheafPushforwardContinuous_counit_app_hom_app, FintypeCat.incl_obj, CategoryTheory.GrothendieckTopology.yoneda_obj_obj, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, AlgebraicGeometry.Proj.res_apply, Algebra.FiniteType.exists_fgAlgCatSkeleton, TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, SheafOfModules.pushforwardSections_coe, CategoryTheory.GrothendieckTopology.map_yonedaEquiv, PresheafOfModules.Sheafify.smul_zero, PresheafOfModules.Sheafify.map_smul, AlgebraicGeometry.StructureSheaf.toOpen_res, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft_hom, CategoryTheory.coherentTopology.isLocallySurjective_iff, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, CategoryTheory.Sheaf.ΓObjEquivSections_naturality, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, CategoryTheory.PreGaloisCategory.exists_galois_representative, LightCondSet.toTopCatMap_hom_apply, FintypeCat.id_hom, HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel, CondensedSet.epi_iff_locallySurjective_on_compHaus, CategoryTheory.Functor.toEssImage_obj_obj, AlgebraicGeometry.StructureSheaf.const_mul, CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_hom_app, CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app, CategoryTheory.constantSheafAdj_counit_app, PresheafOfModules.toSheafify_app_apply, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, TopCat.Sheaf.interUnionPullbackCone_pt, CategoryTheory.GrothendieckTopology.uliftYoneda_map_hom_app_down, CategoryTheory.sheafSectionsNatIsoEvaluation_hom_app, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm, CategoryTheory.ExactFunctor.whiskeringRight_obj_map, CategoryTheory.Functor.essImage.liftFunctor_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, TannakaDuality.FiniteGroup.ofRightFDRep_hom, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, SheafOfModules.instFullPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget, CondensedSet.topCatAdjunctionUnit_hom_app, Types.monoOverEquivalenceSet_counitIso, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map, CategoryTheory.ObjectProperty.isoInv_hom_id_hom_assoc, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, TopCat.Sheaf.isLocallySurjective_iff_epi, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, SimplexCategory.Truncated.Hom.tr_comp'_assoc, fintypeToFinBoolAlgOp_obj, CategoryTheory.Functor.EssImageSubcategory.lift_def, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FGModuleCat.Iso.conj_hom_eq_conj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, CategoryTheory.Sheaf.ΓRes_naturality, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app, CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom, CategoryTheory.ObjectProperty.homMk_hom, AlgebraicGeometry.structureSheafInType.smul_apply, CategoryTheory.Functor.mapContAction_obj_obj, CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_hom_app, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjCofibrantObjects, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, LinearEquiv.toFGModuleCatIso_inv, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, Condensed.isSheafProfinite, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, CategoryTheory.equivYoneda'_inv_hom, CategoryTheory.Sheaf.isSeparated, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, ContAction.res_map, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right, Condensed.id_val, TopCat.Presheaf.mono_iff_stalk_mono, FDRep.hom_action_ρ, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, FDRep.dualTensorIsoLinHom_hom_hom, Condensed.instPreservesFiniteProductsOppositeCompHausObjFunctorIsSheafCoherentTopology, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π, CategoryTheory.RightExactFunctor.forget_obj, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_restriction_assoc, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_app, CategoryTheory.sheafSectionsNatIsoEvaluation_inv_app, CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_hom_app, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val, CategoryTheory.yoneda'_obj_obj, CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply, SheafOfModules.pushforward_obj_val, Condensed.equalizerCondition_profinite, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, FintypeCat.homMk_apply, PresheafOfModules.Sheafify.mul_smul, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app, Condensed.equalizerCondition, CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected, CategoryTheory.instPreservesFiniteLimitsObjFunctorExactFunctor, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom_hom, CategoryTheory.Mat.id_def, PresheafOfModules.Sheafify.SMulCandidate.h, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpenPowersToOpenₗ, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful, Alexandrov.projSup_map, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso, CategoryTheory.ObjectProperty.ihom_map_hom, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.ObjectProperty.isoInv_hom_id_hom, CategoryTheory.Functor.partialRightAdjointHomEquiv_map_comp, FDRep.endRingEquiv_comp_ρ, id_hom, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom, HomotopicalAlgebra.instWeakEquivalenceHomFullSubcategory, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms, CategoryTheory.GrothendieckTopology.yonedaEquiv_apply, CategoryTheory.MonoOver.mono_obj_hom, SheafOfModules.Finite.evaluationPreservesFiniteLimits, CategoryTheory.Limits.FintypeCat.nonempty_pi_of_nonempty, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, CategoryTheory.AdditiveFunctor.ofRightExact_map_hom, CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app, HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel, CategoryTheory.yoneda'_map_hom, CategoryTheory.Equivalence.sheafCongr.inverse_map_hom_app, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj_obj, CategoryTheory.RightExactFunctor.whiskeringRight_obj_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom, CategoryTheory.MonoOver.isIso_iff_isIso_left, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, CategoryTheory.Sheaf.isTerminalTerminal_from_hom, CategoryTheory.Functor.IsCoverDense.Types.naturality_assoc, Action.FintypeCat.ofMulAction_apply, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv_hom, CategoryTheory.MonoOver.instIsIsoLeftDiscretePUnitHomFullSubcategoryOverIsMono, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, AlgebraicGeometry.Spec.map_app, CategoryTheory.ObjectProperty.SerreClassLocalization.essImage_whiskeringLeft, CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_hom_app, SheafOfModules.unitHomEquiv_apply_coe, CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext_iff, AlgebraicGeometry.tilde.toOpen_map_app, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq, CategoryTheory.Functor.IsCoverDense.Types.naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_def 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct category	—	comp_hom
comp_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct category	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
ext 📖	—	obj	—	—	—
ext_iff 📖	mathematical	—	obj	—	ext
id_def 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct category	—	id_hom
id_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct category	—	—
property 📖	mathematical	—	obj	—	—

---

← Back to Index