isLocalization_of_eq_basicOpen — Mathlib

English

More general version: for V ⟶ U with V = X.basicOpen f, IsLocalization.Away f (X.presheaf.obj{ unop := V }).carrier.

Русский

Общая версия: если V ⟶ U и V = X.basicOpen f, тогда IsLocalization.Away f ...

LaTeX

$$$IsLocalization.Away f (X.presheaf.obj{ unop := V }).carrier$$$

Lean4

theorem isLocalization_of_eq_basicOpen {V : X.Opens} (i : V ⟶ U) (e : V = X.basicOpen f) :
    @IsLocalization.Away _ _ f Γ(X, V) _ (X.presheaf.map i.op).hom.toAlgebra := by subst e;
  convert isLocalization_basicOpen hU f using 3

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