English
The IsFraction predicate is stable under negation and multiplication, mirroring the algebraic structure of the local fractions.
Русский
Предикат IsFraction сохраняется при отрицании и умножении, соответствуя алгебраической структуре локальных дробей.
LaTeX
$$$$IsFraction(a) \to IsFraction(-a) \land IsFraction(a\cdot b)$$$$
Lean4
theorem mul_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, ⟨ra * rb, SetLike.mul_mem_graded ra_mem rb_mem⟩,
⟨sa * sb, SetLike.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, Localization.mk_mul]
