Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.app

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

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

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

176 results in Mathlib

Foundations

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