Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app

∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : (TopologicalSpace.Opens ↥X)ᵒᵖ),
  (AlgebraicGeometry.Scheme.Hom.toLRSHom (X.ofRestrict h)).c.app V =
    X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

0 results in Mathlib

Foundations

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