Documentation

Poly.Bifunctor.Sigma

Dependent sums of functors #

source
def CategoryTheory.Functor.Sigma {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F : Functor π’ž (Type w)} (G : Functor F.Elements (Functor π’Ÿ (Type v))) :
Functor π’ž (Functor π’Ÿ (Type (max w v)))

Given functors F : π’ž β₯€ Type v and G : ∫F β₯€ π’Ÿ β₯€ Type v, produce the functor (C, D) ↦ (a : F(C)) Γ— G((C, a))(D).

This is a dependent sum that varies naturally in a parameter C of the first component, and a parameter D of the second component.

We use this to package and compose natural equivalences where one side (or both) is a dependent sum, e.g.

H(C) ⟢ I(D)
=========================
(a : F(C)) Γ— (G(C, a)(D))

is a natural isomorphism of bifunctors π’žα΅’α΅– β₯€ π’Ÿ β₯€ Type v given by (C, D) ↦ H(C) ⟢ I(D) and G.Sigma.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.Sigma_map_app_fst {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F : Functor π’ž (Type w)} (G : Functor F.Elements (Functor π’Ÿ (Type v))) {X✝ Y✝ : π’ž} (f : X✝ ⟢ Y✝) (Y : π’Ÿ) (a✝ : { obj := fun (x : π’ž Γ— π’Ÿ) => match x with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D, map := fun {X Y : π’ž Γ— π’Ÿ} (x : X ⟢ Y) (x_1 : match X with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D) => match x with | (f, g) => match x_1 with | ⟨a, b⟩ => ⟨F.map f a, (G.map ⟨f, β‹―βŸ©).app Y.2 ((G.obj ⟨X.1, a⟩).map g b)⟩, map_id := β‹―, map_comp := β‹― }.obj (X✝, Y)) :
    (((Sigma G).map f).app Y a✝).fst = F.map f a✝.fst
    source
    @[simp]
    theorem CategoryTheory.Functor.Sigma_obj_map_snd {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F : Functor π’ž (Type w)} (G : Functor F.Elements (Functor π’Ÿ (Type v))) (X : π’ž) {X✝ Y✝ : π’Ÿ} (g : X✝ ⟢ Y✝) (a✝ : { obj := fun (x : π’ž Γ— π’Ÿ) => match x with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D, map := fun {X Y : π’ž Γ— π’Ÿ} (x : X ⟢ Y) (x_1 : match X with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D) => match x with | (f, g) => match x_1 with | ⟨a, b⟩ => ⟨F.map f a, (G.map ⟨f, β‹―βŸ©).app Y.2 ((G.obj ⟨X.1, a⟩).map g b)⟩, map_id := β‹―, map_comp := β‹― }.obj (X, X✝)) :
    (((Sigma G).obj X).map g a✝).snd = (G.map ⟨CategoryStruct.id X, β‹―βŸ©).app Y✝ ((G.obj ⟨X, a✝.fst⟩).map g a✝.snd)
    source
    @[simp]
    theorem CategoryTheory.Functor.Sigma_map_app_snd {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F : Functor π’ž (Type w)} (G : Functor F.Elements (Functor π’Ÿ (Type v))) {X✝ Y✝ : π’ž} (f : X✝ ⟢ Y✝) (Y : π’Ÿ) (a✝ : { obj := fun (x : π’ž Γ— π’Ÿ) => match x with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D, map := fun {X Y : π’ž Γ— π’Ÿ} (x : X ⟢ Y) (x_1 : match X with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D) => match x with | (f, g) => match x_1 with | ⟨a, b⟩ => ⟨F.map f a, (G.map ⟨f, β‹―βŸ©).app Y.2 ((G.obj ⟨X.1, a⟩).map g b)⟩, map_id := β‹―, map_comp := β‹― }.obj (X✝, Y)) :
    (((Sigma G).map f).app Y a✝).snd = (G.map ⟨f, β‹―βŸ©).app Y a✝.snd
    source
    @[simp]
    theorem CategoryTheory.Functor.Sigma_obj_obj {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F : Functor π’ž (Type w)} (G : Functor F.Elements (Functor π’Ÿ (Type v))) (X : π’ž) (Y : π’Ÿ) :
    ((Sigma G).obj X).obj Y = ((a : F.obj X) Γ— (G.obj ⟨X, a⟩).obj Y)
    source
    @[simp]
    theorem CategoryTheory.Functor.Sigma_obj_map_fst {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F : Functor π’ž (Type w)} (G : Functor F.Elements (Functor π’Ÿ (Type v))) (X : π’ž) {X✝ Y✝ : π’Ÿ} (g : X✝ ⟢ Y✝) (a✝ : { obj := fun (x : π’ž Γ— π’Ÿ) => match x with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D, map := fun {X Y : π’ž Γ— π’Ÿ} (x : X ⟢ Y) (x_1 : match X with | (C, D) => (a : F.obj C) Γ— (G.obj ⟨C, a⟩).obj D) => match x with | (f, g) => match x_1 with | ⟨a, b⟩ => ⟨F.map f a, (G.map ⟨f, β‹―βŸ©).app Y.2 ((G.obj ⟨X.1, a⟩).map g b)⟩, map_id := β‹―, map_comp := β‹― }.obj (X, X✝)) :
    (((Sigma G).obj X).map g a✝).fst = a✝.fst
    source
    def CategoryTheory.Functor.Sigma.isoCongrLeft {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F₁ Fβ‚‚ : Functor π’ž (Type w)} (G : Functor F₁.Elements (Functor π’Ÿ (Type v))) (i : Fβ‚‚ β‰… F₁) :
    Sigma ((NatTrans.mapElements i.hom).comp G) β‰… Sigma G
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.Functor.Sigma.isoCongrRight {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {F : Functor π’ž (Type w)} {G₁ Gβ‚‚ : Functor F.Elements (Functor π’Ÿ (Type v))} (i : G₁ β‰… Gβ‚‚) :
      Sigma G₁ β‰… Sigma Gβ‚‚
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CategoryTheory.Functor.compβ‚‚_Sigma {π’ž : Type t} [Category.{u, t} π’ž] {π’Ÿ : Type r} [Category.{s, r} π’Ÿ] {π’Ÿ' : Type u_1} [Category.{u_2, u_1} π’Ÿ'] {F : Functor π’ž (Type w)} (G : Functor π’Ÿ' π’Ÿ) (P : Functor F.Elements (Functor π’Ÿ (Type v))) :
        G.compβ‚‚ (Sigma P) = Sigma (G.compβ‚‚ P)

        Over categories #

        source
        def CategoryTheory.Over.equiv_Sigma {π’ž : Type u} [Category.{v, u} π’ž] {A : π’ž} (X : π’ž) (U : Over A) :
        (X ⟢ U.left) ≃ (b : X ⟢ A) Γ— (mk b ⟢ U)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Over.equiv_Sigma_apply_snd {π’ž : Type u} [Category.{v, u} π’ž] {A : π’ž} (X : π’ž) (U : Over A) (g : X ⟢ U.left) :
          ((equiv_Sigma X U) g).snd = homMk g β‹―
          source
          @[simp]
          theorem CategoryTheory.Over.equiv_Sigma_symm_apply {π’ž : Type u} [Category.{v, u} π’ž] {A : π’ž} (X : π’ž) (U : Over A) (p : (b : X ⟢ A) Γ— (mk b ⟢ U)) :
          (equiv_Sigma X U).symm p = p.snd.left
          source
          @[simp]
          theorem CategoryTheory.Over.equiv_Sigma_apply_fst {π’ž : Type u} [Category.{v, u} π’ž] {A : π’ž} (X : π’ž) (U : Over A) (g : X ⟢ U.left) :
          ((equiv_Sigma X U) g).fst = CategoryStruct.comp g U.hom
          source
          def CategoryTheory.Over.equivalence_Elements {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) :
          (yoneda.obj A).Elements β‰Œ (Over A)α΅’α΅–
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Over.equivalence_Elements_inverse_map_coe {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) {X✝ Y✝ : (Over A)α΅’α΅–} (f : X✝ ⟢ Y✝) :
            ↑((equivalence_Elements A).inverse.map f) = f.unop.left.op
            source
            @[simp]
            theorem CategoryTheory.Over.equivalence_Elements_functor_map {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) {X✝ Y✝ : (yoneda.obj A).Elements} (f : X✝ ⟢ Y✝) :
            (equivalence_Elements A).functor.map f = (homMk (↑f).unop β‹―).op
            source
            @[simp]
            theorem CategoryTheory.Over.equivalence_Elements_unitIso {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) :
            (equivalence_Elements A).unitIso = NatIso.ofComponents Iso.refl β‹―
            source
            @[simp]
            theorem CategoryTheory.Over.equivalence_Elements_inverse_obj_fst {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) (U : (Over A)α΅’α΅–) :
            ((equivalence_Elements A).inverse.obj U).fst = Opposite.op (Opposite.unop U).left
            source
            @[simp]
            theorem CategoryTheory.Over.equivalence_Elements_functor_obj {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) (x : (yoneda.obj A).Elements) :
            (equivalence_Elements A).functor.obj x = Opposite.op (mk x.snd)
            source
            @[simp]
            theorem CategoryTheory.Over.equivalence_Elements_counitIso {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) :
            (equivalence_Elements A).counitIso = NatIso.ofComponents Iso.refl β‹―
            source
            @[simp]
            theorem CategoryTheory.Over.equivalence_Elements_inverse_obj_snd {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) (U : (Over A)α΅’α΅–) :
            ((equivalence_Elements A).inverse.obj U).snd = (Opposite.unop U).hom
            source
            def CategoryTheory.Over.forget_iso_Sigma {π’ž : Type u} [Category.{v, u} π’ž] (A : π’ž) :
            (forget A).compβ‚‚ coyoneda β‰… Functor.Sigma ((equivalence_Elements A).functor.comp coyoneda)

            For X ∈ π’ž and f ∈ π’ž/A, π’ž(X, Over.forget f) β‰… Ξ£(g: X ⟢ A), π’ž/A(g, f).

            Equations
            Instances For