Mathlib extraction staging: nested Fubini and Beck-Chevalley

docs/EXTRACTION_LEDGER.md

@@ -89,6 +89,10 @@ product Fubini. Proposed path: `Mathlib/CategoryTheory/Limits/Shapes/Ends/Fubini
 
 **Proof dependencies:** `EndKan.End.Core`, `EndKan.Fubini.Slice`, `EndKan.Fubini.Nested`.
 
+**Staging package:** `scratch/mathlib-fubini/` (`LEMMA_MAP.md`, `MODULE_STRUCTURE.md`);
+buildable examples in `src/Scratch/MathlibFubiniExamples.lean`; PR brief in
+`docs/MATHLIB_PR_FUBINI.md`.
+
 ---
 
 ## 6. Fubini coends
@@ -107,6 +111,9 @@ Proposed path: parallel to end Fubini helpers in Mathlib.
 
 **Proof dependencies:** `EndKan.Coend.Core`, `EndKan.Fubini.CoendSlice`, `EndKan.Fubini.NestedCoend`.
 
+**Staging package:** shared with §5 — `scratch/mathlib-fubini/`, `src/Scratch/MathlibFubiniExamples.lean`,
+`docs/MATHLIB_PR_FUBINI.md`.
+
 ---
 
 ## 7. Kan extension helpers
@@ -127,6 +134,9 @@ main upstream gap. Proposed path: `Mathlib/CategoryTheory/Functor/KanExtension/B
 **Proof dependencies:** `EndKan.Kan.Core`, `EndKan.Kan.BeckChevalley`,
 `EndKan.Kan.BeckChevalley.Hypotheses` (optional).
 
+**Staging package:** `scratch/mathlib-kan-bc/` (`LEMMA_MAP.md`); design brief in
+`docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md`; examples in `src/Scratch/MathlibKanBcExamples.lean`.
+
 ---
 
 ## 10. Beck–Chevalley

docs/MATHLIB_PR_FUBINI.md

