From cd58728bf72d043497286ccc39063bc71e56f564 Mon Sep 17 00:00:00 2001 From: fraware Date: Tue, 16 Jun 2026 08:43:12 -0700 Subject: [PATCH] Add Fubini and Kan/BC Mathlib extraction staging packages. Upstream order steps 3-5: buildable scratch examples, PR briefs, ledger updates, and acceptance gates for nested Fubini and Beck-Chevalley smoke tests. --- docs/EXTRACTION_LEDGER.md | 10 +++ docs/MATHLIB_PR_FUBINI.md | 73 ++++++++++++++++++++++ docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md | 67 ++++++++++++++++++++ lakefile.lean | 3 +- scratch/mathlib-fubini/LEMMA_MAP.md | 46 ++++++++++++++ scratch/mathlib-fubini/MODULE_STRUCTURE.md | 51 +++++++++++++++ scratch/mathlib-fubini/README.md | 16 +++++ scratch/mathlib-kan-bc/LEMMA_MAP.md | 31 +++++++++ scratch/mathlib-kan-bc/README.md | 13 ++++ scripts/acceptance.ps1 | 8 +++ src/Scratch/MathlibFubiniExamples.lean | 65 +++++++++++++++++++ src/Scratch/MathlibKanBcExamples.lean | 49 +++++++++++++++ 12 files changed, 431 insertions(+), 1 deletion(-) create mode 100644 docs/MATHLIB_PR_FUBINI.md create mode 100644 docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md create mode 100644 scratch/mathlib-fubini/LEMMA_MAP.md create mode 100644 scratch/mathlib-fubini/MODULE_STRUCTURE.md create mode 100644 scratch/mathlib-fubini/README.md create mode 100644 scratch/mathlib-kan-bc/LEMMA_MAP.md create mode 100644 scratch/mathlib-kan-bc/README.md create mode 100644 src/Scratch/MathlibFubiniExamples.lean create mode 100644 src/Scratch/MathlibKanBcExamples.lean diff --git a/docs/EXTRACTION_LEDGER.md b/docs/EXTRACTION_LEDGER.md index b22e2d3..fa997b6 100644 --- a/docs/EXTRACTION_LEDGER.md +++ b/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 diff --git a/docs/MATHLIB_PR_FUBINI.md b/docs/MATHLIB_PR_FUBINI.md new file mode 100644 index 0000000..697f4f9 --- /dev/null +++ b/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 diff --git a/docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md b/docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md new file mode 100644 index 0000000..3ea91eb --- /dev/null +++ b/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 diff --git a/lakefile.lean b/lakefile.lean index 24e84e8..2df7760 100644 --- a/lakefile.lean +++ b/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] diff --git a/scratch/mathlib-fubini/LEMMA_MAP.md b/scratch/mathlib-fubini/LEMMA_MAP.md new file mode 100644 index 0000000..2ff66fd --- /dev/null +++ b/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`. diff --git a/scratch/mathlib-fubini/MODULE_STRUCTURE.md b/scratch/mathlib-fubini/MODULE_STRUCTURE.md new file mode 100644 index 0000000..9af2f68 --- /dev/null +++ b/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`. diff --git a/scratch/mathlib-fubini/README.md b/scratch/mathlib-fubini/README.md new file mode 100644 index 0000000..18b56c4 --- /dev/null +++ b/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 +``` diff --git a/scratch/mathlib-kan-bc/LEMMA_MAP.md b/scratch/mathlib-kan-bc/LEMMA_MAP.md new file mode 100644 index 0000000..0f80340 --- /dev/null +++ b/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`) diff --git a/scratch/mathlib-kan-bc/README.md b/scratch/mathlib-kan-bc/README.md new file mode 100644 index 0000000..3ae8559 --- /dev/null +++ b/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 +``` diff --git a/scripts/acceptance.ps1 b/scripts/acceptance.ps1 index 4c2963a..9bd1778 100644 --- a/scripts/acceptance.ps1 +++ b/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 } diff --git a/src/Scratch/MathlibFubiniExamples.lean b/src/Scratch/MathlibFubiniExamples.lean new file mode 100644 index 0000000..74e7314 --- /dev/null +++ b/src/Scratch/MathlibFubiniExamples.lean @@ -0,0 +1,65 @@ +import EndKan.Fubini +import EndKan.Fubini.Examples + +/-! +# Fubini examples (Mathlib extraction staging) + +Concrete nested Fubini on constant profunctors (`OneCat`). Demonstrates the +hypothesis-class consumer path documented in `scratch/mathlib-fubini/LEMMA_MAP.md`. + +No tactics. When porting to Mathlib, replace `EndKan.Fubini` with +`Limits.endFubini` / `Limits.coendFubini` per `MODULE_STRUCTURE.md`. +-/ + +namespace Scratch.MathlibFubiniExamples + +open CategoryTheory +open Opposite +open scoped Prod +open EndKan.Fubini +open EndKan.Fubini.Examples + +universe u v + +variable {E : Type u} [Category.{v, u} E] + +section ConstantEnd + +variable (X : E) + +variable [Limits.HasEnd (EndKan.End.endBifunctor (endConstProfunctor X))] +variable [∀ d, Limits.HasEnd (EndKan.End.endBifunctor (endSlice (endConstProfunctor X) d))] +variable [∀ d, Epi (endInnerLift (endConstProfunctor X) d)] +variable [Limits.HasEnd (EndKan.End.endBifunctor (endOuterProfunctor (endConstProfunctor X)))] + +/-- Nested end Fubini for a constant profunctor: `EndObj F ≅ endNestedObj F`. -/ +noncomputable def constant_end_fubini_iso : + EndKan.End.EndObj (endConstProfunctor X) ≅ endNestedObj (endConstProfunctor X) := + endFubiniIso (endConstProfunctor X) + +/-- Target packaging: nested end Fubini holds for constant profunctors. -/ +theorem constant_end_fubini_target : EndFubiniTarget (endConstProfunctor X) := + end_fubini_target (F := endConstProfunctor X) + +end ConstantEnd + +section ConstantCoend + +variable (X : E) + +variable [Limits.HasCoend (EndKan.Coend.coendBifunctor (coendConstProfunctor X))] +variable [∀ d, Limits.HasCoend (EndKan.Coend.coendBifunctor (coendSlice (coendConstProfunctor X) d))] +variable [∀ d, Mono (coendInnerDesc (coendConstProfunctor X) d)] +variable [Limits.HasCoend (EndKan.Coend.coendBifunctor (coendOuterProfunctor (coendConstProfunctor X)))] + +/-- Nested coend Fubini for a constant profunctor. -/ +noncomputable def constant_coend_fubini_iso : + EndKan.Coend.CoendObj (coendConstProfunctor X) ≅ coendNestedObj (coendConstProfunctor X) := + coendFubiniIso (coendConstProfunctor X) + +theorem constant_coend_fubini_target : CoendFubiniTarget (coendConstProfunctor X) := + coend_fubini_target (F := coendConstProfunctor X) + +end ConstantCoend + +end Scratch.MathlibFubiniExamples diff --git a/src/Scratch/MathlibKanBcExamples.lean b/src/Scratch/MathlibKanBcExamples.lean new file mode 100644 index 0000000..259d5e7 --- /dev/null +++ b/src/Scratch/MathlibKanBcExamples.lean @@ -0,0 +1,49 @@ +import EndKan.Kan.BeckChevalley +import EndKan.Kan.BeckChevalley.Hypotheses + +/-! +# Kan / Beck–Chevalley examples (Mathlib extraction staging) + +Abstract smoke tests for the comparison API under equivalence hypotheses. +No tactics. + +Staging: `scratch/mathlib-kan-bc/`, `docs/MATHLIB_PR_KAN_BECKCHEVALLEY.md`. +-/ + +namespace Scratch.MathlibKanBcExamples + +open CategoryTheory +open CategoryTheory.Functor +open CategoryTheory.Limits +open EndKan.Kan +open EndKan.Kan.BeckChevalley + +universe u v + +variable {C D E B : Type u} [Category.{v, u} C] [Category.{v, u} D] [Category.{v, u} E] + [Category.{v, u} B] +variable {H : Type u} [Category.{v, u} H] +variable (K : C ⥤ D) (M : D ⥤ B) [IsEquivalence K] + +/-- Reflexive square carries a Beck–Chevalley instance when `K` is an equivalence. -/ +theorem refl_square_beck_chevalley : BeckChevalley (reflSquare K M) := + inferInstance + +/-- Comparison morphism is an isomorphism on the reflexive square. -/ +theorem refl_square_compare_iso (F : B ⥤ H) + [HasPointwiseLeftKanExtension K (K ⋙ M ⋙ F)] : + IsIso (beckChevalleyCompare (reflSquare K M) F) := + beckChevalleyIso (reflSquare K M) F + +section SquareComm + +variable {K : C ⥤ D} {M : D ⥤ B} + +/-- South leg of the comma square matches whiskering the commutative datum. -/ +theorem square_comm_whisker_example (L : C ⥤ E) (N : E ⥤ B) (S : Square K L M N) (F : B ⥤ H) : + L ⋙ N ⋙ F = K ⋙ M ⋙ F := + square_comm_whisker S F + +end SquareComm + +end Scratch.MathlibKanBcExamples