Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.ofRestrict_appIso

∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U_1 : (X.restrict h).Opens),
  AlgebraicGeometry.Scheme.Hom.appIso (X.ofRestrict h) U_1 =
    CategoryTheory.Iso.refl
      (X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (X.ofRestrict h)).obj U_1)))

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

1 results in Mathlib

Foundations

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