English
Under qcqs, there exists a relation between powers of a section s and a section f against another section on restricted opens, mirroring the localization structure.
Русский
При qcqs существует связь степеней и умножения секций на ограниченных открытых, соответствующая локализации.
LaTeX
$$$$\\text{exists\_pow\_mul\_structure}$$$$
Lean4
theorem exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (X : Scheme) (S : X.affineOpens) (U₁ U₂ : X.Opens)
{n₁ n₂ : ℕ} {y₁ : Γ(X, U₁)} {y₂ : Γ(X, U₂)} {f : Γ(X, U₁ ⊔ U₂)} {x : Γ(X, X.basicOpen f)} (h₁ : S.1 ≤ U₁)
(h₂ : S.1 ≤ U₂) (e₁ : y₁ |_ X.basicOpen (f |_ U₁) = ((f |_ U₁ |_ X.basicOpen _) ^ n₁) * x |_ X.basicOpen _)
(e₂ : y₂ |_ X.basicOpen (f |_ U₂) = ((f |_ U₂ |_ X.basicOpen _) ^ n₂) * x |_ X.basicOpen _) :
∃ n : ℕ, ∀ m, n ≤ m → ((f |_ U₁) ^ (m + n₂) * y₁) |_ S.1 = ((f |_ U₂) ^ (m + n₁) * y₂) |_ S.1 :=
by
obtain ⟨⟨_, n, rfl⟩, e⟩ :=
(@IsLocalization.eq_iff_exists _ _ _ _ _ _ (S.2.isLocalization_basicOpen (f |_ S.1)) (((f |_ U₁) ^ n₂ * y₁) |_ S.1)
(((f |_ U₂) ^ n₁ * y₂) |_ S.1)).mp <|
by
apply exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux (e₁ := e₁) (e₂ := e₂)
· change X.basicOpen _ ≤ _
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]
exact inf_le_inf h₁ le_rfl
· change X.basicOpen _ ≤ _
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]
exact inf_le_inf h₂ le_rfl
use n
intro m hm
rw [← tsub_add_cancel_of_le hm]
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, pow_add, map_pow, map_mul, mul_assoc, ← Functor.map_comp,
← op_comp, homOfLE_comp, ← CommRingCat.comp_apply] at e ⊢
rw [e]
