map_id — Mathlib

English

The map at i=i is the identity map, by case analysis.

Русский

Отображение при i=i равно тождественному отображению.

LaTeX

$$$\\text{map}\\; hj\\; F\\; τ\\; i\\; i = \\mathit{id}$$$

Lean4

@[simp]
theorem map_id (i : J) (hi : i ≤ Order.succ j) : map hj F τ i i (by rfl) hi = 𝟙 _ :=
  by
  dsimp [map]
  by_cases h₁ : i ≤ j
  · rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]
  · obtain rfl : i = Order.succ j := le_antisymm hi (Order.succ_le_of_lt (not_le.1 h₁))
    rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj), dif_neg h₁]

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