Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq_hom

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  [inst_1 : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g]
  (e :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)),
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq f g e).hom =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift g f ⋯

Defined in

Mathlib.Geometry.RingedSpace.OpenImmersion

Cited by

0 results in Mathlib

Foundations

Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryAlgebraicGeometry.PresheafedSpace.IsOpenImmersionAlgebraicGeometry.PresheafedSpace.IsOpenImmersion