@@ -0,0 +1,73 @@
+# Mathlib PR: nested Fubini for ends and coends
+
+## PR title
+
+`feat(CategoryTheory/Limits): nested product Fubini helpers for ends and coends`
+
+## Summary
+
+Package **nested Fubini** isomorphisms for profunctors on product categories:
+
+- `EndObj F ≅ endNestedObj F` for `F : (C × D)ᵒᵖ × (C × D) ⥤ E`
+- `CoendObj F ≅ coendNestedObj F` for `F : (C × D) × (C × D)ᵒᵖ ⥤ E`
+
+Extracted from `EndKan.Fubini` (`Slice`, `Nested`, `CoendSlice`, `NestedCoend`).
+Staging: `scratch/mathlib-fubini/`, `src/Scratch/MathlibFubiniExamples.lean`.
+
+## Motivation
+
+Mathlib users currently hand-assemble slice embeddings, inner ends/coends, and nested
+outer profunctors. A small Fubini library reduces bookkeeping for double limits over
+`C × D`.
+
+## Proposed files (phased)
+
+| Phase | Mathlib path | Content |
+|-------|--------------|---------|
+| 1 | `Limits/Shapes/End/Fubini/Slice.lean` | `endSlice`, `endInnerMap`, wedge lemmas |
+| 2 | `Limits/Shapes/End/Fubini/Nested.lean` | `endFubiniIso` under hypothesis class |
+| 3 | `Limits/Shapes/Coend/Fubini/*` | coend mirror |
+| 4 | `Limits/Shapes/*/Fubini/Examples.lean` | constant functor instance |
+
+## Lemma checklist
+
+### Ready for Mathlib (with hypothesis)
+
+- [ ] `endSliceEmbed`, `endSlice`, `endWedge`, indexing `@[simp]` lemmas
+- [ ] `endInnerObj`, `endInnerπ`, `endInnerLift`, `endInnerMap` + spec/id/comp
+- [ ] `endSlice_cov_contr` (from `Limits.end_.condition`)
+- [ ] `endOuterProfunctor`, `endNestedObj`, `endFubiniForward` / `Backward`, `endFubiniIso`
+- [ ] Coend mirror: `coendSlice*`, `coendInnerMap`, `coendFubiniIso`
+- [ ] Public targets `end_fubini_target`, `coend_fubini_target`
+
+### Documented boundary (not hidden)
+
+- [ ] `AllEndSliceContrIso` / `CoendSliceContrIso` — contr-leg iso per profunctor
+- [ ] rc1 mutual `IsIso` bootstrap failure (see `scratch/SliceIsoMin.lean`)
+
+### Explicitly deferred
+
+- [ ] Unconditional contr-leg iso instances
+- [ ] EndKan tactics, telemetry, FFI
+- [ ] Full comma-category Beck–Chevalley (separate design issue)
+
+## Test plan
+
+- [ ] `lake build` Mathlib CI on new modules
+- [ ] Constant profunctor example (`OneCat`) elaborates `endFubiniIso`
+- [ ] No import of automation / experimental modules
+
+## Local verification
+
+```powershell
+lake build EndKan.Fubini
+lake build Scratch.MathlibFubiniExamples
+.\scripts\acceptance.ps1
+```
+
+## Remaining gaps before Mathlib submission
+
+1. Maintainer agreement on hypothesis class vs cov-only inner map
+2. Naming: `EndIdx` vs raw `Prod ((C×D)ᵒᵖ) (C×D)`
+3. Whether Fubini PR waits for end/coend β/η PRs (#1–#2) to land first
+4. Zulip design thread before opening Mathlib PR

docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md

@@ -0,0 +1,67 @@
+# Mathlib design issue: Beck–Chevalley for comma squares
+
+## Issue title
+
+`Design: Beck–Chevalley comparison for commutative squares of functors`
+
+## Summary
+
+Propose a Mathlib API for the **Beck–Chevalley comparison morphism**
+
+`Lan_K (L ⋙ N ⋙ F) ⟶ M ⋙ F`
+
+associated to a commutative square `K ⋙ M = L ⋙ N`, and document which geometric
+hypotheses imply it is an isomorphism.
+
+EndKan staging: `EndKan.Kan.BeckChevalley`, `EndKan.Kan.BeckChevalley.Hypotheses`,
+`scratch/mathlib-kan-bc/`.
+
+## What Mathlib already has
+
+- Pointwise left Kan extensions (`Functor.KanExtension.Pointwise`)
+- Comma categories (`CostructuredArrow`, `StructuredArrow`)
+- Finality lemmas (not yet wired into a BC pipeline in EndKan default import graph)
+
+## What EndKan proves today
+
+| Result | Hypothesis |
+|--------|------------|
+| `reflSquare_beckChevalley` | `[IsEquivalence K]` |
+| `pullbackSquare_of_equivalence` | `[IsEquivalence K]` |
+| `fullyFaithfulSquare_of_equivalence` | `[IsEquivalence K,L]`, `[Faithful M]`, FF on legs |
+| `exactSquare_of_equivalence` | + `[Faithful L]`, `[PreservesFilteredColimits M]` |
+
+Comparison map is `descOfIsLeftKanExtension` from the pointwise unit; iso follows from
+`isLeftKanExtensionAlongEquivalence'`.
+
+## Open design questions
+
+1. Should `BeckChevalley` be a typeclass with a `compare_iso` field, or a theorem family?
+2. Naming: `beckChevalleyCompare` vs Mathlib `Lan` API conventions
+3. Pullback squares: comma-category formulation vs equivalence shortcut
+4. Whether `Comma.final_fst` imports are acceptable in core Mathlib (linker budget)
+
+## Proposed minimal Mathlib PR (after design approval)
+
+- Document comparison morphism for `reflSquare`
+- Instance under `[IsEquivalence K]` mirroring `isLeftKanExtensionAlongEquivalence'`
+- **No** EndKan tactics in Mathlib
+
+## Explicitly out of scope for first Mathlib PR
+
+- Full comma-pullback proof of BC
+- EndKan automation (`beck_chevalley!`)
+- Fubini lemmas (separate PR track)
+
+## Local verification
+
+```powershell
+lake build EndKan.Kan.BeckChevalley
+lake build Scratch.MathlibKanBcExamples
+.\scripts\acceptance.ps1
+```
+
+## Staging artifacts
+
+- `scratch/mathlib-kan-bc/LEMMA_MAP.md`
+- `src/Scratch/MathlibKanBcExamples.lean` — `reflSquare` instance smoke test

lakefile.lean

@@ -37,4 +37,5 @@ lean_exe «test-runner» where
   supportInterpreter := true
 
 lean_lib Scratch where
-  roots := #[`Scratch.SliceIsoMin, `Scratch.MathlibEndBetaExamples, `Scratch.MathlibCoendBetaExamples]
+  roots := #[`Scratch.SliceIsoMin, `Scratch.MathlibEndBetaExamples, `Scratch.MathlibCoendBetaExamples,
+    `Scratch.MathlibFubiniExamples, `Scratch.MathlibKanBcExamples]

scratch/mathlib-fubini/LEMMA_MAP.md

