Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) {Y : TopCat}
  {f : Y ⟶ TopCat.of ↑↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h)),
  AlgebraicGeometry.PresheafedSpace.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

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category