Documentation Verification Report

Epi

📁 Source: Mathlib/Condensed/Light/Epi.lean

Statistics

Metric	Count
Definitions `Epi`	1
Theorems `epi_iff_locallySurjective_on_lightProfinite`, `instPreservesEpimorphismsLightCondSetForget`, `instReflectsEpimorphismsLightCondSetForget`, `epi_iff_locallySurjective_on_lightProfinite`, `epi_π_app_zero_of_epi`, `instEpiLightCondModMapNat`, `instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim`, `isLocallySurjective_iff_locallySurjective_on_lightProfinite`	8
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
`Epi` 📖	CompData	371 math math: `isSeparating_iff_epi`, `NormalMonoCategory.epi_of_zero_cancel`, `SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc`, `groupCohomology.instEpiModuleCatH2π`, `ShortComplex.SnakeInput.epi_L₃_g`, `epiOfEffectiveEpi`, `Limits.wideCoequalizer.π_epi`, `ShortComplex.ShortExact.epi_δ`, `preserves_epi_of_preservesColimit`, `epi_of_nonzero_to_simple`, `ShortComplex.Exact.epi_kernelLift`, `groupHomology.map₁_quotientGroupMk'_epi`, `SimplicialObject.Splitting.IndexSet.epiComp_fst`, `Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₁_unit_app`, `Localization.epi'`, `SimplicialObject.Splitting.IndexSet.id_fst`, `Abelian.LeftResolution.epi_π_app`, `ModuleCat.epi_as_hom''_mkQ`, `epi_iff_isPushout`, `Abelian.epi_pullback_of_epi_f`, `Abelian.epi_fst_of_factor_thru_epi_mono_factorization`, `SimplicialObject.Splitting.IndexSet.fac_pull_assoc`, `PresheafOfModules.epi_iff_surjective`, `NatTrans.epi_iff_epi_app`, `Limits.coprod.epi_desc_of_epi_right`, `AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'`, `Under.epi_right_of_epi`, `HomologicalComplex.instEpiOpcyclesMapOfF`, `ShortComplex.LeftHomologyData.exact_iff_epi_f'`, `Abelian.Pseudoelement.epi_of_pseudo_surjective`, `CommGrpCat.epi_iff_surjective`, `SimplicialObject.Splitting.PInfty_comp_πSummand_id`, `LightCondSet.epi_iff_locallySurjective_on_lightProfinite`, `NormalMonoCategory.epi_of_zero_cokernel`, `unop_epi_of_mono`, `Over.epi_iff_epi_left`, `CondensedSet.instEpiTopCatAppCounitTopCatAdjunction`, `Abelian.epi_of_mono_of_epi_of_mono'`, `Limits.biprod.epi_desc_of_epi_right`, `PreGaloisCategory.epi_of_nonempty_of_isConnected`, `RegularEpi.epi`, `epi_iff_surjective`, `Limits.colimMap_epi'`, `Preadditive.epi_of_cokernel_iso_zero`, `unop_mono_iff`, `Profinite.effectiveEpi_tfae`, `Limits.kernel_not_epi_of_nonzero`, `ShortComplex.ShortExact.epi_g`, `Limits.cokernel.desc_epi`, `Sheaf.isLocallySurjective_iff_epi`, `epi_comp_iff_of_epi`, `op_epi_iff`, `Under.epi_of_epi_right`, `Functor.epi_map_iff_epi`, `SimplicialObject.Splitting.cofan_inj_eq`, `AlgebraicGeometry.Flat.epi_of_flat_of_surjective`, `Limits.biprod.epi_desc_of_epi_left`, `ConcreteCategory.epi_of_surjective`, `Condensed.epi_iff_surjective_on_stonean`, `AlgebraicGeometry.StructureSheaf.to_basicOpen_epi`, `instEpiSheafTypeToImage`, `Rep.instEpiModuleCatHom`, `Pretriangulated.Triangle.epi₂`, `Abelian.instEpiFactorThruImage`, `Abelian.tfae_epi`, `HomologicalComplex.instEpiFπTruncGE`, `NonemptyFinLinOrd.epi_iff_surjective`, `epi_of_epi`, `ShortComplex.SnakeInput.instEpiGL₀'`, `Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi`, `SheafOfModules.GeneratingSections.epi`, `Limits.image.preComp_epi_of_epi`, `epi_comp'`, `Limits.Cofork.IsColimit.epi`, `Profinite.epi_iff_surjective`, `NatTrans.epi_iff_epi_app'`, `Limits.coprod.epi_desc_of_epi_left`, `epi_comp`, `SemiNormedGrp.explicitCokernelπ.epi`, `HomologicalComplex.instEpiFOfHasFiniteColimits`, `Abelian.epi_of_epi_of_epi_of_mono'`, `SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq`, `HomologicalComplex.instEpiGShortComplexTruncLE`, `SimplicialObject.Splitting.IndexSet.ext'`, `Limits.coequalizer.π_epi`, `ShortComplex.epi_of_epi_of_epi_of_epi`, `Abelian.epi_factorThruCoimage`, `SimplicialObject.Splitting.IndexSet.mk_snd_coe`, `Localization.epi`, `Abelian.epi_of_epi_of_epi_of_mono`, `ShortComplex.Splitting.epi_g`, `ModuleCat.epi_iff_surjective`, `HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat`, `AlgebraicTopology.DoldKan.Γ₂_obj_p_app`, `Stonean.effectiveEpiFamily_tfae`, `Adjunction.Quadruple.epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft`, `Endofunctor.Algebra.epi_of_epi`, `Sheaf.epi_of_isLocallySurjective'`, `Preadditive.epi_iff_cancel_zero`, `ShortComplex.instEpiPOpcycles`, `ConcreteCategory.epi_iff_surjective_of_preservesPushout`, `ShortComplex.RightHomologyData.instEpiP`, `groupCohomology.cochainsMap_f_map_epi`, `Abelian.epi_of_epi_of_epi_of_epi`, `PresheafOfModules.epi_of_surjective`, `SimplicialObject.Splitting.IndexSet.eqId_iff_mono`, `Over.epi_of_epi_left`, `Functor.map_epi`, `SSet.Subcomplex.instEpiToImage`, `groupHomology.epi_δ_of_isZero`, `Sheaf.isLocallySurjective_iff_epi'`, `instEpiId`, `CondensedMod.epi_iff_surjective_on_stonean`, `PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp`, `Stonean.epi_iff_surjective`, `NonPreadditiveAbelian.instEpiFactorThruImage`, `CondensedSet.epi_iff_surjective_on_stonean`, `Abelian.LeftResolution.instEpiKaroubiAppπ'`, `groupCohomology.epi_δ_of_isZero`, `SimplicialObject.Splitting.IndexSet.mk_fst`, `groupCohomology.instEpiModuleCatH1π`, `Adjunction.Quadruple.epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight`, `Functor.homologySequence_epi_shift_map_mor₁_iff`, `SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero`, `Abelian.epi_kernel_map_of_isPushout`, `ShortComplex.Exact.epi_toCycles`, `groupHomology.chainsMap_f_map_epi`, `StrongEpi.epi`, `Limits.biprod.map_epi`, `Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone`, `HomologicalComplex.instEpiHomologyπ`, `StructuredArrow.epi_homMk`, `ComplexShape.Embedding.epi_liftExtend_f_iff`, `ShortComplex.SnakeInput.epi_v₂₃_τ₂`, `Preadditive.epi_iff_surjective`, `Rep.instEpiModuleCatAppActionCoinvariantsMk`, `Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi`, `Functor.PreservesEpimorphisms.preserves`, `Limits.pushout.inl_of_epi`, `epi_of_strongEpi`, `ChainComplex.isIso_descOpcycles_iff`, `AlgebraicGeometry.isIso_iff_isOpenImmersion`, `CostructuredArrow.epi_homMk`, `LightCondSet.instEpiTopCatAppCounitTopCatAdjunction`, `Abelian.epi_snd_of_isLimit`, `CommRingCat.epi_iff_tmul_eq_tmul`, `NonPreadditiveAbelian.epi_r`, `Limits.instEpiπ`, `ShortComplex.exact_iff_epi_toCycles`, `ShortComplex.exact_and_epi_g_iff_g_is_cokernel`, `Condensed.epi_iff_locallySurjective_on_compHaus`, `Preadditive.epi_of_isZero_cokernel`, `DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff`, `Preadditive.epi_iff_isZero_cokernel`, `GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex`, `groupHomology.chainsMap_id_f_map_epi`, `Limits.prod.map_epi`, `SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty`, `SimplicialObject.Splitting.cofan_inj_πSummand_eq_id`, `Limits.epi_of_epi_image`, `Adjunction.Quadruple.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app`, `groupHomology.instEpiModuleCatGH1CoresCoinf`, `ObjectProperty.isSeparating_iff_epi`, `CommRingCat.epi_iff_epi`, `ShortComplex.Exact.epi_f`, `MorphismProperty.epimorphisms.iff`, `SimplicialObject.Splitting.IndexSet.fac_pull`, `SimplicialObject.Split.cofan_inj_naturality_symm_assoc`, `Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi`, `kernelCokernelCompSequence.instEpiπ`, `Limits.PushoutCocone.epi_of_isColimitMkIdId`, `Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair`, `TopCat.Presheaf.epi_toLocalizationPresheaf`, `AddCommGrpCat.epi_iff_surjective`, `ShortComplex.quasiIso_iff_of_zeros'`, `imageToKernel_epi_of_zero_of_mono`, `Subfunctor.Subpresheaf.epi_iff_range_eq_top`, `Pretriangulated.Triangle.mor₂_eq_zero_iff_epi₁`, `AlgebraicTopology.DoldKan.Γ₀_map_app`, `epi_iff_inl_eq_inr`, `Adjunction.counit_epi_of_R_faithful`, `instEpiMap'KernelCokernelCompSequenceOfNatNat`, `IsLocalization.epi`, `AlgebraicGeometry.SheafedSpace.epi_of_base_surjective_of_stalk_mono`, `AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc`, `CostructuredArrow.epi_of_epi_left`, `SimplicialObject.Splitting.IndexSet.id_snd_coe`, `Subfunctor.instEpiFunctorTypeToRange`, `epi_of_epi_fac`, `RingHom.surjective_iff_epi_and_finite`, `CostructuredArrow.epi_left_of_epi`, `ExtremalEpi.toEpi`, `Abelian.epi_of_mono_of_epi_of_mono`, `SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero`, `AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base`, `epi_comp_iff_of_isIso`, `Limits.epi_coprod_to_pushout`, `Projective.π_epi`, `AddCommGrpCat.epi_iff_range_eq_top`, `SimplicialObject.Splitting.IndexSet.instEpiSimplexCategoryE`, `SimplicialObject.Splitting.cofan_inj_comp_app`, `Limits.IsZero.epi`, `AlgebraicTopology.DoldKan.Γ₀.map_app`, `IsPushout.epi_shortComplex_g`, `SimplexCategory.instEpiσ`, `Limits.imageSubobject_comp_le_epi_of_epi`, `unop_epi_iff`, `op_mono_iff`, `Abelian.epi_pullback_of_epi_g`, `SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc`, `instEpiAppOfFunctor`, `ShortComplex.Exact.epi_f'`, `isSeparator_iff_epi`, `Adjunction.Triple.epi_rightToLeft_app_iff`, `ShortComplex.epi_τ₂_of_exact_of_epi`, `Monad.algebra_epi_of_epi`, `GlueData.π_epi`, `Preadditive.epi_of_cokernel_zero`, `isIso_iff_mono_and_epi`, `CompHausLike.epi_of_surjective`, `SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc`, `IsSplitEpi.epi`, `ShortComplex.SnakeInput.epi_v₂₃_τ₃`, `PresheafOfModules.instEpiFromFreeYonedaCoproduct`, `CompHaus.effectiveEpi_tfae`, `SimplicialObject.Splitting.decomposition_id`, `ShortComplex.instEpiCokernelToAbelianCoimage`, `Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂`, `Limits.instEpiFst`, `ShortComplex.exact_and_epi_g_iff_of_iso`, `Over.epi_homMk`, `Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi`, `groupHomology.instEpiModuleCatH1π`, `Sheaf.Hom.epi_of_presheaf_epi`, `Square.IsPushout.epi_f₂₄`, `Abelian.LeftResolution.instEpiKaroubiAppπ`, `groupHomology.instEpiModuleCatH2π`, `ShortComplex.exact_iff_epi_imageToKernel`, `groupCohomology.cochainsMap_id_f_map_epi`, `CompHaus.presentation.epi_π`, `Limits.colimitQuotientCoproduct_epi`, `Preadditive.epi_of_isZero_cokernel'`, `LightCondMod.epi_iff_locallySurjective_on_lightProfinite`, `Pretriangulated.Triangle.epi₃`, `Sheaf.epi_of_isLocallySurjective`, `ShortComplex.SnakeInput.epi_δ`, `groupHomology.instEpiModuleCatH0π`, `Preadditive.epi_iff_isZero_cokernel'`, `SimplicialObject.Splitting.IndexSet.epiComp_snd_coe`, `HomologicalComplex.epi_homologyMap_shortComplexTruncLE_g`, `TopCat.epi_iff_surjective`, `SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc`, `SimplicialObject.Split.natTransCofanInj_app`, `CondensedMod.epi_iff_locallySurjective_on_compHaus`, `HomologicalComplex.epi_homologyMap_of_epi_of_not_rel`, `ShortComplex.exact_iff_epi_kernel_lift`, `SSet.Finite.exists_epi_from_isCardinalPresentable`, `ComposableArrows.IsComplex.epi_cokerToKer'`, `AddGrpCat.epi_iff_range_eq_top`, `AddGrpCat.epi_iff_surjective`, `Limits.instEpiSnd`, `Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃`, `op_epi_of_mono`, `Over.epi_left_of_epi`, `Abelian.epi_of_cokernel_π_eq_zero`, `CompHaus.epi_iff_surjective`, `Limits.IsInitial.epi_to`, `SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc`, `Arrow.epi_right`, `TopModuleCat.instEpiCokerπ`, `Square.IsPushout.epi_f₃₄`, `Limits.coprod.map_epi`, `LightProfinite.epi_iff_surjective`, `Subobject.epi_iff_mk_eq_top`, `SimplicialObject.Splitting.comp_PInfty_eq_zero_iff`, `Functor.epi_of_epi_map`, `Limits.epi_image_of_epi`, `ShortComplex.instEpiLeftHomologyπ`, `Idempotents.DoldKan.Γ_map_app`, `Endofunctor.Coalgebra.epi_of_epi`, `groupHomology.instEpiModuleCatGShortComplexH0`, `Limits.epi_of_isColimit_parallelFamily`, `AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app`, `Linear.instEpiHSMulHomOfInvertible`, `SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero`, `IsIso.epi_of_iso`, `groupHomology.H1CoresCoinfOfTrivial_g_epi`, `Abelian.epi_fst_of_isLimit`, `Limits.HasZeroObject.instEpi`, `Profinite.presentation.epi_π`, `SimplicialObject.Splitting.IndexSet.eqId_iff_eq`, `epi_iff_isIso_inl`, `SSet.Subcomplex.instEpiToRange`, `Limits.epi_of_target_iso_zero`, `Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₂_counit_app`, `SSet.Subcomplex.range_eq_top_iff`, `AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued`, `ShortComplex.LeftHomologyData.instEpiπ`, `ShortComplex.epi_homologyMap_of_epi_cyclesMap`, `ProjectivePresentation.epi`, `epi_iff_surjective_up_to_refinements`, `Pretriangulated.Triangle.epi₁`, `Comonad.algebra_epi_of_epi`, `LightProfinite.instEpiAppOppositeNatπAsLimitCone`, `Rep.epi_iff_surjective`, `AlgebraicTopology.DoldKan.Γ₂_map_f_app`, `ShortComplex.epi_of_mono_of_epi_of_mono`, `Preadditive.epi_iff_surjective'`, `ShortComplex.Exact.epi_f_iff`, `instEpiOfIsThin`, `groupHomology.epi_map_0_of_epi`, `ShortComplex.SnakeInput.epi_L₁_g`, `GrpCat.epi_iff_range_eq_top`, `imageToKernel_epi_of_epi_of_zero`, `HomologicalComplex.instEpiπTruncGE`, `ObjectProperty.IsCoseparating.epi_iff`, `Preadditive.epi_of_cancel_zero`, `Under.epi_homMk`, `HomologicalComplex.instEpiPOpcycles`, `AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'`, `GrpCat.epi_iff_surjective`, `CompHaus.effectiveEpiFamily_tfae`, `CondensedSet.epi_iff_locallySurjective_on_compHaus`, `AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ`, `CommGrpCat.epi_iff_range_eq_top`, `ProjectiveResolution.instEpiFNatπ`, `CostructuredArrow.epi_iff_epi_left`, `SimplexCategory.instEpiFactorThruImage`, `ShortComplex.exact_iff_epi`, `ObjectProperty.IsSeparating.epi_coproductFrom`, `DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff`, `Limits.map_π_epi`, `SimplicialObject.Split.cofan_inj_naturality_symm`, `ModuleCat.epi_iff_range_eq_top`, `SimplicialObject.Splitting.cofan_inj_comp_app_assoc`, `Profinite.effectiveEpiFamily_tfae`, `ShortComplex.epi_homologyMap_of_epi_cyclesMap'`, `ShortComplex.exact_iff_epi_imageToKernel'`, `SimplexCategory.epi_iff_surjective`, `Subfunctor.epi_iff_range_eq_top`, `AlgebraicGeometry.Scheme.instEpiCommRingCatResidue`, `epi_iff_isIso_inr`, `ModuleCat.smulShortComplex_g_epi`, `SplitEpi.epi`, `SimplicialObject.Splitting.cofan_inj_eq_assoc`, `instEpiFunctorWhiskerRightOfPreservesEpimorphisms`, `groupHomology.mapCycles₁_quotientGroupMk'_epi`, `AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc`, `ShortComplex.SnakeInput.epi_v₂₃_τ₁`, `ShortComplex.instEpiGCokernelSequence`, `Limits.Multicoequalizer.instEpiSigmaπ`, `Preadditive.instEpiNegHom`, `IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f`, `Limits.instEpiFactorThruImageSubobjectOfHasEqualizers`, `Functor.ReflectsEpimorphisms.reflects`, `Stonean.effectiveEpi_tfae`, `epi_of_effectiveEpi`, `StructuredArrow.epi_of_epi_right`, `JointlyReflectEpimorphisms.epi_iff`, `IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f`, `SimplicialObject.Splitting.IndexSet.eqId_iff_len_le`, `epi_iff_forall_injective`, `ShortComplex.instEpiHomologyπ`, `Functor.homologySequence_epi_shift_map_mor₂_iff`, `Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `Limits.instEpiDescι`, `HomologicalComplex.instEpiFRestrictionToTruncGE'`, `reflects_epi_of_reflectsColimit`, `Limits.epi_of_isColimit_cofork`, `Limits.pushout.inr_of_epi`, `Adjunction.Quadruple.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app`

LightCondMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_locallySurjective_on_lightProfinite` 📖	mathematical	—	`CategoryTheory.Epi` `LightCondMod` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `Opposite.op` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	`CategoryTheory.Sheaf.isLocallySurjective_iff_epi'` `CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `ModuleCat.forget_preservesMonomorphisms` `ModuleCat.forget_preservesEpimorphisms` `LightProfinite.instWEqualsLocallyBijectiveCoherentTopology` `ModuleCat.hasLimits'` `ModuleCat.hasColimitsOfSize` `AddCommGrpCat.hasColimitsOfSize` `UnivLE.self` `ModuleCat.FilteredColimits.forget_preservesFilteredColimits` `ModuleCat.forget_preservesLimits` `ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier` `LightProfinite.hasSheafify` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite` `CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits`
`instPreservesEpimorphismsLightCondSetForget` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `LightCondMod` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `LightCondSet` `CategoryTheory.types` `LightCondensed.forget`	—	`CategoryTheory.Sheaf.isLocallySurjective_iff_epi'` `CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom` `LightProfinite.instWEqualsLocallyBijectiveCoherentTopology` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfSize` `CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits` `CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom` `CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `LightProfinite.hasSheafify_type` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.SheafOfTypes.balanced` `CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget` `CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `ModuleCat.forget_preservesMonomorphisms` `ModuleCat.forget_preservesEpimorphisms` `ModuleCat.hasLimits'` `ModuleCat.hasColimitsOfSize` `AddCommGrpCat.hasColimitsOfSize` `ModuleCat.FilteredColimits.forget_preservesFilteredColimits` `ModuleCat.forget_preservesLimits` `ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier` `LightProfinite.hasSheafify` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory`
`instReflectsEpimorphismsLightCondSetForget` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsEpimorphisms` `LightCondMod` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `LightCondSet` `CategoryTheory.types` `LightCondensed.forget`	—	`CategoryTheory.Sheaf.isLocallySurjective_iff_epi'` `CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization` `CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations` `ModuleCat.forget_preservesMonomorphisms` `ModuleCat.forget_preservesEpimorphisms` `LightProfinite.instWEqualsLocallyBijectiveCoherentTopology` `ModuleCat.hasLimits'` `ModuleCat.hasColimitsOfSize` `AddCommGrpCat.hasColimitsOfSize` `UnivLE.self` `ModuleCat.FilteredColimits.forget_preservesFilteredColimits` `ModuleCat.forget_preservesLimits` `ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier` `LightProfinite.hasSheafify` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget` `CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom` `CategoryTheory.Limits.Types.hasLimitsOfSize` `CategoryTheory.Limits.Types.hasColimitsOfSize` `CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits` `CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom` `CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `LightProfinite.hasSheafify_type` `CategoryTheory.Functor.corepresentable_preservesLimit` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.SheafOfTypes.balanced`

LightCondSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_locallySurjective_on_lightProfinite` 📖	mathematical	—	`CategoryTheory.Epi` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `CategoryTheory.NatTrans.app` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.Sheaf.Hom.val` `Opposite.op` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	`CategoryTheory.Sheaf.isLocallySurjective_iff_epi'` `CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom` `LightProfinite.instWEqualsLocallyBijectiveCoherentTopology` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfSize` `CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits` `CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom` `CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `LightProfinite.hasSheafify_type` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.SheafOfTypes.balanced` `LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite` `CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits`

LightCondensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_π_app_zero_of_epi` 📖	mathematical	`CategoryTheory.Epi` `LightCondMod` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Nat.instPreorder` `Opposite.op` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE`	`CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	—	`CategoryTheory.Functor.epi_of_epi_map` `LightCondMod.instReflectsEpimorphismsLightCondSetForget` `CategoryTheory.coherentTopology.epi_π_app_zero_of_epi` `LightProfinite.instPreregular` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CategoryTheory.Limits.instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory` `LightProfinite.instHasCountableLimits` `CategoryTheory.countableCategoryOpposite` `CategoryTheory.instCountableCategoryNat` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map` `LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology` `LightProfinite.hasSheafify_type` `CategoryTheory.SheafOfTypes.balanced` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `LightProfinite.instWEqualsLocallyBijectiveCoherentTopology` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfSize` `CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits` `CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom` `CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `CategoryTheory.Adjunction.isRightAdjoint` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `CategoryTheory.Functor.map_epi` `LightCondMod.instPreservesEpimorphismsLightCondSetForget`
`instEpiLightCondModMapNat` 📖	mathematical	`CategoryTheory.Epi` `LightCondMod` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory`	`CategoryTheory.Limits.piObj` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable` `CategoryTheory.Limits.hasCountableProducts_of_hasProducts` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `instHasLimitsOfSizeLightCondMod_1` `instCountableNat` `CategoryTheory.Discrete.functor` `CategoryTheory.Limits.Pi.map`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable` `CategoryTheory.Limits.hasCountableProducts_of_hasProducts` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `instHasLimitsOfSizeLightCondMod_1` `instCountableNat` `epi_π_app_zero_of_epi` `CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ` `CategoryTheory.Limits.SequentialProduct.functorMap_epi` `CategoryTheory.Abelian.hasFiniteBiproducts`
`instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `CategoryTheory.Functor` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `LightCondMod` `instCategoryLightCondensed` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Functor.category` `CategoryTheory.Limits.lim` `CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable` `CategoryTheory.Limits.hasCountableProducts_of_hasProducts` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `instHasLimitsOfSizeLightCondMod_1` `instCountableNat`	—	`CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable` `CategoryTheory.Limits.hasCountableProducts_of_hasProducts` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `instHasLimitsOfSizeLightCondMod_1` `instCountableNat` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.limit.hom_ext` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp` `CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp_assoc` `CategoryTheory.epi_comp` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.IsSplitEpi.EffectiveEpi` `CategoryTheory.IsSplitEpi.of_iso` `CategoryTheory.Iso.isIso_inv` `instEpiLightCondModMapNat` `CategoryTheory.instEpiAppOfFunctor` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Abelian.hasFiniteColimits` `CategoryTheory.Iso.isIso_hom`
`isLocallySurjective_iff_locallySurjective_on_lightProfinite` 📖	mathematical	—	`CategoryTheory.Sheaf.IsLocallySurjective` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.coherentTopology` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `Opposite.op` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	`LightProfinite.instPreregular` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CategoryTheory.coherentTopology.isLocallySurjective_iff` `CategoryTheory.regularTopology.isLocallySurjective_iff`

---

← Back to Index