mem_carrier_iff_of_mem_mul — Mathlib

English

Continuous map from Proj mais ToSpec is defined, respecting primeness and the topological structure of basic opens.

Русский

Постоянный переход From Proj к Spec с сохранением простоты и топологии базовых открытых.

LaTeX

$$$\text{toSpec}$ is continuous$$

Lean4

theorem mem_carrier_iff_of_mem_mul (hm : 0 < m) (q : Spec.T A⁰_ f) (a : A) {n} (hn : a ∈ 𝒜 (n * m)) :
    a ∈ carrier f_deg q ↔
      (HomogeneousLocalization.mk ⟨m * n, ⟨a, mul_comm n m ▸ hn⟩, ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ :
          A⁰_ f) ∈
        q.asIdeal :=
  by
  rw [mem_carrier_iff_of_mem f_deg hm q a hn, iff_iff_eq, eq_comm, ←
    Ideal.IsPrime.pow_mem_iff_mem (α := A⁰_ f) inferInstance m hm]
  congr 1
  apply HomogeneousLocalization.val_injective
  simp only [HomogeneousLocalization.val_mk, HomogeneousLocalization.val_pow, Localization.mk_pow, pow_mul]
  rfl

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