objSupIsoProdEqLocus_hom_snd — Mathlib

English

There is a canonical isomorphism between the value on the supremum and the corresponding equality-locus representation.

Русский

Существует каноническое изоморфизм между значением на верхнем пределе и представлением через локус равенства.

LaTeX

$$$\\mathrm{Iso}(F(U \\sqcup V), \\operatorname{of}(\\text{locus}))$$$

Lean4

theorem objSupIsoProdEqLocus_hom_snd {X : TopCat} (F : X.Sheaf CommRingCat) (U V : Opens X) (x) :
    ((F.objSupIsoProdEqLocus U V).hom x).1.snd = F.1.map (homOfLE le_sup_right).op x :=
  ConcreteCategory.congr_hom
    ((F.isLimitPullbackCone U V).conePointUniqueUpToIso_hom_comp (CommRingCat.pullbackConeIsLimit _ _)
      WalkingCospan.right)
    x

Похожие утверждения