objSupIsoProdEqLocus — Mathlib

English

The value of a sheaf on a supremum open is isomorphic to an equality-locus of two pullback maps from the product over U and V to the intersection.

Русский

Значение на объединении объёмов из верхнего предела изоморфно через множество точек равенств двух отображений, получаемых через произведение на пересечение.

LaTeX

$$$F(U \\sqcup V) \\cong \\mathrm{eqLocus}(\\text{fst}, \\text{snd})$$$

Lean4

/-- `F(U ⊔ V)` is isomorphic to the `eq_locus` of the two maps `F(U) × F(V) ⟶ F(U ⊓ V)`. -/
def objSupIsoProdEqLocus {X : TopCat} (F : X.Sheaf CommRingCat) (U V : Opens X) :
    F.1.obj (op <| U ⊔ V) ≅
      CommRingCat.of <|
        -- Porting note: Lean 3 is able to figure out the ring homomorphism automatically
        RingHom.eqLocus
          (RingHom.comp (F.val.map (homOfLE inf_le_left : U ⊓ V ⟶ U).op).hom
            (RingHom.fst (F.val.obj <| op U) (F.val.obj <| op V)))
          (RingHom.comp (F.val.map (homOfLE inf_le_right : U ⊓ V ⟶ V).op).hom
            (RingHom.snd (F.val.obj <| op U) (F.val.obj <| op V))) :=
  (F.isLimitPullbackCone U V).conePointUniqueUpToIso (CommRingCat.pullbackConeIsLimit _ _)

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