isIso_lift — Mathlib

English

If i1,i2: Z1,Z2 → X are closed immersions with equal kernels, then lift i1 i2 h is an isomorphism.

Русский

Если равны ядра замкнутых вложений i1,i2, то lift i1 i2 h является изоморфизмом.

LaTeX

$$IsIso(lift i1 i2 h)$$

Lean4

theorem isIso_lift {Z₁ Z₂ X : Scheme.{u}} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [IsClosedImmersion i₁] [IsClosedImmersion i₂]
    (h : i₁.ker = i₂.ker) : IsIso (lift i₁ i₂ h.le) :=
  isIso_of_ker_eq i₂ i₁ _ (by simp) h.symm

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