Documentation

Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Adjunction of pushforward and pullback in P.Over Q X #

Under suitable assumptions on P, Q and f, a morphism f : X ⟶ Y defines two functors:

such that Over.map is the left adjoint to Over.pullback.

source
def CategoryTheory.MorphismProperty.Over.map {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) :
Functor (P.Over Q X) (P.Over Q Y)

If P is stable under composition and f : X ⟶ Y satisfies P, this is the functor P.Over Q X ⥤ P.Over Q Y given by composing with f.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.MorphismProperty.Over.map_map_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) {X✝ Y✝ : MorphismProperty.Comma (Functor.id T) (Functor.fromPUnit X) P Q ⊤} (f✝ : X✝ ⟶ Y✝) :
    ((map Q hPf).map f✝).left = (Comma.Hom.hom f✝).left
    source
    @[simp]
    theorem CategoryTheory.MorphismProperty.Over.map_obj_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) (X✝ : MorphismProperty.Comma (Functor.id T) (Functor.fromPUnit X) P Q ⊤) :
    ((map Q hPf).obj X✝).left = X✝.left
    source
    @[simp]
    theorem CategoryTheory.MorphismProperty.Over.map_obj_hom {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) (X✝ : MorphismProperty.Comma (Functor.id T) (Functor.fromPUnit X) P Q ⊤) :
    ((map Q hPf).obj X✝).hom = CategoryStruct.comp X✝.hom f
    source
    theorem CategoryTheory.MorphismProperty.Over.map_comp {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) :
    map Q ⋯ = (map Q hf).comp (map Q hg)
    source
    def CategoryTheory.MorphismProperty.Over.mapCongr {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) :
    map Q hf ≅ map Q ⋯

    Promote an equality to an isomorphism of Over.map functors.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X✝ : P.Over Q X) :
      ((mapCongr Q hfg hf).hom.app X✝).left = CategoryStruct.id X✝.left
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X✝ : P.Over Q X) :
      ((mapCongr Q hfg hf).inv.app X✝).left = CategoryStruct.id X✝.left
      source
      def CategoryTheory.MorphismProperty.Over.mapId {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryStruct.id X) (hf : f = CategoryStruct.id X := by cat_disch) :
      map Q ⋯ ≅ Functor.id (P.Over Q X)

      Over.map preserves identities.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.Over.mapId_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryStruct.id X) (hf : f = CategoryStruct.id X := by cat_disch) (X✝ : P.Over Q X) :
        ((mapId Q X f hf).inv.app X✝).left = CategoryStruct.id X✝.left
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.Over.mapId_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryStruct.id X) (hf : f = CategoryStruct.id X := by cat_disch) (X✝ : P.Over Q X) :
        ((mapId Q X f hf).hom.app X✝).left = CategoryStruct.id X✝.left
        source
        def CategoryTheory.MorphismProperty.Over.mapComp {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) :
        map Q ⋯ ≅ (map Q hf).comp (map Q hg)

        Over.map commutes with composition.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q X) :
          ((mapComp Q hf hg fg hfg).inv.app X✝).left = CategoryStruct.id X✝.left
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q X) :
          ((mapComp Q hf hg fg hfg).hom.app X✝).left = CategoryStruct.id X✝.left
          source
          instance CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] (A : P.Over Q Y) :
          Limits.HasPullback A.hom f
          source
          instance CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [P.IsStableUnderBaseChangeAlong g] (A : P.Over Q Z) :
          Limits.HasPullback (Limits.pullback.snd A.hom g) f
          source
          noncomputable def CategoryTheory.MorphismProperty.Over.pullback {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] :
          Functor (P.Over Q Y) (P.Over Q X)

          If P and Q are stable under base change and pullbacks along f exist for morphisms in P, this is the functor P.Over Q Y ⥤ P.Over Q X given by base change along f.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.MorphismProperty.Over.pullback_obj_hom {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) :
            ((pullback P Q f).obj A).hom = Limits.pullback.snd A.hom f
            source
            @[simp]
            theorem CategoryTheory.MorphismProperty.Over.pullback_obj_left {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) :
            ((pullback P Q f).obj A).left = Limits.pullback A.hom f
            source
            @[simp]
            theorem CategoryTheory.MorphismProperty.Over.pullback_map_left {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] {A B : P.Over Q Y} (g : A ⟶ B) :
            ((pullback P Q f).map g).left = Limits.pullback.lift (CategoryStruct.comp (Limits.pullback.fst A.hom f) g.left) (Limits.pullback.snd A.hom f) ⋯
            source
            noncomputable def CategoryTheory.MorphismProperty.Over.pullbackComp {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) :
            pullback P Q fg ≅ (pullback P Q g).comp (pullback P Q f)

            Over.pullback commutes with composition.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q Z) :
              ((pullbackComp f g fg hfg).inv.app X✝).left = CategoryStruct.comp (Limits.pullbackLeftPullbackSndIso X✝.hom g f).hom (Limits.pullback.map X✝.hom (CategoryStruct.comp f g) X✝.hom fg (CategoryStruct.id X✝.left) (CategoryStruct.id X) (CategoryStruct.id Z) ⋯ ⋯)
              source
              @[simp]
              theorem CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q Z) :
              ((pullbackComp f g fg hfg).hom.app X✝).left = CategoryStruct.comp (Limits.pullback.map X✝.hom fg X✝.hom (CategoryStruct.comp f g) (CategoryStruct.id X✝.left) (CategoryStruct.id X) (CategoryStruct.id Z) ⋯ ⋯) (Limits.pullbackLeftPullbackSndIso X✝.hom g f).inv
              source
              theorem CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (A : P.Over Q Z) :
              CategoryStruct.comp ((pullbackComp f g (CategoryStruct.comp f g) ⋯).hom.app A).left (CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.snd A.hom g) f) (Limits.pullback.fst A.hom g)) = Limits.pullback.fst A.hom (CategoryStruct.comp f g)
              source
              noncomputable def CategoryTheory.MorphismProperty.Over.pullbackCongr {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] {g : X ⟶ Y} (h : f = g) :
              pullback P Q f ≅ pullback P Q g

              If f = g, then base change along f is naturally isomorphic to base change along g.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPullbacksAlong f] {g : X ⟶ Y} [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (h : f = g) (A : P.Over Q Y) :
                CategoryStruct.comp ((pullbackCongr h).hom.app A).left (Limits.pullback.fst A.hom g) = Limits.pullback.fst A.hom f
                source
                @[simp]
                theorem CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPullbacksAlong f] {g : X ⟶ Y} [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (h : f = g) (A : P.Over Q Y) {Z : T} (h✝ : A.left ⟶ Z) :
                CategoryStruct.comp ((pullbackCongr h).hom.app A).left (CategoryStruct.comp (Limits.pullback.fst A.hom g) h✝) = CategoryStruct.comp (Limits.pullback.fst A.hom f) h✝
                source
                noncomputable def CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} (f : X ⟶ Y) (hPf : P f) (hQf : Q f) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [Q.IsStableUnderBaseChange] [Limits.HasPullbacks T] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : CategoryStruct.comp f g = fg := by cat_disch) :
                (pullback P Q fg).comp (map Q hPf) ⟶ pullback P Q g

                The natural map between pullback functors induced by pullback.map.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} (f : X ⟶ Y) (hPf : P f) (hQf : Q f) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [Q.IsStableUnderBaseChange] [Limits.HasPullbacks T] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : CategoryStruct.comp f g = fg := by cat_disch) (A : P.Over Q Z) :
                  (pullbackMapHomPullback f hPf hQf g fg hfg).app A = Over.homMk (Limits.pullback.map A.hom fg A.hom g (CategoryStruct.id A.left) f (CategoryStruct.id Z) ⋯ ⋯) ⋯ ⋯
                  source
                  noncomputable def CategoryTheory.MorphismProperty.Over.mapPullbackAdj {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderBaseChange] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) :
                  map Q hPf ⊣ pullback P Q f

                  P.Over.map is left adjoint to P.Over.pullback if pullbacks of morphisms satisfying P exist along f and are also in P, and f is in both P and Q.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderBaseChange] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) (Y✝ : P.Over Q Y) :
                    (mapPullbackAdj P Q f hPf hQf).counit.app Y✝ = Over.homMk (Limits.pullback.fst Y✝.hom f) ⋯ ⋯
                    source
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderBaseChange] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) (X✝ : P.Over Q X) :
                    (mapPullbackAdj P Q f hPf hQf).unit.app X✝ = Over.homMk (Limits.pullback.lift (CategoryStruct.id X✝.left) X✝.hom ⋯) ⋯ ⋯