Theorems · Theorem · category theory
CategoryTheory.eqToHom_app
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D} (h : F = G) (X : C), (CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom ⋯- Defined in
- Mathlib.CategoryTheory.EqToHom
- Cited by
- 22 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.
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
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
- CategoryTheory.eqToHomstatement and proof · cited by 860
- CategoryTheory.Functor.congr_objstatement · cited by 27
Cited by22
Results whose statement or proof uses this declaration.
- CategoryTheory.ComposableArrows.ext_succproof · cited by 5
- CategoryTheory.shiftFunctorAdd'_add_zeroproof · cited by 3
- CategoryTheory.shiftFunctorAdd'_assocproof · cited by 3
- CategoryTheory.Grothendieck.map_mapproof · cited by 2
- CochainComplex.ι_mapBifunctorShift₁Iso_hom_fproof · cited by 2
- CategoryTheory.Functor.curry_obj_uncurry_objproof · cited by 2
- CategoryTheory.shiftFunctorAdd'_zero_addproof · cited by 2
- CategoryTheory.Grothendieck.map_map_fiberproof · cited by 1
- AlgebraicGeometry.Spec.basicOpen_hom_extproof · cited by 1
- CategoryTheory.pullbackShiftFunctorZero'_inv_appproof · cited by 1
- CategoryTheory.Grothendieck.map_comp_eqproof · cited by 0