f_eq — Mathlib

English

Let e: c → c' be an embedding, φ: K.restriction e ⟶ L with hφ: e.HasLift φ. For any i′, i with hi: e.f i = i′, the f-component (e.liftExtend φ hφ).f i′ is epi iff φ.f i is epi.

Русский

Пусть e: c → c' — вложение, φ: K.restriction e ⟶ L, и есть hφ: e.HasLift φ. Для любых i′, i с hi: e.f i = i′, компонент f у (e.liftExtend φ hφ).f i′ эпиморфизм тогда и только тогда, когда φ.f i эпиморфизм.

LaTeX

$$$$ \forall i\, \forall i'\, (hi : e.f i = i'):\quad Epi\big((e.liftExtend φ hφ).f i'\big) \iff Epi(φ.f i) $$$$

Lean4

theorem f_eq {i : ι} {i' : ι'} (h : e.f i = i') :
    f ψ i = (K.restrictionXIso e h).hom ≫ ψ.f i' ≫ (L.extendXIso e h).hom :=
  by
  subst h
  simp [f, restrictionXIso]

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