Theorems · Theorem · category theory
CategoryTheory.eqToHom_op
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y),
(CategoryTheory.eqToHom h).op = CategoryTheory.eqToHom ⋯- Defined in
- Mathlib.CategoryTheory.EqToHom
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Quiver.Hom.opstatement and proof · cited by 1,948
- CategoryTheory.eqToHomstatement and proof · cited by 860
Cited by68
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.appIso_homproof · cited by 8
- TopCat.Sheaf.eq_of_locally_eq'proof · cited by 6
- AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_appproof · cited by 5
- AlgebraicGeometry.IsAffineOpen.exists_basicOpen_leproof · cited by 5
- AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturalityproof · cited by 4
- AlgebraicGeometry.morphismRestrict_appproof · cited by 4
- AlgebraicGeometry.Proj.awayι_comp_mapproof · cited by 3
- AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTopproof · cited by 3
- TopCat.Presheaf.pushforwardEq_hom_appproof · cited by 3
- AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_topproof · cited by 3
- AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTopproof · cited by 3
- CategoryTheory.compatiblePreservingOfFlatproof · cited by 3