isoOfRangeEq_hom_fac — Mathlib

English

The hom component of the isomorphism between X and Y obtained from equal opens is given by lift g f (le_of_eq e).

Русский

Гом-компонента изоморфизма между X и Y, полученного из равных образов открытий, задаётся как lift g f (le_of_eq e).

LaTeX

$$$ (\text{isoOfRangeEq } f g e).hom = \text{lift } g f (le\_of\_eq e) $$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfRangeEq_hom_fac {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g]
    (e : Set.range f.base = Set.range g.base) : (isoOfRangeEq f g e).hom ≫ g = f :=
  lift_fac _ _ (le_of_eq e)

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