Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE

∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : Y.Opens) (W : X.Opens)
  (e₁ : V ≤ (TopologicalSpace.Opens.map g.base).obj U) (e₂ : W ≤ (TopologicalSpace.Opens.map f.base).obj V),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE g U V e₁)
      (AlgebraicGeometry.Scheme.Hom.appLE f V W e₂) =
    AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U W ⋯

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

15 results in Mathlib

Foundations

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