AlgebraicGeometry.Scheme.comp_val_base

theorem AlgebraicGeometry.Scheme.comp_val_base : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).val.base = CategoryTheory.CategoryStruct.comp f.val.base g.val.base

The theorem `AlgebraicGeometry.Scheme.comp_val_base` states that for any three schemes `X`, `Y`, and `Z` in algebraic geometry, and any two morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the base of the value of the composition of `f` and `g` (expressed as `(CategoryTheory.CategoryStruct.comp f g).val.base`) is equal to the composition of the bases of the values of `f` and `g` (expressed as `CategoryTheory.CategoryStruct.comp f.val.base g.val.base`). In essence, this theorem ensures that the process of composition in the category of schemes respects the underlying structure of the schemes.

More concisely: The base of the composition of two morphisms in the category of schemes is equal to the composition of their bases.