English
Characterizes when an inverse image under the isomorphism corresponds to equality of its components in the product diagram.
Русский
Характеризуется, когда образ обратной под изоморфизма соответствует равенству его компонент в произведении.
LaTeX
$$$\\text{eq} \\Leftrightarrow (\\text{fst eq}, \\text{snd eq})$$$
Lean4
theorem objSupIsoProdEqLocus_inv_eq_iff {X : TopCat.{u}} (F : X.Sheaf CommRingCat.{u}) {U V W UW VW : Opens X}
(e : W ≤ U ⊔ V) (x) (y : F.1.obj (op W)) (h₁ : UW = U ⊓ W) (h₂ : VW = V ⊓ W) :
F.1.map (homOfLE e).op ((F.objSupIsoProdEqLocus U V).inv x) = y ↔
F.1.map (homOfLE (h₁ ▸ inf_le_left : UW ≤ U)).op x.1.1 = F.1.map (homOfLE <| h₁ ▸ inf_le_right).op y ∧
F.1.map (homOfLE (h₂ ▸ inf_le_left : VW ≤ V)).op x.1.2 = F.1.map (homOfLE <| h₂ ▸ inf_le_right).op y :=
by
subst h₁ h₂
constructor
· rintro rfl
rw [← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]
simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp, homOfLE_comp, and_self]
· rintro ⟨e₁, e₂⟩
refine F.eq_of_locally_eq₂ (homOfLE (inf_le_right : U ⊓ W ≤ W)) (homOfLE (inf_le_right : V ⊓ W ≤ W)) ?_ _ _ ?_ ?_
· rw [← inf_sup_right]
exact le_inf e le_rfl
· rw [← e₁, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst]
simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp, homOfLE_comp]
· rw [← e₂, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]
simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp, homOfLE_comp]