@@ -0,0 +1,46 @@
+# Fubini — Mathlib upstream lemma map
+
+Staging for the **third** Mathlib extraction wave (see `docs/EXTRACTION_LEDGER.md` §5–§6).
+Source: `EndKan.Fubini.*`. Target Mathlib pin: `v4.31.0-rc1`.
+
+## Mathlib overlap
+
+Mathlib has `Limits.end_` / `Limits.coend` on curried profunctors but **no packaged
+nested product Fubini** swapping an end over `C × D` with ends over `C` at fixed `d`.
+
+## Status key
+
+- **ready** — kernel-checked, plausible Mathlib naming
+- **hypothesis** — needs explicit typeclass (extraction boundary on rc1)
+- **defer** — design issue or automation-only
+
+## End Fubini
+
+| Status | EndKan name | Local path | Proposed Mathlib path |
+|--------|-------------|------------|----------------------|
+| ready | `endSliceEmbed`, `endSlice` | `Fubini/Slice.lean` | `.../Ends/Fubini/Slice.lean` |
+| ready | `endInnerObj`, `endInnerπ`, `endInnerLift` | Slice | Fubini/Slice |
+| ready | `endInnerMap`, `endInnerMap_spec` | Slice | Fubini/Slice |
+| ready | `endSlice_cov_contr` | Slice | Fubini/Slice |
+| hypothesis | `AllEndSliceContrIso`, `endSliceOpCovIso` | Slice | documented boundary |
+| ready | `endOuterProfunctor` | `Fubini/Nested.lean` | `.../Ends/Fubini/Nested.lean` |
+| ready | `endFubiniIso`, `endFubiniIso_hom` | Nested | Fubini/Nested |
+| ready | `end_fubini_target` | `Fubini.lean` | Fubini API |
+| ready | `end_fubini_beta`, `end_fubini_π` | Fubini.lean | thin re-exports |
+| defer | `EndSliceJointMono` bootstrap | Slice | rc1 mutual `IsIso` blocked |
+
+## Coend Fubini
+
+| Status | EndKan name | Local path | Proposed Mathlib path |
+|--------|-------------|------------|----------------------|
+| ready | `coendSliceEmbed`, `coendSlice` | `Fubini/CoendSlice.lean` | `.../Coends/Fubini/Slice.lean` |
+| ready | `coendInnerMap`, `coendInnerDesc` | CoendSlice | Fubini/Slice |
+| ready | `coendSliceMid_*` | CoendSlice | mid-level API (not `ι ≫ Cov`) |
+| hypothesis | `CoendSliceContrIso` | CoendSlice | documented boundary |
+| ready | `coendFubiniIso` | `Fubini/NestedCoend.lean` | Fubini/Nested |
+| ready | `coend_fubini_target` | Fubini.lean | Fubini API |
+
+## Consumer example (not for Mathlib PR body)
+
+`EndKan.Fubini.Examples` — constant profunctor on `OneCat` discharges hypothesis
+classes via `allEndSliceContrIsoOfData` / `coendSliceContrIsoOfData`.

scratch/mathlib-fubini/MODULE_STRUCTURE.md

@@ -0,0 +1,51 @@
+# Draft Mathlib module structure — nested Fubini
+
+Proposed layout under `Mathlib/CategoryTheory/Limits/Shapes/`:
+
+```
+End/Fubini/
+  Slice.lean      -- endSliceEmbed, endInnerMap, wedge indexing
+  Nested.lean     -- endOuterProfunctor, endFubiniIso
+  Examples.lean   -- constant / representable instances (hypothesis discharge)
+Coend/Fubini/
+  Slice.lean
+  Nested.lean
+  Examples.lean
+```
+
+## PR sequencing (recommended)
+
+1. **Slice lemmas only** — embedding, inner end, `d`-action, `endSlice_cov_contr`
+2. **Nested iso** — `endFubiniIso` under explicit `AllEndSliceContrIso`-style class
+3. **Design issue** — unconditional contr-leg iso / remove hypothesis class
+
+## Namespace sketch (`End/Fubini/Slice.lean`)
+
+```lean
+namespace CategoryTheory.Limits
+
+variable {C D E : Type*} [Category C] [Category D] [Category E]
+
+abbrev EndIdx (C D : Type*) [Category C] [Category D] :=
+  Prod ((C × D)ᵒᵖ) (C × D)
+
+def endWedge (c : C) (d : D) : EndIdx C D := (op (c, d), c, d)
+
+def endSliceEmbed (d : D) : Cᵒᵖ × C ⥤ EndIdx C D := ...
+
+def endSlice (F : EndIdx C D ⥤ E) (d : D) : Cᵒᵖ × C ⥤ E := endSliceEmbed d ⋙ F
+
+-- inner end, endInnerMap, endSlice_cov_contr, ...
+
+end CategoryTheory.Limits
+```
+
+## Extraction boundary (document in Mathlib PR)
+
+On Lean 4.31-rc1, default `[IsIso (endSliceContrMap …)]` instances require a mutual
+fixpoint that the kernel rejects. Mathlib should either:
+
+- accept a typeclass `EndSliceContrIso` per profunctor, or
+- wait for a cov-only inner-map API that avoids bootstrap isos.
+
+EndKan documents both in `Slice.lean` `sliceIsoBootstrap` and `scratch/SliceIsoMin.lean`.

