mk' — Mathlib

English

If f is epi and satisfies a lifting property for all squares in a certain mono-epimorphism setup, then f is StrongEpi.

Русский

Если f является эпиморфизмом и удовлетворяет свойству подъема для всех квадратов в данной конфигурации моно-эпиморфизмов, то f является сильным эпиморфизмом.

LaTeX

$$$\forall f: P \to Q, [Epi f] \Rightarrow (\forall X Y z, (Mono z) \to (u: P \to X) (v: Q \to Y) (sq: CommSq u f z v), sq.HasLift) \Rightarrow \text{StrongEpi } f$$$

Lean4

theorem mk' {f : P ⟶ Q} [Epi f]
    (hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Mono z) (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v), sq.HasLift) :
    StrongEpi f :=
  { epi := inferInstance
    llp := fun {X Y} z hz => ⟨fun {u v} sq => hf X Y z hz u v sq⟩ }

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