English
The map toSpec 𝒜 f is injective for f_deg, hm.
Русский
toSpec 𝒜 f инъективно при f_deg, hm.
LaTeX
$$$toSpec(𝒜,f) \text{ is injective for } f_deg, hm>0$$$
Lean4
/-- The ring map from `A⁰_ f` to the local sections of the structure sheaf of the projective spectrum of
`A` on the basic open set `D(f)` defined by sending `s ∈ A⁰_f` to the section `x ↦ s` on `D(f)`.
-/
def awayToSection (f) : CommRingCat.of (A⁰_ f) ⟶ (structureSheaf 𝒜).1.obj (op (pbo f)) :=
CommRingCat.ofHom (S := (structureSheaf 𝒜).1.obj (op (pbo f)))
{ toFun
s :=
⟨fun x ↦ HomogeneousLocalization.mapId 𝒜 (Submonoid.powers_le.mpr x.2) s, fun x ↦
by
obtain ⟨s, rfl⟩ := HomogeneousLocalization.mk_surjective s
obtain ⟨n, hn : f ^ n = s.den.1⟩ := s.den_mem
exact
⟨_, x.2, 𝟙 _, s.1, s.2, s.3, fun x hsx ↦ x.2 (Ideal.IsPrime.mem_of_pow_mem inferInstance n (hn ▸ hsx)),
fun _ ↦ rfl⟩⟩
map_add' _ _ := by ext; simp only [map_add, HomogeneousLocalization.val_add, «Proj».add_apply]
map_mul' _ _ := by ext; simp only [map_mul, HomogeneousLocalization.val_mul, «Proj».mul_apply]
map_zero' := by ext; simp only [map_zero, HomogeneousLocalization.val_zero, «Proj».zero_apply]
map_one' := by ext; simp only [map_one, HomogeneousLocalization.val_one, «Proj».one_apply] }
