English
The appLE of the composition equals the composition of appLE maps with a transported e: g.appLE U V e1 ≫ f.appLE V W e2 = (f ≫ g).appLE U W (e2.trans ((Opens.map f.base).map (homOfLE e1)).le).
Русский
APPLE композиции равен композиции APPLE с переносом e черезех: g.appLE U V e1 ≫ f.appLE V W e2 = (f ≫ g).appLE U W (e2.trans ((Opens.map f.base).map (homOfLE e1)).le).
LaTeX
$$$g.appLE U V e_1 \\; \\gg \\; f.appLE V W e_2 = (f \\gg g).appLE U W \\big(e_2.\\mathrm{trans}((\\mathrm{Opens.map} f.base).map(\\mathrm{homOfLE} e_1)).\\mathrm{le}\\big)$$$
Lean4
theorem appLE_comp_appLE {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U V W e₁ e₂) :
g.appLE U V e₁ ≫ f.appLE V W e₂ = (f ≫ g).appLE U W (e₂.trans ((Opens.map f.base).map (homOfLE e₁)).le) :=
by
dsimp [Hom.appLE]
rw [Category.assoc, f.naturality_assoc, ← Functor.map_comp]
rfl
