English
A technical lemma (auxiliary) that provides a constructive way to realize certain relations between powers of f and elements y on nested opens, under qcqs hypotheses.
Русский
Техническое вспомогательное лемма, строящее отношение между степенями f и элементами y на вложенных открытых, при предположениях qcqs.
LaTeX
$$$$\\text{(auxiliary construction)}$$$$
Lean4
theorem exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux {X : TopCat} (F : X.Presheaf CommRingCat)
{U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens X} {n₁ n₂ : ℕ} {y₁ : F.obj (op U₁)} {y₂ : F.obj (op U₂)} {f : F.obj (op <| U₁ ⊔ U₂)}
{x : F.obj (op U₃)} (h₄₁ : U₄ ≤ U₁) (h₄₂ : U₄ ≤ U₂) (h₅₁ : U₅ ≤ U₁) (h₅₃ : U₅ ≤ U₃) (h₆₂ : U₆ ≤ U₂) (h₆₃ : U₆ ≤ U₃)
(h₇₄ : U₇ ≤ U₄) (h₇₅ : U₇ ≤ U₅) (h₇₆ : U₇ ≤ U₆) (e₁ : y₁ |_ U₅ = (f |_ U₁ |_ U₅) ^ n₁ * x |_ U₅)
(e₂ : y₂ |_ U₆ = (f |_ U₂ |_ U₆) ^ n₂ * x |_ U₆) :
(((f |_ U₁) ^ n₂ * y₁) |_ U₄) |_ U₇ = (((f |_ U₂) ^ n₁ * y₂) |_ U₄) |_ U₇ :=
by
apply_fun (fun x : F.obj (op U₅) ↦ x |_ U₇) at e₁
apply_fun (fun x : F.obj (op U₆) ↦ x |_ U₇) at e₂
dsimp only [TopCat.Presheaf.restrictOpenCommRingCat_apply] at e₁ e₂ ⊢
simp only [map_mul, map_pow, ← op_comp, ← F.map_comp, homOfLE_comp, ← CommRingCat.comp_apply] at e₁ e₂ ⊢
rw [e₁, e₂, mul_left_comm]
