Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.map_fromSpec

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

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

2 results in Mathlib

Foundations

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