Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.ofRestrict_appLE

∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : X.Opens) (W : (X.restrict h).Opens)
  (e : W ≤ (TopologicalSpace.Opens.map (X.ofRestrict h).base).obj V),
  AlgebraicGeometry.Scheme.Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

1 results in Mathlib

Foundations

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