Theorems · Theorem · algebraic geometry

AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) {Y : TopCat}
  {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace),
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U =
    CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))

Defined in

Mathlib.Geometry.RingedSpace.OpenImmersion

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category