Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc

∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] [inst_1 : AlgebraicGeometry.IsAffine Y]
  (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f))
      (CategoryTheory.CategoryStruct.comp Y.isoSpec.inv h) =
    CategoryTheory.CategoryStruct.comp X.isoSpec.inv (CategoryTheory.CategoryStruct.comp f h)

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

2 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsAffineAlgebraicGeometry.IsAffine