English
The map toSpec 𝒜 f is bijective for the given data 𝒜, f, hm.
Русский
Соотношение toSpec 𝒜 f биективно для данных 𝒜, f, hm.
LaTeX
$$$toSpec(𝒜,f) \text{ is bijective for } f \text{ with degree } m \text{ (}hm>0\text{)}$$$
Lean4
/-- The continuous function `Spec A⁰_f → Proj|D(f)` sending `q` to `{a | aᵢᵐ/fⁱ ∈ q}` where
`m` is the degree of `f` -/
def fromSpec {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : (Spec.T (A⁰_ f)) ⟶ (Proj.T| (pbo f)) :=
TopCat.ofHom
{ toFun := FromSpec.toFun f_deg hm
continuous_toFun :=
by
rw [isTopologicalBasis_subtype (ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜)
(pbo f).1 |>.continuous_iff]
rintro s ⟨_, ⟨a, rfl⟩, rfl⟩
have h₁ :
Subtype.val (p := (pbo f).1) ⁻¹' (pbo a) =
⋃ i : ℕ, Subtype.val (p := (pbo f).1) ⁻¹' (pbo (decompose 𝒜 a i)) :=
by simp [ProjectiveSpectrum.basicOpen_eq_union_of_projection 𝒜 a]
let e : _ ≃ _ := ⟨FromSpec.toFun f_deg hm, ToSpec.toFun f, toSpec_fromSpec _ _ _, fromSpec_toSpec _ _ _⟩
change IsOpen <| e ⁻¹' _
rw [Set.preimage_equiv_eq_image_symm, h₁, Set.image_iUnion]
exact isOpen_iUnion fun i ↦ toSpec.image_basicOpen_eq_basicOpen f_deg hm a i ▸ PrimeSpectrum.isOpen_basicOpen }
