extend_hom_app — Mathlib

English

Compatibility of the equivalence with respect to a basis: evaluating the equivalence on a basis element recovers the original morphism component.

Русский

Совместимость эквивалентности относительно базиса: при применении эквивалентности к элементу базиса восстанавливается исходный компонент морфизма.

LaTeX

$$$\text{extend_hom_app}(h,\alpha,i):\; (\text{restrictHomEquivHom } F F' h \alpha).app (op (B i)) = \alpha.app (op i)$$$

Lean4

@[simp]
theorem extend_hom_app (h : Opens.IsBasis (Set.range B)) (α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.1)
    (i : ι) : (restrictHomEquivHom F F' h α).app (op (B i)) = α.app (op i) :=
  by
  nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]
  rfl

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