Documentation

Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

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

A morphism f : X ⟶ Y defines two functors:

These are adjoint under suitable assumptions on P and Q.

source
def CategoryTheory.MorphismProperty.Over.map {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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_obj_hom {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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
    @[simp]
    theorem CategoryTheory.MorphismProperty.Over.map_obj_left {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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_map_left {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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
    theorem CategoryTheory.MorphismProperty.Over.map_comp {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {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.mapComp {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] :
    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.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (X✝ : P.Over Q X) :
      ((mapComp Q hf hg).inv.app X✝).left = CategoryStruct.id X✝.left
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (X✝ : P.Over Q X) :
      ((mapComp Q hf hg).hom.app X✝).left = CategoryStruct.id X✝.left
      source
      noncomputable def CategoryTheory.MorphismProperty.Over.pullback {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] :
      Functor (P.Over Q Y) (P.Over Q X)

      If P and Q are stable under base change and pullbacks exist in T, 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_map_left {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [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
        @[simp]
        theorem CategoryTheory.MorphismProperty.Over.pullback_obj_hom {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [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.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) :
        ((pullback P Q f).obj A).left = Limits.pullback A.hom f
        source
        noncomputable def CategoryTheory.MorphismProperty.Over.pullbackComp {T : Type u_1} [Category.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
        pullback P Q (CategoryStruct.comp f g) ≅ (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.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : P.Over Q Z) :
          ((pullbackComp f g).inv.app X✝).left = (Limits.pullbackLeftPullbackSndIso X✝.hom g f).hom
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left {T : Type u_1} [Category.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : P.Over Q Z) :
          ((pullbackComp f g).hom.app X✝).left = (Limits.pullbackLeftPullbackSndIso X✝.hom g f).inv
          source
          theorem CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst {T : Type u_1} [Category.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (A : P.Over Q Z) :
          CategoryStruct.comp ((pullbackComp 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.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f 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
          Instances For
            source
            @[simp]
            theorem CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst {T : Type u_1} [Category.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f g : X ⟶ Y} (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.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f g : X ⟶ Y} (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.mapPullbackAdj {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Limits.HasPullbacks T] [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 f satisfies P.

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