Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp

∀ (X : AlgebraicGeometry.LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace),
  AlgebraicGeometry.LocallyRingedSpace.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 95 from the axioms · uses propext, Classical.choice, Quot.sound