scratch/mathlib-fubini/README.md

@@ -0,0 +1,16 @@
+# Fubini extraction staging (upstream order #3)
+
+Nested product Fubini for ends and coends over `(C × D)ᵒᵖ × (C × D)` and
+`(C × D) × (C × D)ᵒᵖ`. See `docs/MATHLIB_PR_FUBINI.md` and `docs/EXTRACTION_LEDGER.md` §5–§6.
+
+**Not Mathlib-ready as a single PR today:** slice contr-leg isomorphisms require
+`AllEndSliceContrIso` / `CoendSliceContrIso` hypothesis classes on Lean `v4.31.0-rc1`
+(mutual `IsIso` bootstrap blocked). Package helper lemmas and a concrete constant
+example first; full unconditional Fubini is a follow-up design issue.
+
+## Local build
+
+```powershell
+lake build Scratch.MathlibFubiniExamples
+lake build EndKan.Fubini
+```

scratch/mathlib-kan-bc/LEMMA_MAP.md

@@ -0,0 +1,31 @@
+# Kan / Beck–Chevalley — Mathlib upstream map
+
+Staging for extraction waves **4–5** (`docs/EXTRACTION_LEDGER.md` §7, §10).
+
+## Kan extensions (mostly Mathlib already)
+
+| Status | EndKan name | Notes |
+|--------|-------------|-------|
+| alias | `Lan`, `Ran` | `pointwiseLeftKanExtension` / `pointwiseRightKanExtension` |
+| alias | `lan_obj_eq`, `ran_obj_eq` | Document in Mathlib docstrings |
+| defer | EndKan tactics | local automation |
+
+## Beck–Chevalley
+
+| Status | EndKan name | Mathlib-ready? | Notes |
+|--------|-------------|----------------|-------|
+| ready | `Square`, `reflSquare`, `beckChevalleyCompare` | API | Comparison morphism |
+| ready | `beckChevalleyIso`, `beckChevalleyPullback` | extraction | tactic keys |
+| proved | `reflSquare_beckChevalley` | under `[IsEquivalence K]` | `Hypotheses.lean` |
+| proved | `pullbackSquare_of_equivalence` | equivalence hypothesis | not bare pullback |
+| proved | `fullyFaithfulSquare_of_equivalence` | strong hypotheses | |
+| proved | `exactSquare_of_equivalence` | PES-style | |
+| boundary | `IsPullbackSquare.comma_pullback` | Prop placeholder | comma finality deferred |
+| ready | `beckChevalleySouth`, `beckChevalleyNorth` | staging aliases | `Hypotheses.lean` |
+| ready | `square_comm_whisker`, `refl_beckChevalleySouth_eq` | partial geometry | |
+
+## Recommended Mathlib sequence
+
+1. **Design issue:** Beck–Chevalley for comma squares (goals, naming, `compare_iso` field)
+2. **Small PR:** `lan_obj_eq` / structured-arrow documentation if missing
+3. **Later:** equivalence-based instances (mirror `Hypotheses.lean`)

scratch/mathlib-kan-bc/README.md

@@ -0,0 +1,13 @@
+# Kan extension and Beck–Chevalley staging (upstream order #4–#5)
+
+Pointwise Kan abbreviations and Beck–Chevalley comparison lemmas. The **first Mathlib
+contribution** here should be a **design issue** + minimal API, not a full comma-pullback proof.
+
+See `docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md` and `docs/EXTRACTION_LEDGER.md` §7, §10.
+
+## Local build
+
+```powershell
+lake build Scratch.MathlibKanBcExamples
+lake build EndKan.Kan.BeckChevalley
+```

scripts/acceptance.ps1

@@ -33,6 +33,14 @@ Invoke-Step "lake build Scratch.SliceIsoMin" {
     lake build Scratch.SliceIsoMin
 }
 
+Invoke-Step "lake build Scratch.MathlibFubiniExamples" {
+    lake build Scratch.MathlibFubiniExamples
+}
+
+Invoke-Step "lake build Scratch.MathlibKanBcExamples" {
+    lake build Scratch.MathlibKanBcExamples
+}
+
 Invoke-Step "lake env lean scratch/SliceIsoMin.lean" {
     lake env lean scratch/SliceIsoMin.lean
 }