Documentation

Mathlib.CategoryTheory.Category.Pairwise

The category of "pairwise intersections". #

Given ι : Type v, we build the diagram category Pairwise ι with objects single i and pair i j, for i j : ι, whose only non-identity morphisms are left : pair i j ⟶ single i and right : pair i j ⟶ single j.

We use this later in describing (one formulation of) the sheaf condition.

Given any function U : ι → α, where α is some complete lattice (e.g. (opens X)ᵒᵖ), we produce a functor Pairwise ι ⥤ α in the obvious way, and show that iSup U provides a colimit cocone over this functor.

inductive CategoryTheory.Pairwise (ι : Type v) :

An inductive type representing either a single term of a type ι, or a pair of terms. We use this as the objects of a category to describe the sheaf condition.

Instances For
    Equations

    Morphisms in the category Pairwise ι. The only non-identity morphisms are left i j : single i ⟶ pair i j and right i j : single j ⟶ pair i j.

    Instances For
      Equations
      def CategoryTheory.Pairwise.comp {ι : Type v} {o₁ : CategoryTheory.Pairwise ι} {o₂ : CategoryTheory.Pairwise ι} {o₃ : CategoryTheory.Pairwise ι} :
      o₁.Hom o₂o₂.Hom o₃o₁.Hom o₃

      Composition of morphisms in Pairwise ι.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        A helper tactic for aesop_cat and Pairwise.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          def CategoryTheory.Pairwise.diagramObj {ι : Type v} {α : Type v} (U : ια) [SemilatticeInf α] :

          Auxiliary definition for diagram.

          Equations
          Instances For

            Auxiliary definition for diagram.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Given a function U : ι → α for [SemilatticeInf α], we obtain a functor Pairwise ι ⥤ α, sending single i to U i and pair i j to U i ⊓ U j, and the morphisms to the obvious inequalities.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Auxiliary definition for cocone.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Pairwise.cocone_pt {ι : Type v} {α : Type v} (U : ια) [CompleteLattice α] :

                  Given a function U : ι → α for [CompleteLattice α], iSup U provides a cocone over diagram U.

                  Equations
                  Instances For

                    Given a function U : ι → α for [CompleteLattice α], iInf U provides a limit cone over diagram U.

                    Equations
                    Instances For