Spec_iff — Mathlib

English

Equality of P and affineLocally P expresses the same notion of locality via affine covers.

Русский

Равенство P и affineLocally P задаёт одно и то же локальное свойство через аффинные покрытия.

LaTeX

$$eq_affineLocally$$

Lean4

theorem Spec_iff {R S : CommRingCat.{u}} {φ : R ⟶ S} : P (Spec.map φ) ↔ Q φ.hom :=
  by
  have H := (isLocal_ringHomProperty P).respectsIso
  rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom, ← CommRingCat.hom_comp,
    Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]

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