Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.appTop

{X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → (Y.presheaf.obj (Opposite.op ⊤) ⟶ X.presheaf.obj (Opposite.op ⊤))

Given a morphism of schemes f : X ⟶ Y, this is the induced map Γ(Y, ⊤) ⟶ Γ(X, ⊤). This is treated as a suffix in lemma names.

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

109 results in Mathlib

Foundations

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