English
One can normalize a finite collection of fractions representing a local section to ensure coherence relations among them on overlaps.
Русский
Можно нормализовать конечную совокупность дробей, представляющих локальную секцию, чтобы соблюдались соотношения на перекрытиях.
LaTeX
$$$\\exists a', h', iDh' \\text{ so that } a'_i h'_j = h'_i a'_j \\text{ on overlaps and } \\text{maps agree with s}$.$$
Lean4
theorem normalize_finite_fraction_representation (U : Opens (PrimeSpectrum.Top R)) (s : (structureSheaf R).1.obj (op U))
{ι : Type*} (t : Finset ι) (a h : ι → R) (iDh : ∀ i : ι, PrimeSpectrum.basicOpen (h i) ⟶ U)
(h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i))
(hs :
∀ i : ι,
(const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) fun _ hy => hy) = (structureSheaf R).1.map (iDh i).op s) :
∃ (a' h' : ι → R) (iDh' : ∀ i : ι, PrimeSpectrum.basicOpen (h' i) ⟶ U),
(U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i)) ∧
(∀ (i) (_ : i ∈ t) (j) (_ : j ∈ t), a' i * h' j = h' i * a' j) ∧
∀ i ∈ t,
(structureSheaf R).1.map (iDh' i).op s =
const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) fun _ hy => hy :=
by
-- First we show that the fractions `(a i * h j) / (h i * h j)` and `(h i * a j) / (h i * h j)`
-- coincide in the localization of `R` at `h i * h j`
have fractions_eq :
∀ i j : ι,
IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, Submonoid.mem_powers _⟩ =
IsLocalization.mk' _ (h i * a j) ⟨h i * h j, Submonoid.mem_powers _⟩ :=
by
intro i j
let D := PrimeSpectrum.basicOpen (h i * h j)
let iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE (PrimeSpectrum.basicOpen_mul_le_left _ _)
let iDj : D ⟶ PrimeSpectrum.basicOpen (h j) :=
homOfLE
(PrimeSpectrum.basicOpen_mul_le_right _ _)
-- Crucially, we need injectivity of `toBasicOpen`
apply toBasicOpen_injective R (h i * h j)
rw [toBasicOpen_mk', toBasicOpen_mk']
simp only []
-- Here, both sides of the equation are equal to a restriction of `s`
trans
on_goal 1 =>
convert congr_arg ((structureSheaf R).1.map iDj.op) (hs j).symm using 1
convert congr_arg ((structureSheaf R).1.map iDi.op) (hs i) using 1
all_goals rw [res_const]; apply const_ext;
ring
-- The remaining two goals were generated during the rewrite of `res_const`
-- These can be solved immediately
exacts [PrimeSpectrum.basicOpen_mul_le_left _ _, PrimeSpectrum.basicOpen_mul_le_right _ _]
-- From the equality in the localization, we obtain for each `(i,j)` some power `(h i * h j) ^ n`
-- which equalizes `a i * h j` and `h i * a j`
have exists_power : ∀ i j : ι, ∃ n : ℕ, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n :=
by
intro i j
obtain ⟨⟨c, n, rfl⟩, hc⟩ := IsLocalization.eq.mp (fractions_eq i j)
use n + 1
rw [pow_succ]
dsimp at hc
convert hc using 1 <;> ring
let n := fun p : ι × ι => (exists_power p.1 p.2).choose
have n_spec := fun p : ι × ι => (exists_power p.fst p.snd).choose_spec
let N := (t ×ˢ t).sup n
have basic_opens_eq : ∀ i : ι, PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i) := fun i =>
PrimeSpectrum.basicOpen_pow _ _
(by cutsat)
-- Expanding the fraction `a i / h i` by the power `(h i) ^ n` gives the desired normalization
refine ⟨fun i => a i * h i ^ N, fun i => h i ^ (N + 1), fun i => eqToHom (basic_opens_eq i) ≫ iDh i, ?_, ?_, ?_⟩
· simpa only [basic_opens_eq] using h_cover
· intro i hi j hj
have n_le_N : n (i, j) ≤ N := Finset.le_sup (Finset.mem_product.mpr ⟨hi, hj⟩)
obtain ⟨k, hk⟩ := Nat.le.dest n_le_N
simp only [← hk, pow_add, pow_one]
-- To accommodate for the difference `k`, we multiply both sides of the equation `n_spec (i, j)`
-- by `(h i * h j) ^ k`
convert congr_arg (fun z => z * (h i * h j) ^ k) (n_spec (i, j)) using 1 <;>
· simp only [n, mul_pow];
ring
-- Lastly, we need to show that the new fractions still represent our original `s`
intro i _
rw [op_comp, Functor.map_comp, ConcreteCategory.comp_apply, ← hs, res_const]
-- additional goal spit out by `res_const`
swap
· exact (basic_opens_eq i).le
apply const_ext
dsimp
rw [pow_succ]
ring
-- The proof here follows the argument in Hartshorne's Algebraic Geometry, Proposition II.2.2.
