instUniversallyInjectiveOfMonoScheme

English

UniversallyInjective is stable under base change: if f is universally injective, then any base change of f is universally injective.

Русский

UniversallyInjective сохраняется при базовом изменении: если f универсально инъективен, то любая базовая замена f также универсальна инъективна.

LaTeX

$$$\text{IsStableUnderBaseChange }(\operatorname{UniversallyInjective}).$$$

Lean4

instance (priority := 900) [Mono f] : UniversallyInjective f :=
  have := (pullback.isIso_diagonal_iff f).mpr inferInstance
  (UniversallyInjective.iff_diagonal f).mpr inferInstance

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