iso_hom_base_inv_base — Mathlib

English

An equality of opens induces a compatible equality on Spec maps via eqToHom; the open-level map respects equality of the domain opens.

Русский

Равенство открытых подмножеств порождает согласованное равенство отображений на Spеc через eqToHom; карта открытий сохраняет равенство областей.

LaTeX

$$$(\mathrm{Spec}.map (X.presheaf.map (\mathrm{CategoryTheory.eqToHom} h).op)).app W = \mathrm{eqToHom}(...)$$$

Lean4

@[reassoc (attr := simp)]
theorem iso_hom_base_inv_base {X Y : Scheme.{u}} (e : X ≅ Y) : e.hom.base ≫ e.inv.base = 𝟙 _ :=
  LocallyRingedSpace.iso_hom_base_inv_base (Scheme.forgetToLocallyRingedSpace.mapIso e)

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