Module

OverPullbackLeft.lean

Nyll.SchemeTheory.CategoryTheory.OverPullbackLeft

5 declarations indexed from sourceView source ↗

Module documentation

Pullback in over categories using left projections

The left-projection pullback functor on over categories is defined together with its object and morphism formulas. A natural isomorphism compares it with the usual over-category pullback functor.

Imports1

Mathlib.CategoryTheory.Comma.Over.Pullback

Imported by2

def

pullbackLeft

L36 ↗

CategoryTheory.Over.pullbackLeft

Documentation

Pullback over the first factor, retaining the native objects Limits.pullback c g.hom. The standard Over.pullback c uses the factors in the opposite order.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.Over
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPullbacks C]
noncomputable section

Lean source · full declaration

def pullbackLeft {X B : C} (c : X ⟶ B) : Over B ⥤ Over X where
  obj g := Over.mk (Limits.pullback.fst c g.hom)
  map {g h} k :=
    Over.homMk
      (Limits.pullback.map c g.hom c h.hom (𝟙 X) k.left (𝟙 B)
        ((Category.comp_id c).trans (Category.id_comp c).symm)
        ((Category.comp_id g.hom).trans (Over.w k).symm))
      (by
        simp only [Over.mk_hom]
        exact (Limits.pullback.lift_fst _ _ _).trans (Category.comp_id _))
  map_id g := by
    apply Over.OverMorphism.ext
    simp only [Over.homMk_left, Over.id_left]
    exact Limits.pullback.map_id
  map_comp {g h k} a b := by
    apply Over.OverMorphism.ext
    simp only [Over.comp_left, Over.homMk_left]
    symm
    refine (Limits.pullback.map_comp (𝟙 X) (𝟙 X) a.left b.left (𝟙 B) (𝟙 B)
      ((Category.comp_id c).trans (Category.id_comp c).symm)
      ((Category.comp_id g.hom).trans (Over.w a).symm)
      ((Category.comp_id c).trans (Category.id_comp c).symm)
      ((Category.comp_id h.hom).trans (Over.w b).symm)).trans ?_
    apply Limits.pullback.hom_ext <;>
      simp only [Limits.pullback.lift_fst, Limits.pullback.lift_snd, Category.comp_id]

theorem

pullbackLeft_obj_left

L63 ↗

CategoryTheory.Over.pullbackLeft_obj_left

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.Over
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPullbacks C]
noncomputable section

Lean source · statement

theorem pullbackLeft_obj_left {X B : C} (c : X ⟶ B) (g : Over B) :
    ((pullbackLeft c).obj g).left = Limits.pullback c g.hom

theorem

pullbackLeft_obj_hom

L67 ↗

CategoryTheory.Over.pullbackLeft_obj_hom

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.Over
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPullbacks C]
noncomputable section

Lean source · statement

theorem pullbackLeft_obj_hom {X B : C} (c : X ⟶ B) (g : Over B) :
    ((pullbackLeft c).obj g).hom = Limits.pullback.fst c g.hom

theorem

pullbackLeft_map_left

L71 ↗

CategoryTheory.Over.pullbackLeft_map_left

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.Over
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPullbacks C]
noncomputable section

Lean source · statement

theorem pullbackLeft_map_left {X B : C} (c : X ⟶ B) {g h : Over B} (k : g ⟶ h) :
    ((pullbackLeft c).map k).left =
      Limits.pullback.map c g.hom c h.hom (𝟙 X) k.left (𝟙 B)
        ((Category.comp_id c).trans (Category.id_comp c).symm)
        ((Category.comp_id g.hom).trans (Over.w k).symm)

def

pullbackLeftIsoPullback

L79 ↗

CategoryTheory.Over.pullbackLeftIsoPullback

Documentation

The native left-leg construction is naturally isomorphic to the existing Mathlib Limits.pullback functor; the comparison is the usual Limits.pullback symmetry.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe v u
namespace CategoryTheory.Over
open CategoryTheory Limits
variable {C : Type u} [Category.{v} C] [HasPullbacks C]
noncomputable section

Lean source · statement

def pullbackLeftIsoPullback {X B : C} (c : X ⟶ B) :
    pullbackLeft c ≅ Over.pullback c

Module documentation

Pullback in over categories using left projections

Declarations

pullbackLeft

pullbackLeft_obj_left

pullbackLeft_obj_hom

pullbackLeft_map_left

pullbackLeftIsoPullback