Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc

∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U) {Z_1 : CommRingCat}
  (h : X.presheaf.obj (Opposite.op V) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U V e)
      h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e) h)

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

0 results in Mathlib

Foundations

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