base change / pullback

Stream: Is there code for X?

[Joseph Hua]

I was wondering where in the category theory library should the construction of a base change functor go?

[Joseph Hua]

import category_theory.over
import category_theory.limits.shapes.pullbacks

universes u₀ v₀

noncomputable theory

namespace category_theory

open limits

variables {C : Type u₀} [category.{v₀} C] [has_pullbacks C] {X Y} (g : X ⟶ Y)

/-- The `pullback_functor` on objects-/
@[simp] def pullback_functor_obj (E : over Y) : over X :=
over.mk (pullback.fst : (pullback g E.hom) ⟶ X)

/-
Consider the cone over the diagram     X ----> Y <---- E₁.left

                     pullback.snd          h.left
  pullback g E₀.hom -------------> E₀.left -----> E₁.left
        |                                           |
        | pullback.fst                              |
        V                                           |
        X ----------------------------------------> Y

The universal property of `pullback g E₁.hom` gives the below definition
-/
/-- The `pullback_functor` on morphisms, as a morphism in the category-/
@[simp] def pullback_functor_map_mk_map {E₀ E₁ : over Y} (h : E₀ ⟶ E₁) :
  (pullback_functor_obj g E₀).left ⟶ (pullback_functor_obj g E₁).left :=
limits.pullback.lift (pullback.fst : pullback g E₀.hom ⟶ X) (pullback.snd ≫ h.left)
(by { simp only [pullback.condition, category.assoc], congr, exact (over.w h).symm })

/-- The `pullback_functor` on morphisms -/
@[simp] def pullback_functor_map (E₀ E₁ : over Y) (h : E₀ ⟶ E₁) :
  pullback_functor_obj g E₀ ⟶ pullback_functor_obj g E₁ :=
over.hom_mk (pullback_functor_map_mk_map g h)
(by { dsimp, simp [limits.pullback.lift_fst] })

/-- Pullback as a functor between over categories -/
def pullback_functor {X Y : C} (g : X ⟶ Y) :
  over Y ⥤ over X :=
{ obj := λ E, over.mk (pullback.fst : (pullback g E.hom) ⟶ X),
  map := pullback_functor_map g }

notation g `^*`:40 := pullback_functor g

end category_theory

[Joseph Hua]

I would also like to show that pullback_functor (terminal.from Y) : C/* ⥤ C/* is the same as Y × - : C ⥤ C, I don't see C/* ⥤ C proven anywhere though

[Andrew Yang]

I think it should be added in src/category_theory/limits/shapes/pullbacks.lean.
Note that the map could also be
over.hom_mk (pullback.map _ _ _ _ i.left (𝟙 _) (𝟙 _) (by simp) (by simp)) (by simp) but that doesn't matter a lot.

Also it might be worth it to add over.map f ⊣ base_change f into src/category_theory/adjunction/over.lean. Feel free to steal these if you want.

This functor C/* ⥤ C should just be over.forget. The other way C ⥤ C/* is category_theory.star, but we only know that they are adjoint and I don't think we know the equivalence for terminal objects.

[Joseph Hua]

Andrew Yang said:

I think it should be added in src/category_theory/limits/shapes/pullbacks.lean.
Note that the map could also be
over.hom_mk (pullback.map _ _ _ _ i.left (𝟙 _) (𝟙 _) (by simp) (by simp)) (by simp) but that doesn't matter a lot.

Also it might be worth it to add over.map f ⊣ base_change f into src/category_theory/adjunction/over.lean. Feel free to steal these if you want.

This functor C/* ⥤ C should just be over.forget. The other way C ⥤ C/* is category_theory.star, but we only know that they are adjoint and I don't think we know the equivalence for terminal objects.

Thanks! About the last point - they are equivalent and I have just written up a proof. I will try to get back to you on the other points later

[Joseph Hua]

import category_theory.over
import category_theory.polynomial.basic

universes u₀ v₀

noncomputable theory

namespace category_theory

namespace endofunctor
open limits

variables {C : Type u₀} [category.{v₀} C] [has_pullbacks C] [has_terminal C] (X Y: C)

namespace over_terminal

/-
If category `C` has a terminal object then
`C` and `over ⊤_ C` (the overcategory of the terminal object)
are equivalent categories via the forgetful functor.
-/

/--
The inverse to the functor forgetting from the over category of the terminal object.
This leads to an equivalence in `is_equivalence_forget`.
-/
@[simp] def forget_inverse : C ⥤ over ⊤_ C :=
{ obj := λ X, over.mk (terminal.from X),
    map := λ X Y f, over.hom_mk f (by tidy) }

/-- On objects, the identity on `over ⊤_ C` is equal to the composition with `forget_inverse` -/
@[simp] def unit_iso_obj (X : over ⊤_ C) :
  X ≅ (over.forget (⊤_ C) ⋙ forget_inverse).obj X :=
eq_to_iso (by {cases X, congr, tidy})

/-- The identity on `over ⊤_ C` is naturally isomorphic to the composition with `forget_inverse` -/
def unit_iso : 𝟭 (over (⊤_ C)) ≅ over.forget (⊤_ C) ⋙ forget_inverse :=
nat_iso.of_components (λ X, unit_iso_obj X) (by tidy)

/-- The precomposition with the `forget_inverse` is naturally isomorphic to the identity on C -/
def counit_iso : forget_inverse ⋙ over.forget (⊤_ C) ≅ 𝟭 C :=
nat_iso.of_components (λ X, iso.refl _) (by tidy)

/-- The forgetful functor `over ⊤_ C → C` is an equivalence, with inverse `forget_inverse` -/
def is_equivalence_forget : is_equivalence (over.forget ⊤_ C) :=
is_equivalence.mk forget_inverse unit_iso counit_iso

/-
We show that `pullback_functor (terminal.from Y) : C/* ⥤ C/*`
is the same as `Y × - : C ⥤ C`, in the sense that the following
commutes

  C/* ⥤ C/*
   |      |
   |      | forget
   V      V
   C  ⥤  C
-/


end over_terminal
end endofunctor
end category_theory

[Joseph Hua]

oh i should change it to category.star wait no star doesn't seem like the right thing here aha they are the same thing

[Joseph Hua]

oh i see by "dont know" you meant "we don't have it in the library"

[Andrew Yang]

Yeah. By we I meant mathlib : )
I think forget_inverse should still be kept since that is the one people think of when considering the functor C ⥤ over ⊤_ C.
And it does not require that C has products. But a natural isomorphism should be useful.

[Joseph Hua]

pullback.map is a great idea!