Structures · Category theory
CategoryTheory.Balanced
A category is called balanced if any morphism that is both monic and epic is an isomorphism.
- Defined in
- Mathlib.CategoryTheory.Balanced
- Shape
- One type argument · adds isIso_of_mono_of_epi
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- CategoryTheory.Sheaf
- SSet
- SimplexCategory
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by78
- CategoryTheory.isIso_of_mono_of_epi
- CategoryTheory.ShortComplex.Exact.fIsKernel
- CategoryTheory.ShortComplex.Exact.gIsCokernel
- CategoryTheory.ShortComplex.Exact.lift_f
- CategoryTheory.ShortComplex.Exact.lift
- CategoryTheory.Balanced.isIso_of_mono_of_epi
- CategoryTheory.ShortComplex.Exact.desc
- CategoryTheory.ComposableArrows.Exact.cokerIsoKer'
- CategoryTheory.ShortComplex.Exact.g_desc
- CategoryTheory.Sheaf.isLocallySurjective_iff_epi'
- CategoryTheory.ObjectProperty.IsSeparating.isDetecting
- CategoryTheory.IsSeparator.isDetector
- CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles
- CategoryTheory.ComposableArrows.Exact.cokerIsoKer
- CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac
- CategoryTheory.ShortComplex.mono_τ₂_of_exact_of_mono
- CategoryTheory.ShortComplex.ShortExact.fIsKernel
- Condensed.epi_iff_locallySurjective_on_compHaus
- Condensed.epi_iff_surjective_on_stonean
- CategoryTheory.isIso_iff_mono_and_epi
- CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting
- CategoryTheory.ShortComplex.Exact.isIso_g'
- CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel
- CategoryTheory.ShortComplex.Exact.g_desc_assoc
- CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel
- CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃
- CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id
- CategoryTheory.ComposableArrows.Exact.isIso_map'
- CategoryTheory.ShortComplex.ShortExact.gIsCokernel
- CategoryTheory.JointlyFaithful.jointlyReflectsIsomorphisms
- TopCat.Sheaf.isLocallySurjective_iff_epi
- CategoryTheory.coherentTopology.epi_π_app_zero_of_epi
- CategoryTheory.ShortComplex.Exact.isIso_f'
- CategoryTheory.ShortComplex.ShortExact.splittingOfInjective
- CategoryTheory.isDetector_separator
- CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel
- CategoryTheory.ShortComplex.Splitting.ofExactOfRetraction
- CategoryTheory.ShortComplex.epi_τ₂_of_exact_of_epi
- CategoryTheory.IsCoseparator.isCodetector
- CategoryTheory.isCodetector_coseparator
- CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac
- CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id
- CategoryTheory.Subobject.epi_iff_mk_eq_top
- CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃'
- CategoryTheory.ObjectProperty.isDetecting_iff_isSeparating
- CategoryTheory.ShortComplex.Exact.lift'
- CategoryTheory.ShortComplex.Exact.desc'
- CategoryTheory.Functor.balanced_of_preserves
- CategoryTheory.ShortComplex.Splitting.ofExactOfSection
- CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc
Ancestors0
No ancestors.