English
Negation is closed in the locally fractional section; the negative of a locally fractional section is locally fractional as well.
Русский
Отрицание сохраняется в локально дробной части; отрицание локально дробной секции тоже локально дробно.
LaTeX
$$$$(-a) \in \text{sectionsSubring}(U) \text{ if } a \in \text{sectionsSubring}(U)$$$$
Lean4
theorem add_mem' (U : (Opens (ProjectiveSpectrum.top 𝒜))ᵒᵖ) (a b : ∀ x : U.unop, at x.1)
(ha : (isLocallyFraction 𝒜).pred a) (hb : (isLocallyFraction 𝒜).pred b) : (isLocallyFraction 𝒜).pred (a + b) :=
fun x => by
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩
rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, hwb, wb⟩
refine
⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb,
⟨sb * ra + sa * rb,
add_mem (add_comm jb ja ▸ mul_mem_graded sb_mem ra_mem : sb * ra ∈ 𝒜 (ja + jb)) (mul_mem_graded sa_mem rb_mem)⟩,
⟨sa * sb, mul_mem_graded sa_mem sb_mem⟩, fun y ↦
y.1.asHomogeneousIdeal.toIdeal.primeCompl.mul_mem (hwa ⟨y.1, y.2.1⟩) (hwb ⟨y.1, y.2.2⟩), ?_⟩
rintro ⟨y, hy⟩
simp only [Subtype.forall, Opens.apply_mk] at wa wb
simp [wa y hy.1, wb y hy.2, ext_iff_val, add_mk, add_comm (sa * rb)]
