instLiftSchemeId — Mathlib

English

The diagonal morphism pullback.diagonal f is an immersion (in particular, a mono high-level property).

Русский

Диагональная карта pullback.diagonal f является вложением (в частности, моно).

LaTeX

$$$\\text{IsImmersion}(\\text{pullback.diagonal}(f))$$$

Lean4

instance : IsImmersion (prod.lift (𝟙 X) (𝟙 X)) :=
  by
  rw [← MorphismProperty.cancel_right_of_respectsIso @IsImmersion _ (prodIsoPullback X X).hom]
  convert inferInstanceAs (IsImmersion (pullback.diagonal (terminal.from X)))
  ext : 1 <;> simp

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