isoOfRangeEq_inv_fac — Mathlib

English

The inverse component of the same isomorphism is given by lift f g (le_of_eq e.symm).

Русский

Обратная составляющая изоморфизма задаётся как lift f g (le_of_eq e.symm).

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem isoOfRangeEq_inv_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).inv ≫ f = g :=
  lift_fac _ _ (le_of_eq e.symm)

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