Mathlib Map

Theorems · Definition · combinatorics

Quiver.homOfEq

{V : Type u_1} → [inst : Quiver V] → {X Y X' Y' : V} → (X ⟶ Y) → X = X' → Y = Y' → (X' ⟶ Y')

An arrow in a quiver can be transported across equalities between the source and target objects.

Defined in
Mathlib.Combinatorics.Quiver.Basic
Cited by
21 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
Quiver
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Quiv.homEquivOfIso · cited by 2Quiv.homEquivOfIsoCategoryTheory.Quiv.hom_map_inv_map_of_iso · cited by 1Quiv.hom_map_inv_map_of_i…Quiver.homOfEq_rfl · cited by 1Quiver.homOfEq_rflSSet.OneTruncation₂.homOfEq_edge · cited by 1OneTruncation₂.homOfEq_ed…Quiver.homOfEq.congr_simp · cited by 1homOfEq.congr_simpCategoryTheory.ReflPrefunctor.congr_hom · cited by 1ReflPrefunctor.congr_homPrefunctor.congr_hom · cited by 1Prefunctor.congr_homPrefunctor.ext' · cited by 1Prefunctor.ext'Quiver.heq_of_homOfEq_ext · cited by 1Quiver.heq_of_homOfEq_extCategoryTheory.Quiv.homEquivOfIso_symm_apply · cited by 0Quiv.homEquivOfIso_symm_a…CategoryTheory.Quiv.homOfEq_map_homOfEq · cited by 0Quiv.homOfEq_map_homOfEqPrefunctor.homOfEq_map · cited by 0Prefunctor.homOfEq_mapQuiver.homOfEq_injective · cited by 0Quiver.homOfEq_injectiveQuiver.homOfEq_trans · cited by 0Quiver.homOfEq_transCategoryTheory.Quiv.inv_map_hom_map_of_iso · cited by 0Quiv.inv_map_hom_map_of_i…Quiver.Hom · cited by 32603Quiver.HomQuiver · cited by 405QuiverQuiver.homOfEqCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Quiver.Homstatement and proof · cited by 32,603
  • Quiverstatement and proof · cited by 405

Cited by23

Results whose statement or proof uses this declaration.