Lean4
/-- The functions satisfying `isLocallyFraction` form a subring.
-/
def sectionsSubring (U : (Opens (PrimeSpectrum.Top R))ᵒᵖ) : Subring (∀ x : U.unop, Localizations R x)
where
carrier := {f | (isLocallyFraction R).pred f}
zero_mem' := by
refine fun x => ⟨unop U, x.2, 𝟙 _, 0, 1, fun y => ⟨?_, ?_⟩⟩
· rw [← Ideal.ne_top_iff_one]; exact y.1.isPrime.1
· simp
one_mem' := by
refine fun x => ⟨unop U, x.2, 𝟙 _, 1, 1, fun y => ⟨?_, ?_⟩⟩
· rw [← Ideal.ne_top_iff_one]; exact y.1.isPrime.1
· simp
add_mem' := by
intro a b ha hb x
rcases ha x with ⟨Va, ma, ia, ra, sa, wa⟩
rcases hb x with ⟨Vb, mb, ib, rb, sb, wb⟩
refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ra * sb + rb * sa, sa * sb, ?_⟩
intro ⟨y, hy⟩
rcases wa (Opens.infLELeft _ _ ⟨y, hy⟩) with ⟨nma, wa⟩
rcases wb (Opens.infLERight _ _ ⟨y, hy⟩) with ⟨nmb, wb⟩
fconstructor
· intro H; cases y.isPrime.mem_or_mem H <;> contradiction
· simp only [Opens.apply_mk, Pi.add_apply, RingHom.map_mul, add_mul, RingHom.map_add] at wa wb ⊢
grind
neg_mem' := by
intro a ha x
rcases ha x with ⟨V, m, i, r, s, w⟩
refine ⟨V, m, i, -r, s, ?_⟩
intro y
rcases w y with ⟨nm, w⟩
fconstructor
· exact nm
· simp only [RingHom.map_neg, Pi.neg_apply]
rw [← w]
simp only [neg_mul]
mul_mem' := by
intro a b ha hb x
rcases ha x with ⟨Va, ma, ia, ra, sa, wa⟩
rcases hb x with ⟨Vb, mb, ib, rb, sb, wb⟩
refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ra * rb, sa * sb, ?_⟩
intro ⟨y, hy⟩
rcases wa (Opens.infLELeft _ _ ⟨y, hy⟩) with ⟨nma, wa⟩
rcases wb (Opens.infLERight _ _ ⟨y, hy⟩) with ⟨nmb, wb⟩
fconstructor
· intro H; cases y.isPrime.mem_or_mem H <;> contradiction
· simp only [Opens.apply_mk, Pi.mul_apply, RingHom.map_mul] at wa wb ⊢
rw [← wa, ← wb]
simp only [mul_left_comm, mul_assoc, mul_comm]
