English
A repeated auxiliary construction within the qcqs framework to handle nested intersections and localizations.
Русский
Повторная вспомогательная конструкция в рамках qcqs для работы со вложенными пересечениями и локализацией.
LaTeX
$$$$\\text{auxiliary\_structure}$$$$
Lean4
theorem exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme.{u}) (U : X.Opens) (hU : IsCompact U.1)
(hU' : IsQuasiSeparated U.1) (f : Γ(X, U)) (x : Γ(X, X.basicOpen f)) :
∃ (n : ℕ) (y : Γ(X, U)), y |_ X.basicOpen f = (f |_ X.basicOpen f) ^ n * x :=
by
dsimp only [TopCat.Presheaf.restrictOpenCommRingCat_apply]
revert hU' f x
refine compact_open_induction_on U hU ?_ ?_
· intro _ f x
use 0, f
refine @Subsingleton.elim _ (CommRingCat.subsingleton_of_isTerminal (X.sheaf.isTerminalOfEqEmpty ?_)) _ _
rw [eq_bot_iff]
exact X.basicOpen_le f
· -- Given `f : 𝒪(S ∪ U), x : 𝒪(X_f)`, we need to show that `f ^ n * x` is the restriction of
-- some `y : 𝒪(S ∪ U)` for some `n : ℕ`.
intro S hS U hU hSU f x
obtain ⟨n₁, y₁, hy₁⟩ :=
hU (hSU.of_subset Set.subset_union_left) (X.presheaf.map (homOfLE le_sup_left).op f)
(X.presheaf.map (homOfLE _).op x)
-- · rw [X.basicOpen_res]; exact inf_le_right
-- We know that such `y₂, n₂` exists on `U` since `U` is affine.
obtain ⟨n₂, y₂, hy₂⟩ :=
exists_eq_pow_mul_of_isAffineOpen X _ U.2 (X.presheaf.map (homOfLE le_sup_right).op f)
(X.presheaf.map (homOfLE _).op x)
dsimp only [TopCat.Presheaf.restrictOpenCommRingCat_apply] at hy₂
obtain ⟨s, hs', hs⟩ :=
(isCompactOpen_iff_eq_finset_affine_union _).mp
⟨hSU _ _ Set.subset_union_left S.2 hS Set.subset_union_right U.1.2 U.2.isCompact, (S ⊓ U.1).2⟩
haveI := hs'.to_subtype
cases nonempty_fintype s
replace hs : S ⊓ U.1 = iSup fun i : s => (i : X.Opens) := by ext1; simpa using hs
have hs₁ (i : s) : i.1.1 ≤ S := by
refine le_trans ?_ (inf_le_left (b := U.1))
rw [hs]
exact le_iSup (fun (i : s) => (i : X.Opens)) i
have hs₂ (i : s) : i.1.1 ≤ U.1 := by
refine le_trans ?_ (inf_le_right (a := S))
rw [hs]
exact le_iSup (fun (i : s) => (i : X.Opens)) i
have := fun i ↦ exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux X i.1 S U (hs₁ i) (hs₂ i) hy₁ hy₂
choose n hn using this
have :
X.presheaf.map (homOfLE <| inf_le_left).op
(X.presheaf.map (homOfLE le_sup_left).op f ^ (Finset.univ.sup n + n₂) * y₁) =
X.presheaf.map (homOfLE <| inf_le_right).op
(X.presheaf.map (homOfLE le_sup_right).op f ^ (Finset.univ.sup n + n₁) * y₂) :=
by
fapply X.sheaf.eq_of_locally_eq' fun i : s => i.1.1
· refine fun i => homOfLE ?_; rw [hs]
exact le_iSup (fun (i : s) => (i : X.Opens)) i
· exact le_of_eq hs
· intro i
change (X.presheaf.map _) _ = (X.presheaf.map _) _
simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp]
apply hn
exact Finset.le_sup (Finset.mem_univ _)
use Finset.univ.sup n + n₁ + n₂
use (X.sheaf.objSupIsoProdEqLocus S U.1).inv ⟨⟨_ * _, _ * _⟩, this⟩
refine
(X.sheaf.objSupIsoProdEqLocus_inv_eq_iff _ _ _ (X.basicOpen_res _ (homOfLE le_sup_left).op)
(X.basicOpen_res _ (homOfLE le_sup_right).op)).mpr
⟨?_, ?_⟩
· -- This unfolds `X.sheaf`
change (X.presheaf.map _) _ = (X.presheaf.map _) _
rw [add_assoc, add_comm n₁]
simp only [pow_add, map_pow, map_mul, hy₁, ← CommRingCat.comp_apply, ← mul_assoc, ← Functor.map_comp, ← op_comp,
homOfLE_comp]
· -- This unfolds `X.sheaf`
change (X.presheaf.map _) _ = (X.presheaf.map _) _
simp only [pow_add, map_pow, map_mul, hy₂, ← CommRingCat.comp_apply, ← mul_assoc, ← Functor.map_comp, ← op_comp,
homOfLE_comp]
