Theorems · Definition · category theory
CategoryTheory.inv
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f : X ⟶ Y) → [I : CategoryTheory.IsIso f] → Y ⟶ XThe inverse of a morphism f when we have [IsIso f].
- Defined in
- Mathlib.CategoryTheory.Iso
- Cited by
- 467 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 20 definitions · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.IsIsostatement and proof · cited by 1,156
- CategoryTheory.IsIso.outproof · cited by 2
Cited by522
Results whose statement or proof uses this declaration.
- CategoryTheory.asIsoproof · cited by 177
- CategoryTheory.IsIso.hom_inv_idstatement · cited by 97
- CategoryTheory.IsIso.inv_hom_idstatement · cited by 88
- CategoryTheory.MorphismProperty.LeftFraction.mapproof · cited by 43
- CategoryTheory.Functor.map_invstatement and proof · cited by 38
- CategoryTheory.IsIso.inv_hom_id_assocstatement and proof · cited by 37
- CategoryTheory.MorphismProperty.cancel_left_of_respectsIsoproof · cited by 33
- CategoryTheory.IsIso.Iso.inv_invstatement · cited by 30
- CategoryTheory.IsIso.hom_inv_id_assocstatement and proof · cited by 29
- CategoryTheory.IsIso.inv_eq_of_hom_inv_idstatement and proof · cited by 24
- AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invAppproof · cited by 24
- CategoryTheory.inv.congr_simpstatement and proof · cited by 23
Showing the 200 most cited of 522.