Theorems · Theorem · category theory
CategoryTheory.Iso.op_hom
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y), α.op.hom = α.hom.op- Defined in
- Mathlib.CategoryTheory.Opposites
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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 · cited by 32,603
- Oppositestatement · cited by 8,081
- CategoryTheory.Iso.homstatement and proof · cited by 7,684
- CategoryTheory.Isostatement and proof · cited by 3,963
- Quiver.Hom.opstatement · cited by 1,948
- CategoryTheory.Iso.opstatement and proof · cited by 52
Cited by13
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.germ_stalkClosedPointToproof · cited by 4
- AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalkproof · cited by 3
- CompHausLike.LocallyConstant.incl_of_counitAppAppproof · cited by 3
- CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIsoproof · cited by 2
- AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersionproof · cited by 2
- AlgebraicGeometry.IsClosedImmersion.Spec_iffproof · cited by 1
- SimplicialObject.opFunctorCompOpFunctorIso_inv_app_appproof · cited by 0
- AlgebraicGeometry.AffineSpace.SpecIso_hom_appTopproof · cited by 0
- AlgebraicGeometry.Scheme.Hom.normalization.hom_extproof · cited by 0
- AlgebraicGeometry.Scheme.Hom.id_appIsoproof · cited by 0
- AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_compproof · cited by 0
- AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAndproof · cited by 0