homOfLE_homOfLE — Mathlib

English

Composition of restriction maps equals the restriction map for the composed inclusion.

Русский

Состав ограничивающих отображений равен ограничивающему отображению для композиции вложений.

LaTeX

$$$ X.homOfLE e_1 ≫ X.homOfLE e_2 = X.homOfLE (e_1 \\text{ trans } e_2) $$$

Lean4

@[reassoc (attr := simp)]
theorem homOfLE_homOfLE (X : Scheme.{u}) {U V W : X.Opens} (e₁ : U ≤ V) (e₂ : V ≤ W) :
    X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE (e₁.trans e₂) := by
  rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]

Похожие утверждения