Theorems · Theorem · category theory
CategoryTheory.isIso_iff_bijective
∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.IsIso f ↔ Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)A morphism in Type u is an isomorphism if and only if it is bijective.
- Defined in
- Mathlib.CategoryTheory.Types.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- TypeCat.Funstatement · cited by 1,307
- CategoryTheory.IsIsostatement and proof · cited by 1,156
- Function.Bijectivestatement and proof · cited by 863
- CategoryTheory.asIsoproof · cited by 177
- Equiv.bijectiveproof · cited by 132
- Equiv.ofBijectiveproof · cited by 70
- Equiv.toIsoproof · cited by 58
- CategoryTheory.Iso.toEquivproof · cited by 32
Cited by16
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.Types.isPullback_iffproof · cited by 4
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'proof · cited by 4
- CategoryTheory.Presieve.isSheafFor_of_preservesProductproof · cited by 2
- TopCat.Presheaf.app_isIso_of_stalkFunctor_map_isoproof · cited by 2
- CategoryTheory.Limits.Types.isPushout_of_isPullback_of_monoproof · cited by 1
- CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquivproof · cited by 1
- IsCoveringMap.monodromy_bijectiveproof · cited by 1
- CategoryTheory.isCodetector_iff_reflectsIsomorphisms_yoneda_objproof · cited by 0
- CategoryTheory.Monoidal.Reflective.isIso_tfaeproof · cited by 0
- CategoryTheory.Types.isStrongGenerator_punitproof · cited by 0