Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.coprodPresheafObjIso

{X Y : AlgebraicGeometry.Scheme} →
  (U : (X ⨿ Y).Opens) →
    (X ⨿ Y).presheaf.obj (Opposite.op U) ≅
      X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U)) ⨯
        Y.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U))

The sections on coproducts of schemes are the (categorical) product of the sections on the components

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

5 results in Mathlib

Foundations

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