of_retract — Mathlib

English

A standard stability result: if a property P is stable under retracts, then the retracts of monomorphisms (or epimorphisms) inherit the property. In particular, the class of monomorphisms is stable under retracts.

Русский

Стандартное свойство стабильности: если свойство P стабильно по ретракциям, то ретракты мономорфизмов наследуют это свойство. Особо: множество мономорфизмов стабильно по ретракциям.

LaTeX

$$$\text{If }P\text{ is stable under retracts, and }f\text{ is a retract of }g\text{ with }g\text{ mono, then }f\text{ is mono.}$$$

Lean4

theorem of_retract {P : MorphismProperty C} [P.IsStableUnderRetracts] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
    (h : RetractArrow f g) (hg : P g) : P f :=
  IsStableUnderRetracts.of_retract h hg

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