lift_fac — Mathlib

English

The composition lift f g H with f equals g, i.e., lift f g H ≫ f = g.

Русский

Составление lift f g H удовлетворяет равенству lift f g H followed by f equals g.

LaTeX

$$$lift(f,g,H) \\circ f = g$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_fac {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion f] (H : f.ker ≤ g.ker) :
    lift f g H ≫ f = g := by
  nth_rw 2 [← f.toImage_imageι]
  simp [lift, -Scheme.Hom.toImage_imageι, g.toImage_imageι]

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