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} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (hPf : P f) :
CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (hPf : P f) (X✝ : CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤) :
    ((CategoryTheory.MorphismProperty.Over.map Q hPf).obj X✝).hom = CategoryTheory.CategoryStruct.comp X✝.hom f
    source
    @[simp]
    theorem CategoryTheory.MorphismProperty.Over.map_obj_left {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (hPf : P f) (X✝ : CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤) :
    ((CategoryTheory.MorphismProperty.Over.map Q hPf).obj X✝).left = X✝.left
    source
    @[simp]
    theorem CategoryTheory.MorphismProperty.Over.map_map_left {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (hPf : P f) {X✝ Y✝ : CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤} (f✝ : X✝ ⟶ Y✝) :
    ((CategoryTheory.MorphismProperty.Over.map Q hPf).map f✝).left = (CategoryTheory.MorphismProperty.Comma.Hom.hom f✝).left
    source
    theorem CategoryTheory.MorphismProperty.Over.map_comp {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) :
    CategoryTheory.MorphismProperty.Over.map Q ⋯ = (CategoryTheory.MorphismProperty.Over.map Q hf).comp (CategoryTheory.MorphismProperty.Over.map Q hg)
    source
    def CategoryTheory.MorphismProperty.Over.mapComp {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] :
    CategoryTheory.MorphismProperty.Over.map Q ⋯ ≅ (CategoryTheory.MorphismProperty.Over.map Q hf).comp (CategoryTheory.MorphismProperty.Over.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} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.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) :
      ((CategoryTheory.MorphismProperty.Over.mapComp Q hf hg).inv.app X✝).left = CategoryTheory.CategoryStruct.id X✝.left
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.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) :
      ((CategoryTheory.MorphismProperty.Over.mapComp Q hf hg).hom.app X✝).left = CategoryTheory.CategoryStruct.id X✝.left
      source
      noncomputable def CategoryTheory.MorphismProperty.Over.pullback {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] :
      CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {A B : P.Over Q Y} (g : A ⟶ B) :
        ((CategoryTheory.MorphismProperty.Over.pullback P Q f).map g).left = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom f) g.left) (CategoryTheory.Limits.pullback.snd A.hom f) ⋯
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.Over.pullback_obj_hom {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) :
        ((CategoryTheory.MorphismProperty.Over.pullback P Q f).obj A).hom = CategoryTheory.Limits.pullback.snd A.hom f
        source
        @[simp]
        theorem CategoryTheory.MorphismProperty.Over.pullback_obj_left {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) :
        ((CategoryTheory.MorphismProperty.Over.pullback P Q f).obj A).left = CategoryTheory.Limits.pullback A.hom f
        source
        noncomputable def CategoryTheory.MorphismProperty.Over.pullbackComp {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
        CategoryTheory.MorphismProperty.Over.pullback P Q (CategoryTheory.CategoryStruct.comp f g) ≅ (CategoryTheory.MorphismProperty.Over.pullback P Q g).comp (CategoryTheory.MorphismProperty.Over.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} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : P.Over Q Z) :
          ((CategoryTheory.MorphismProperty.Over.pullbackComp f g).inv.app X✝).left = (CategoryTheory.Limits.pullbackLeftPullbackSndIso X✝.hom g f).hom
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : P.Over Q Z) :
          ((CategoryTheory.MorphismProperty.Over.pullbackComp f g).hom.app X✝).left = (CategoryTheory.Limits.pullbackLeftPullbackSndIso X✝.hom g f).inv
          source
          theorem CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (A : P.Over Q Z) :
          CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.pullbackComp f g).hom.app A).left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd A.hom g) f) (CategoryTheory.Limits.pullback.fst A.hom g)) = CategoryTheory.Limits.pullback.fst A.hom (CategoryTheory.CategoryStruct.comp f g)
          source
          noncomputable def CategoryTheory.MorphismProperty.Over.pullbackCongr {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f g : X ⟶ Y} (h : f = g) :
          CategoryTheory.MorphismProperty.Over.pullback P Q f ≅ CategoryTheory.MorphismProperty.Over.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} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] [CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f g : X ⟶ Y} (h : f = g) (A : P.Over Q Y) :
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.pullbackCongr h).hom.app A).left (CategoryTheory.Limits.pullback.fst A.hom g) = CategoryTheory.Limits.pullback.fst A.hom f
            source
            @[simp]
            theorem CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] [CategoryTheory.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) :
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.pullbackCongr h).hom.app A).left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom g) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom f) h✝
            source
            noncomputable def CategoryTheory.MorphismProperty.Over.mapPullbackAdj {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [CategoryTheory.Limits.HasPullbacks T] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) :
            CategoryTheory.MorphismProperty.Over.map Q hPf ⊣ CategoryTheory.MorphismProperty.Over.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