appIso_inv_appLE — Mathlib

English

For opens U ⊆ Y and V ⊆ X with a subset e, the equality holds between f.appLE U V e ≫ (f.appIso V).inv and a presheaf map; i.e. the composite equals X.presheaf.map (homOfLE ...).op.

Русский

Для открытых U ⊆ Y и V ⊆ X и включения-e выполнено равенство между f.appLE U V e затем inv и отображением прешефа.

LaTeX

$$$$ f.appLE U V e \;\; ≫ (f.appIso V).inv = X.presheaf.map(homOfLE(\dots)).op $$$$

Lean4

@[reassoc (attr := simp)]
theorem appIso_inv_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] {U V : X.Opens} (e : V ≤ f ⁻¹ᵁ f ''ᵁ U) :
    (f.appIso U).inv ≫ f.appLE (f ''ᵁ U) V e = X.presheaf.map (homOfLE (by rwa [preimage_image_eq] at e)).op :=
  by
  simp only [appLE, appIso_inv_app_assoc, eqToHom_op]
  rw [← Functor.map_comp]
  rfl

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