Theorems · Theorem · algebraic geometry

AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply

∀ {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) {F : C → C → Type uF} {carrier : C → Type w_1}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier ((X.restrict h).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U)) x =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))))
      x

Defined in

Mathlib.Geometry.RingedSpace.OpenImmersion

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.ConcreteCategory