Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.appLE

{X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (U : Y.Opens) →
      (V : X.Opens) →
        V ≤ (TopologicalSpace.Opens.map f.base).obj U →
          (Y.presheaf.obj (Opposite.op U) ⟶ X.presheaf.obj (Opposite.op V))

Given a morphism of schemes f : X ⟶ Y, and open sets U ⊆ Y, V ⊆ f ⁻¹' U, this is the induced map Γ(Y, U) ⟶ Γ(X, V). This is treated as a suffix in lemma names.

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

138 results in Mathlib

Foundations

Depth 100 from the axioms, rests on 1,349 definitions · uses propext, Classical.choice, Quot.sound