Skip to content

Commit

Permalink
feat(category_theory/pullback): make the is_limit helper lemmas more …
Browse files Browse the repository at this point in the history 
…ergonomic (#3398)





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
@semorrison
semorrison and semorrison committed Jul 15, 2020
1 parent 8495f76 commit 51a75ff
Show file tree
Hide file tree
Showing 3 changed files with 93 additions and 67 deletions.
12 changes: 6 additions & 6 deletions src/category_theory/abelian/non_preadditive.lean
View file
Expand Up @@ -130,7 +130,7 @@ let ⟨b', hb'⟩ := kernel_fork.is_limit.lift' i' (kernel.ι (prod.lift f g)) $
... = (0 : kernel (prod.lift f g) ⟶ P ⨯ Q) ≫ limits.prod.snd : by rw kernel.condition_assoc
... = 0 : has_zero_morphisms.zero_comp _ _ in
{ cone := pullback_cone.mk a' b' $ by { simp at ha' hb', rw [ha', hb'] },
is_limit := pullback_cone.is_limit.mk _
is_limit := pullback_cone.is_limit.mk _ _ _
(λ s, kernel.lift (prod.lift f g) (pullback_cone.snd s ≫ b) $ prod.hom_ext
(calc ((pullback_cone.snd s ≫ b) ≫ prod.lift f g) ≫ limits.prod.fst
= pullback_cone.snd s ≫ b ≫ f : by simp only [prod.lift_fst, category.assoc]
Expand All @@ -147,9 +147,9 @@ let ⟨b', hb'⟩ := kernel_fork.is_limit.lift' i' (kernel.ι (prod.lift f g)) $
by { rw kernel_fork.ι_of_ι at ha', simp [ha', pullback_cone.condition s] })
(λ s, (cancel_mono b).1 $
by { rw kernel_fork.ι_of_ι at hb', simp [hb'] })
(λ s m h, (cancel_mono (kernel.ι (prod.lift f g))).1 $ calc m ≫ kernel.ι (prod.lift f g)
(λ s m h₁ h₂, (cancel_mono (kernel.ι (prod.lift f g))).1 $ calc m ≫ kernel.ι (prod.lift f g)
= m ≫ a' ≫ a : by { congr, exact ha'.symm }
... = pullback_cone.fst s ≫ a : by erw [←category.assoc, h walking_cospan.left]
... = pullback_cone.fst s ≫ a : by rw [←category.assoc, h₁]
... = pullback_cone.snd s ≫ b : pullback_cone.condition s
... = kernel.lift (prod.lift f g) (pullback_cone.snd s ≫ b) _ ≫ kernel.ι (prod.lift f g) :
by rw kernel.lift_ι) }
Expand All @@ -171,7 +171,7 @@ let ⟨b', hb'⟩ := cokernel_cofork.is_colimit.desc' i' (cokernel.π (coprod.de
... = coprod.inr ≫ (0 : P ⨿ Q ⟶ cokernel (coprod.desc f g)) : by rw cokernel.condition
... = 0 : has_zero_morphisms.comp_zero _ _ in
{ cocone := pushout_cocone.mk a' b' $ by { simp only [cofork.π_of_π] at ha' hb', rw [ha', hb'] },
is_colimit := pushout_cocone.is_colimit.mk _
is_colimit := pushout_cocone.is_colimit.mk _ _ _
(λ s, cokernel.desc (coprod.desc f g) (b ≫ pushout_cocone.inr s) $ coprod.hom_ext
(calc coprod.inl ≫ coprod.desc f g ≫ b ≫ pushout_cocone.inr s
= f ≫ b ≫ pushout_cocone.inr s : by rw coprod.inl_desc_assoc
Expand All @@ -185,9 +185,9 @@ let ⟨b', hb'⟩ := cokernel_cofork.is_colimit.desc' i' (cokernel.π (coprod.de
(λ s, (cancel_epi a).1 $
by { rw cokernel_cofork.π_of_π at ha', simp [reassoc_of ha', pushout_cocone.condition s] })
(λ s, (cancel_epi b).1 $ by { rw cokernel_cofork.π_of_π at hb', simp [reassoc_of hb'] })
(λ s m h, (cancel_epi (cokernel.π (coprod.desc f g))).1 $ calc cokernel.π (coprod.desc f g) ≫ m
(λ s m h₁ h₂, (cancel_epi (cokernel.π (coprod.desc f g))).1 $ calc cokernel.π (coprod.desc f g) ≫ m
= (a ≫ a') ≫ m : by { congr, exact ha'.symm }
... = a ≫ pushout_cocone.inl s : by erw [category.assoc, h walking_span.left]
... = a ≫ pushout_cocone.inl s : by rw [category.assoc, h₁]
... = b ≫ pushout_cocone.inr s : pushout_cocone.condition s
... = cokernel.π (coprod.desc f g) ≫ cokernel.desc (coprod.desc f g) (b ≫ pushout_cocone.inr s) _ :
by rw cokernel.π_desc) }
Expand Down
16 changes: 8 additions & 8 deletions src/category_theory/limits/shapes/constructions/pullbacks.lean
View file
Expand Up @@ -27,14 +27,14 @@ def has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair
[has_limit (parallel_pair (prod.fst ≫ f) (prod.snd ≫ g))] : has_limit (cospan f g) :=
let π₁ : X ⨯ Y ⟶ X := prod.fst, π₂ : X ⨯ Y ⟶ Y := prod.snd, e := equalizer.ι (π₁ ≫ f) (π₂ ≫ g) in
{ cone := pullback_cone.mk (e ≫ π₁) (e ≫ π₂) $ by simp only [category.assoc, equalizer.condition],
is_limit := pullback_cone.is_limit.mk _
is_limit := pullback_cone.is_limit.mk _ _ _
(λ s, equalizer.lift (prod.lift (s.π.app walking_cospan.left)
(s.π.app walking_cospan.right)) $ by
rw [←category.assoc, limit.lift_π, ←category.assoc, limit.lift_π];
exact pullback_cone.condition _)
(by simp) (by simp) $ λ s m h, by { ext,
{ simpa using h walking_cospan.left },
{ simpa using h walking_cospan.right } } }
(by simp) (by simp) $ λ s m h₁ h₂, by { ext,
{ simpa using h₁ },
{ simpa using h₂ } } }

section

Expand All @@ -59,14 +59,14 @@ let ι₁ : Y ⟶ Y ⨿ Z := coprod.inl, ι₂ : Z ⟶ Y ⨿ Z := coprod.inr,
c := coequalizer.π (f ≫ ι₁) (g ≫ ι₂) in
{ cocone := pushout_cocone.mk (ι₁ ≫ c) (ι₂ ≫ c) $
by rw [←category.assoc, ←category.assoc, coequalizer.condition],
is_colimit := pushout_cocone.is_colimit.mk _
is_colimit := pushout_cocone.is_colimit.mk _ _ _
(λ s, coequalizer.desc (coprod.desc (s.ι.app walking_span.left)
(s.ι.app walking_span.right)) $ by
rw [category.assoc, colimit.ι_desc, category.assoc, colimit.ι_desc];
exact pushout_cocone.condition _)
(by simp) (by simp) $ λ s m h, by { ext,
{ simpa using h walking_span.left },
{ simpa using h walking_span.right } } }
(by simp) (by simp) $ λ s m h₁ h₂, by { ext,
{ simpa using h₁ },
{ simpa using h₂ } } }

section

Expand Down
132 changes: 79 additions & 53 deletions src/category_theory/limits/shapes/pullbacks.lean
View file
Expand Up @@ -152,6 +152,33 @@ abbreviation fst (t : pullback_cone f g) : t.X ⟶ X := t.π.app walking_cospan.
/-- The second projection of a pullback cone. -/
abbreviation snd (t : pullback_cone f g) : t.X ⟶ Y := t.π.app walking_cospan.right

/-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content -/
def is_limit_aux (t : pullback_cone f g) (lift : Π (s : cone (cospan f g)), s.X ⟶ t.X)
(fac_left : ∀ (s : pullback_cone f g), lift s ≫ t.fst = s.fst)
(fac_right : ∀ (s : pullback_cone f g), lift s ≫ t.snd = s.snd)
(uniq : ∀ (s : pullback_cone f g) (m : s.X ⟶ t.X)
(w : ∀ j : walking_cospan, m ≫ t.π.app j = s.π.app j), m = lift s) :
is_limit t :=
{ lift := lift,
fac' := λ s j, option.cases_on j
(by { rw [← s.w inl, ← t.w inl, ←category.assoc], congr, exact fac_left s, } )
(λ j', walking_pair.cases_on j' (fac_left s) (fac_right s)),
uniq' := uniq }

/-- This is another convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts. -/
def is_limit_aux' (t : pullback_cone f g)
(create : Π (s : pullback_cone f g),
{l // l ≫ t.fst = s.fst ∧ l ≫ t.snd = s.snd ∧ ∀ {m}, m ≫ t.fst = s.fst → m ≫ t.snd = s.snd → m = l}) :
limits.is_limit t :=
pullback_cone.is_limit_aux t
(λ s, (create s).1)
(λ s, (create s).2.1)
(λ s, (create s).2.2.1)
(λ s m w, (create s).2.2.2 (w walking_cospan.left) (w walking_cospan.right))

/-- A pullback cone on `f` and `g` is determined by morphisms `fst : W ⟶ X` and `snd : W ⟶ Y`
such that `fst ≫ f = snd ≫ g`. -/
@[simps]
Expand Down Expand Up @@ -194,38 +221,24 @@ def is_limit.lift' {t : pullback_cone f g} (ht : is_limit t) {W : C} (h : W ⟶
(w : h ≫ f = k ≫ g) : {l : W ⟶ t.X // l ≫ fst t = h ∧ l ≫ snd t = k} :=
⟨ht.lift $ pullback_cone.mk _ _ w, ht.fac _ _, ht.fac _ _⟩

/-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content -/
def is_limit.mk (t : pullback_cone f g) (lift : Π (s : cone (cospan f g)), s.X ⟶ t.X)
(fac_left : ∀ (s : cone (cospan f g)), lift s ≫ t.π.app walking_cospan.left = s.π.app walking_cospan.left)
(fac_right : ∀ (s : cone (cospan f g)), lift s ≫ t.π.app walking_cospan.right = s.π.app walking_cospan.right)
(uniq : ∀ (s : cone (cospan f g)) (m : s.X ⟶ t.X)
(w : ∀ j : walking_cospan, m ≫ t.π.app j = s.π.app j), m = lift s) :
is_limit t :=
{ lift := lift,
fac' := λ s j, option.cases_on j
(by { simp [← s.w inl, ← t.w inl, ← fac_left s] } )
(λ j', walking_pair.cases_on j' (fac_left s) (fac_right s)),
uniq' := uniq }

/-- This is another convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts. -/
def is_limit.mk' (t : pullback_cone f g)
(create : Π (s : pullback_cone f g),
{l // l ≫ t.fst = s.fst ∧ l ≫ t.snd = s.snd ∧ ∀ {m}, m ≫ t.fst = s.fst → m ≫ t.snd = s.snd → m = l}) :
is_limit t :=
pullback_cone.is_limit.mk t
(λ s, (create s).1)
(λ s, (create s).2.1)
(λ s, (create s).2.2.1)
(λ s m w, (create s).2.2.2 (w walking_cospan.left) (w walking_cospan.right))
/--
This is a more convenient formulation to show that a `pullback_cone` constructed using
`pullback_cone.mk` is a limit cone.
-/
def is_limit.mk {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : fst ≫ f = snd ≫ g)
(lift : Π (s : pullback_cone f g), s.X ⟶ W)
(fac_left : ∀ (s : pullback_cone f g), lift s ≫ fst = s.fst)
(fac_right : ∀ (s : pullback_cone f g), lift s ≫ snd = s.snd)
(uniq : ∀ (s : pullback_cone f g) (m : s.X ⟶ W)
(w_fst : m ≫ fst = s.fst) (w_snd : m ≫ snd = s.snd), m = lift s) :
is_limit (mk fst snd eq) :=
is_limit_aux _ lift fac_left fac_right (λ s m w, uniq s m (w walking_cospan.left) (w walking_cospan.right))

/-- The flip of a pullback square is a pullback square. -/
def flip_is_limit {W : C} {h : W ⟶ X} {k : W ⟶ Y}
{comm : h ≫ f = k ≫ g} (t : is_limit (mk _ _ comm.symm)) :
is_limit (mk _ _ comm) :=
is_limit.mk' _ $ λ s,
is_limit_aux' _ $ λ s,
begin
refine ⟨(is_limit.lift' t _ _ s.condition.symm).1,
(is_limit.lift' t _ _ _).2.2,
Expand All @@ -251,6 +264,32 @@ abbreviation inl (t : pushout_cocone f g) : Y ⟶ t.X := t.ι.app walking_span.l
/-- The second inclusion of a pushout cocone. -/
abbreviation inr (t : pushout_cocone f g) : Z ⟶ t.X := t.ι.app walking_span.right

/-- This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone.
It only asks for a proof of facts that carry any mathematical content -/
def is_colimit_aux (t : pushout_cocone f g) (desc : Π (s : pushout_cocone f g), t.X ⟶ s.X)
(fac_left : ∀ (s : pushout_cocone f g), t.inl ≫ desc s = s.inl)
(fac_right : ∀ (s : pushout_cocone f g), t.inr ≫ desc s = s.inr)
(uniq : ∀ (s : pushout_cocone f g) (m : t.X ⟶ s.X)
(w : ∀ j : walking_span, t.ι.app j ≫ m = s.ι.app j), m = desc s) :
is_colimit t :=
{ desc := desc,
fac' := λ s j, option.cases_on j (by { simp [← s.w fst, ← t.w fst, fac_left s] } )
(λ j', walking_pair.cases_on j' (fac_left s) (fac_right s)),
uniq' := uniq }

/-- This is another convenient method to verify that a pushout cocone is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts. -/
def is_colimit_aux' (t : pushout_cocone f g)
(create : Π (s : pushout_cocone f g),
{l // t.inl ≫ l = s.inl ∧ t.inr ≫ l = s.inr ∧ ∀ {m}, t.inl ≫ m = s.inl → t.inr ≫ m = s.inr → m = l}) :
is_colimit t :=
is_colimit_aux t
(λ s, (create s).1)
(λ s, (create s).2.1)
(λ s, (create s).2.2.1)
(λ s m w, (create s).2.2.2 (w walking_cospan.left) (w walking_cospan.right))

/-- A pushout cocone on `f` and `g` is determined by morphisms `inl : Y ⟶ W` and `inr : Z ⟶ W` such
that `f ≫ inl = g ↠ inr`. -/
@[simps]
Expand Down Expand Up @@ -293,37 +332,24 @@ def is_colimit.desc' {t : pushout_cocone f g} (ht : is_colimit t) {W : C} (h : Y
(w : f ≫ h = g ≫ k) : {l : t.X ⟶ W // inl t ≫ l = h ∧ inr t ≫ l = k } :=
⟨ht.desc $ pushout_cocone.mk _ _ w, ht.fac _ _, ht.fac _ _⟩

/-- This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone.
It only asks for a proof of facts that carry any mathematical content -/
def is_colimit.mk (t : pushout_cocone f g) (desc : Π (s : cocone (span f g)), t.X ⟶ s.X)
(fac_left : ∀ (s : cocone (span f g)), t.ι.app walking_span.left ≫ desc s = s.ι.app walking_span.left)
(fac_right : ∀ (s : cocone (span f g)), t.ι.app walking_span.right ≫ desc s = s.ι.app walking_span.right)
(uniq : ∀ (s : cocone (span f g)) (m : t.X ⟶ s.X)
(w : ∀ j : walking_span, t.ι.app j ≫ m = s.ι.app j), m = desc s) :
is_colimit t :=
{ desc := desc,
fac' := λ s j, option.cases_on j (by { simp [← s.w fst, ← t.w fst, fac_left s] } )
(λ j', walking_pair.cases_on j' (fac_left s) (fac_right s)),
uniq' := uniq }

/-- This is another convenient method to verify that a pushout cocone is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts. -/
def is_colimit.mk' (t : pushout_cocone f g)
(create : Π (s : pushout_cocone f g),
{l // t.inl ≫ l = s.inl ∧ t.inr ≫ l = s.inr ∧ ∀ {m}, t.inl ≫ m = s.inl → t.inr ≫ m = s.inr → m = l}) :
is_colimit t :=
is_colimit.mk t
(λ s, (create s).1)
(λ s, (create s).2.1)
(λ s, (create s).2.2.1)
(λ s m w, (create s).2.2.2 (w walking_cospan.left) (w walking_cospan.right))
/--
This is a more convenient formulation to show that a `pushout_cocone` constructed using
`pushout_cocone.mk` is a colimit cocone.
-/
def is_colimit.mk {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : f ≫ inl = g ≫ inr)
(desc : Π (s : pushout_cocone f g), W ⟶ s.X)
(fac_left : ∀ (s : pushout_cocone f g), inl ≫ desc s = s.inl)
(fac_right : ∀ (s : pushout_cocone f g), inr ≫ desc s = s.inr)
(uniq : ∀ (s : pushout_cocone f g) (m : W ⟶ s.X)
(w_inl : inl ≫ m = s.inl) (w_inr : inr ≫ m = s.inr), m = desc s) :
is_colimit (mk inl inr eq) :=
is_colimit_aux _ desc fac_left fac_right (λ s m w, uniq s m (w walking_cospan.left) (w walking_cospan.right))

/-- The flip of a pushout square is a pushout square. -/
def flip_is_colimit {W : C} {h : Y ⟶ W} {k : Z ⟶ W}
{comm : f ≫ h = g ≫ k} (t : is_colimit (mk _ _ comm.symm)) :
is_colimit (mk _ _ comm) :=
is_colimit.mk' _ $ λ s,
is_colimit_aux' _ $ λ s,
begin
refine ⟨(is_colimit.desc' t _ _ s.condition.symm).1,
(is_colimit.desc' t _ _ _).2.2,
Expand Down

0 comments on commit 51a75ff

Please sign in to comment.