Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc

∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens}
  (hV : AlgebraicGeometry.IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) {Z : AlgebraicGeometry.Scheme}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map f))
      (CategoryTheory.CategoryStruct.comp hU.fromSpec h) =
    CategoryTheory.CategoryStruct.comp hV.fromSpec h

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

0 results in Mathlib

Foundations

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