arrow_congr — Mathlib

English

Let A be an object and X,Y be two subobjects of A with X = Y. Then the transport along this equality identifies the corresponding arrows into A; equivalently, the transport of X to Y followed by Y.arrow equals X.arrow.

Русский

Пусть A — объект, X и Y — подпредметы A такие, что X = Y. Тогда перенос по этому равенству идентифицирует соответствующие отображения в A; эквивалентно: перенос X в Y по равенству и затем стрелка Y равны X.arrow.

LaTeX

$$$eqToHom(\\congr_arg(\\lambda S: \\text{Subobject } A\\, S)\\ h) \\;\\gg\\; Y.arrow = X.arrow$$$

Lean4

@[simp]
theorem arrow_congr {A : C} (X Y : Subobject A) (h : X = Y) :
    eqToHom (congr_arg (fun X : Subobject A => (X : C)) h) ≫ Y.arrow = X.arrow :=
  by
  induction h
  simp

Похожие утверждения