feat(CategoryTheory/Limits): Pullback squares in cartesian monoidal categories by edegeltje · Pull Request #37045 · leanprover-community/mathlib4

edegeltje · 2026-03-23T16:32:51Z

This PR adds various lemmas about standard pullback squares in categories with chosen finite products.

github-actions · 2026-03-23T16:33:59Z

PR summary 96c77b07ff

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.CartesianMonoidal` (new file)	663

Declarations diff

+ HasEqualizer.of_isPullback_lift_diag_of_cartesianMonoidal
+ IsPullback.comp_lift_diag_tensorHom
+ IsPullback.comp_lift_of_isPullback_of_cartesianMonoidal
+ IsPullback.equalizer_ι_comp_lift_diag_of_cartesianMonoidal
+ IsPullback.fst_snd_toUnit_toUnit
+ IsPullback.of_isPullback_diag_tensorHom
+ IsPullback.tensor
+ IsPullback.whiskerLeft_horiz
+ IsPullback.whiskerRight_horiz
+ lift_tensorObjProdIso_hom
+ lift_tensorObjProdIso_inv
+ tensorObjProdIso
+ tensorObjProdIso_hom
+ tensorObjProdIso_hom_braiding_hom
+ tensorObjProdIso_hom_fst
+ tensorObjProdIso_hom_map
+ tensorObjProdIso_hom_snd
+ tensorObjProdIso_hom_whiskerLeft
+ tensorObjProdIso_hom_whiskerRight
+ tensorObjProdIso_inv
+ tensorObjProdIso_inv_braiding_hom
+ tensorObjProdIso_inv_fst
+ tensorObjProdIso_inv_snd
+ tensorObjProdIso_inv_tensorHom
+ tensorObjProdIso_inv_whiskerLeft
+ tensorObjProdIso_inv_whiskerRight

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/CartesianMonoidal.lean

robin-carlier · 2026-03-27T12:27:43Z

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/CartesianMonoidal.lean

+/--
+In a cartesian monoidal category, the following is a pullback square:
+```
+     (f ▷ Z)
+X ⊗ Z  →  Y ⊗ Z
+  |          |
+  π₁         π₁
+  ↓          ↓
+  X   -f→    Y
+```
+-/
+lemma IsPullback.whiskerRight_horiz {X Y : C} (f : X ⟶ Y) (Z : C) :
+    IsPullback (f ▷ Z) (fst X Z) (fst Y Z) f := by
+  refine IsPullback.of_isLimit' (by simp) ?_
+  apply PullbackCone.IsLimit.mk _ fun s => CartesianMonoidalCategory.lift s.snd (s.fst ≫ snd _ _)
+  · intro s
+    ext <;> simp [s.condition]
+  · cat_disch
+  · intro s m hm₁ hm₂
+    ext
+    · simpa
+    · simp [← hm₁]


I didn’t try with this one, but perhaps you can reduce it to CategoryTheory.IsPullback.of_prod_fst_with_id?

i tried it, and it turns out that that lemma is bait. instead this is more easily proven with IsPullback.of_right and IsPullback.fst_snd_toUnit_toUnit twice. In order to go the route via IsPullback.of_prod_fst_with_id, we need better API for an Iso between Limits.prod and tensorObj. I wrote some API in the Monoidal/Cartesian/Basic file, which can be split from this PR if you think it's good enough.

robin-carlier · 2026-03-27T12:44:06Z

Also, since we're adding this kind of square, we could as well give this one as a shortcut

lemma isPullback_toUnit_toUnit (X Y : C) :
    IsPullback (fst X Y) (snd X Y) (toUnit _) (toUnit _) :=
  .of_isLimit_binaryFan_of_isTerminal (tensorProductIsBinaryProduct X Y) isTerminalTensorUnit

(or maybe with a better name)

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/CartesianMonoidal.lean

Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/CartesianMonoidal.lean

robin-carlier · 2026-04-03T07:51:29Z

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/CartesianMonoidal.lean

+      use hpb.lift (a ≫ f) (CartesianMonoidalCategory.lift a b) (by cat_disch)
+      simp)
+
+lemma IsPullback.pullback_fst_monoidal {A₁ A₂ A₃ B₁ B₂ B₃ Z₁ Z₂ : C}


Suggested change

lemma IsPullback.pullback_fst_monoidal {A₁ A₂ A₃ B₁ B₂ B₃ Z₁ Z₂ : C}

lemma IsPullback.comp_lift_of_isPullback {A₁ A₂ A₃ B₁ B₂ B₃ Z₁ Z₂ : C}

maybe? I have to admit I’m not sure what would be a good name for this one, but given that fst is not in the statement, I think the current one is not correct. Same for its snd twin below.

Also, can you please copy over the description from the module docstring as a docstring here? so that in other files we can have some info by hovering of the term

the fst refers to the fact that we're taking the pullback of the top morphisms in two pullback squares which are commonly named fst as a variable, similar to how one would refer to pullback.fst if we were using the HasPullback API... but i agree that it's hard to determine the statement of the lemma merely from the names. I suppose we might just drop the snd version, since it can be obtained relatively easily from this one some combination of fliping the fst version? which then leaves name space (hah) for the fst version not to mention fst

I removed the snd variant. I decided to also add of_cartesianMonoidal to the name, since other than that i don't see what disambiguates this lemma from the (possibly hypothetical) HasProducts variant (i.e. the one that uses Limits.prod instead), but i'm open to other disambiguating strategies. I did this for the HasEqualizer lemmas as well

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/CartesianMonoidal.lean

Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

add lemmas

8f300cd

github-actions bot added the t-category-theory Category theory label Mar 23, 2026

run lake exe mk_all

98d1943

mathlib-triage bot assigned joelriou Mar 26, 2026

dagurtomas reviewed Mar 26, 2026

View reviewed changes

dagurtomas added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 26, 2026

adapt suggestions

cea5d72

edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026

robin-carlier reviewed Mar 27, 2026

View reviewed changes

robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026

edegeltje added 4 commits March 27, 2026 23:20

simplify proofs

d491efd

simplify proofs more

242c254

tiny golf

92f9561

make linter happy

ac7a259

edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026

remove lint command

7bf409a

joelriou reviewed Mar 31, 2026

View reviewed changes

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/CartesianMonoidal.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026

edegeltje added 2 commits March 31, 2026 13:06

Merge branch 'master' into ispullback_monoidal

e8d8981

fix non-terminal simps

073440e

edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026

robin-carlier reviewed Apr 3, 2026

View reviewed changes

robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026

FernandoChu reviewed Apr 3, 2026

View reviewed changes

edegeltje added 2 commits April 4, 2026 10:20

adapt suggestions

d76b7ea

fix lint

a71669c

edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 4, 2026

	lemma IsPullback.pullback_fst_monoidal {A₁ A₂ A₃ B₁ B₂ B₃ Z₁ Z₂ : C}
	lemma IsPullback.comp_lift_of_isPullback {A₁ A₂ A₃ B₁ B₂ B₃ Z₁ Z₂ : C}

Conversation

edegeltje commented Mar 23, 2026

Uh oh!

github-actions bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 96c77b07ff

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

robin-carlier Mar 27, 2026

Choose a reason for hiding this comment

Uh oh!

edegeltje Mar 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robin-carlier commented Mar 27, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

robin-carlier Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

edegeltje Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

edegeltje Apr 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Mar 23, 2026 •

edited

Loading

edegeltje Mar 27, 2026 •

edited

Loading

edegeltje Apr 4, 2026 •

edited

Loading