Theorems · Theorem · algebraic geometry

TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff

∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X) {U V W UW VW : TopologicalSpace.Opens ↑X} (e : W ≤ U ⊔ V)
  (x :
    ↑(CommRingCat.of
        ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus
            ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
              (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))))))
  (y : ↑(F.obj.obj (Opposite.op W))) (h₁ : UW = U ⊓ W) (h₂ : VW = V ⊓ W),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE e).op))
        ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) =
      y ↔
    (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) (↑x).1 =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) y ∧
      (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) (↑x).2 =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) y

Defined in

Mathlib.Topology.Sheaves.CommRingCat

Cited by

1 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound