objEquiv_symm_apply — Mathlib

English

On morphisms f: ⟨m⟩ ⟶ ⟨n⟩, the symm of objEquiv sends f to the corresponding finite morphism; the i-th coordinate matches.

Русский

На морфизмах f: ⟨m⟩ ⟶ ⟨n⟩ симметричный образ objEquiv отправляет f в соответствующий конечный морфизм; i-ая координата совпадает.

LaTeX

$$$(objEquiv)^{−1} f(i) = f(i)$$$

Lean4

@[simp]
theorem objEquiv_symm_apply {n m : ℕ} (f : ⦋m⦌ ⟶ ⦋n⦌) (i : Fin (m + 1)) :
    (objEquiv.{u}.symm f : Δ[n] _⦋m⦌) i = f.toOrderHom i :=
  rfl

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