map_self — Mathlib

English

For any φ: a → b with IsStronglyCocartesian p f φ, the lift over the identity on f, i.e., map p f φ (comp_id f).symm φ, is the identity on b. This expresses that lifting along an identity does nothing new.

Русский

Для φ: a → b со свойством IsStronglyCocartesian p f φ отображение над тождественным морфизмом по f возвращает тождество на b.

LaTeX

$$$\mathrm{map}\ p\ f\ φ\ (\mathrm{comp\_id}\ f)^{\text{-1}}\ φ = \mathrm{id}_b$$$

Lean4

@[simp]
theorem map_self : map p f φ (comp_id f).symm φ = 𝟙 b :=
  by
  subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [comp_id]

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