map — Mathlib

English

The map Mk₁.map sends a morphism f : X₀ ⟶ X₁ to a family of morphisms in Fin 2 respecting the order, namely the identity on diagonal entries and f on the (0,1) entry.

Русский

Функция Mk₁.map отправляет морфизм f: X₀ ⟶ X₁ в семейство морфизмов в Fin 2, сохраняющее порядок: единицы по диагонали и f в позиции (0,1).

LaTeX

$${ map : ∀ (i j : Fin 2) (h : i ≤ j),\; obj X₀ X₁ i ⟶ obj X₀ X₁ j | ⟨0, _⟩, ⟨0, _⟩, _ => 𝟙 _ | ⟨0, _⟩, ⟨1, _⟩, _ => f | ⟨1, _⟩, ⟨1, _⟩, _ => 𝟙 _ }$$

Lean4

/-- The obvious map `obj X₀ X₁ i ⟶ obj X₀ X₁ j` whenever `i j : Fin 2` satisfy `i ≤ j`. -/
@[simp]
def map : ∀ (i j : Fin 2) (_ : i ≤ j), obj X₀ X₁ i ⟶ obj X₀ X₁ j
  | ⟨0, _⟩, ⟨0, _⟩, _ => 𝟙 _
  | ⟨0, _⟩, ⟨1, _⟩, _ => f
  | ⟨1, _⟩, ⟨1, _⟩, _ => 𝟙 _

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