mk' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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