Lean4
/-- The sheaf condition for the structure sheaf on `Spec R`
for a covering of the whole prime spectrum by basic opens. -/
theorem existsUnique_algebraMap_eq_of_span_eq_top (s : Set R) (span_eq : Ideal.span s = ⊤) (f : Π a : s, Away a.1)
(h : ∀ a b : s, Away.awayToAwayRight (P := Away (a * b : R)) a.1 b (f a) = Away.awayToAwayLeft b.1 a (f b)) :
∃! r : R, ∀ a : s, algebraMap R _ r = f a :=
by
have mem := (Ideal.eq_top_iff_one _).mp span_eq; clear span_eq
wlog finset_eq : ∃ t : Finset R, t = s generalizing s
· have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span mem
have ⟨r, eq, uniq⟩ := this t (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦ h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) mem ⟨_, rfl⟩
refine ⟨r, fun a ↦ ?_, fun _ eq ↦ uniq _ fun a ↦ eq ⟨a, hts a.2⟩⟩
replace hts := Set.insert_subset a.2 hts
classical
have ⟨r', eq, _⟩ :=
this ({ a.1 } ∪ t) (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦ h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩)
(Ideal.span_mono (fun _ ↦ .inr) mem) ⟨{ a.1 } ∪ t, by simp⟩
exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)
have span_eq := (Ideal.eq_top_iff_one _).mpr mem
refine
existsUnique_of_exists_of_unique ?_ fun x y hx hy ↦
algebraMap_injective_of_span_eq_top s span_eq (funext fun a ↦ (hx a).trans (hy a).symm)
obtain ⟨s, rfl⟩ := finset_eq
choose n r eq using fun a ↦ Away.surj a.1 (f a)
let N := s.attach.sup n
let r a := a ^ (N - n a) * r a
have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
rw [map_mul, ← eq, mul_left_comm, ← map_pow, ← map_mul, ← pow_add,
Nat.sub_add_cancel (Finset.le_sup <| s.mem_attach a)]
have eq2 a b : ∃ N', (a * b) ^ N' * (r a * b ^ N) = (a * b) ^ N' * (r b * a ^ N) :=
Away.exists_of_eq (S := Away (a * b : R)) _ <| by
simp_rw [map_mul, ← Away.awayToAwayRight_eq (S := Away a.1) a.1 b (r a), ←
Away.awayToAwayLeft_eq (S := Away b.1) b.1 a (r b), ← eq, map_mul, Away.awayToAwayRight_eq,
Away.awayToAwayLeft_eq, h, mul_assoc, ← map_mul, mul_comm]
choose N' hN' using eq2
let N' := (s ×ˢ s).attach.sup fun a ↦ N' ⟨_, (Finset.mem_product.mp a.2).1⟩ ⟨_, (Finset.mem_product.mp a.2).2⟩
have eq2 a b : (a * b) ^ N' * (r a * b ^ N) = (a * b) ^ N' * (r b * a ^ N) := by dsimp only [N'];
rw [← Nat.sub_add_cancel (Finset.le_sup <| (Finset.mem_attach _ ⟨⟨a, b⟩, Finset.mk_mem_product a.2 b.2⟩)), pow_add,
mul_assoc, hN', ← mul_assoc]
let N := N' + N
let r a := a ^ N' * r a
have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
rw [map_mul, ← eq, mul_left_comm, ← map_mul, ← pow_add]
have eq2 a b : r a * b ^ N = r b * a ^ N := by
rw [pow_add, mul_mul_mul_comm, ← mul_pow, eq2, mul_comm a.1, mul_pow, mul_mul_mul_comm, ← pow_add]
have ⟨c, eq1⟩ :=
(Submodule.mem_span_range_iff_exists_fun _).mp <|
(Ideal.eq_top_iff_one _).mp <| (Set.image_eq_range _ _ ▸ Ideal.span_pow_eq_top _ span_eq N)
refine ⟨∑ b, c b * r b, fun a ↦ ((Away.algebraMap_isUnit a.1).pow N).mul_left_inj.mp ?_⟩
simp_rw [← map_pow, eq, ← map_mul, Finset.sum_mul, mul_assoc, eq2 _ a, mul_left_comm (c _), ← Finset.mul_sum, ←
smul_eq_mul (a := c _), eq1, mul_one]
