Lean4
/-- For any `R`-module `M` and any open subset `U ⊆ Spec R`, `M^~(U)` is an `𝒪_{Spec R}(U)`-submodule
of `∏_{𝔭 ∈ U} M_𝔭`. -/
noncomputable def sectionsSubmodule (U : (Opens (PrimeSpectrum R))ᵒᵖ) :
Submodule ((Spec.structureSheaf R).1.obj U) (∀ x : U.unop, Localizations M x.1)
where
carrier := {f | (isLocallyFraction M).pred f}
zero_mem' x := ⟨unop U, x.2, 𝟙 _, 0, 1, fun y => ⟨Ideal.ne_top_iff_one _ |>.1 y.1.isPrime.1, by 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, sb • ra + sa • rb, sa * sb, ?_⟩
intro y
rcases wa (Opens.infLELeft _ _ y : Va) with ⟨nma, wa⟩
rcases wb (Opens.infLERight _ _ y : Vb) with ⟨nmb, wb⟩
fconstructor
· intro H; cases y.1.isPrime.mem_or_mem H <;> contradiction
· simp only [LocalizedModule.mkLinearMap_apply, Opens.comp_apply, Pi.add_apply, smul_add, map_add,
map_smul] at wa wb ⊢
rw [← wa, ← wb, ← mul_smul, ← mul_smul]
congr 2
simp [mul_comm]
smul_mem' := by
intro r a ha x
rcases ha x with ⟨Va, ma, ia, ra, sa, wa⟩
rcases r.2 x with ⟨Vr, mr, ir, rr, sr, wr⟩
refine ⟨Va ⊓ Vr, ⟨ma, mr⟩, Opens.infLELeft _ _ ≫ ia, rr • ra, sr * sa, ?_⟩
intro y
rcases wa (Opens.infLELeft _ _ y : Va) with ⟨nma, wa⟩
rcases wr (Opens.infLERight _ _ y) with ⟨nmr, wr⟩
fconstructor
· intro H; cases y.1.isPrime.mem_or_mem H <;> contradiction
· simp only [Pi.smul_apply, LinearMapClass.map_smul, Opens.apply_def] at wa wr ⊢
rw [mul_comm, ← Algebra.smul_def] at wr
rw [sections_smul_localizations_def, ← wa, ← mul_smul, ← smul_assoc, mul_comm sr, mul_smul, wr, mul_comm rr,
Algebra.smul_def, ← map_mul]
rfl
