homOfLE_rfl — Mathlib

English

For any scheme X and open U, homOfLE on the reflexive inclusion equals the identity morphism.

Русский

Для схемы X и открытого U отображение homOfLE на рефлексивном включении равно тождественному морфизму.

LaTeX

$$$ X.homOfLE(\\mathrm{refl}\\ U) = \\mathrm{Id} $$$

Lean4

@[simp]
theorem homOfLE_rfl (X : Scheme.{u}) (U : X.Opens) : X.homOfLE (refl U) = 𝟙 _ := by
  rw [← cancel_mono U.ι, Scheme.homOfLE_ι, Category.id_comp]

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