epi_liftExtend_f_iff — 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 epi_liftExtend_f_iff (hi : e.f i = i') : Epi ((e.liftExtend φ hφ).f i') ↔ Epi (φ.f i) :=
  (MorphismProperty.epimorphisms C).arrow_mk_iso_iff (e.liftExtendfArrowIso φ hφ hi)

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