feat(CategoryTheory/MorphismProperty): trivial bundles

[joelriou]

In a category C, we introduce a structure TrivialBundleWithFiber p F which records the fact that for p : E ⟶ B, there is a morphism r : E ⟶ F which allows to identify E to the binary product of B and F. The corresponding property of morphisms is trivialBundlesWithFiber F.

(In a certain distant future, in the case of a suitable convenient category of topological spaces, this will be used as part of the formalization of the model category structure on simplicial sets.)

From https://github.com/joelriou/topcat-model-category

---

[github-actions]

PR summary 78cb073b61

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.MorphismProperty.TrivialBundles (new file)	665

---

Declarations diff (regex)

+ BinaryCofan.IsColimit.exists_desc
+ BinaryFan.IsLimit.exists_lift
+ TrivialBundleWithFiber
+ chgFiber
+ exists_iso
+ ext
+ ext_iff
+ instance {ι : Type*} (W : ι → MorphismProperty C) [∀ i, (W i).IsStableUnderBaseChange] :
+ instance {ι : Type*} (W : ι → MorphismProperty C) [∀ i, (W i).IsStableUnderCobaseChange] :
+ isPullback
+ isPullback_of_isTerminal
+ isoOfIsTerminal
+ map
+ mem_trivialBundles_iff
+ ofIsTerminal
+ ofIso
+ pullback
+ trivialBundles
+ trivialBundles.of_isPullback_of_fac
+ trivialBundlesWithFiber
+ trivialBundlesWithFiber_le_trivialBundles
++ instance (F : C) : (trivialBundlesWithFiber F).IsStableUnderBaseChange

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 78cb073).

• +43 new declarations
• −0 removed declarations

+CategoryTheory.Limits.BinaryCofan.IsColimit.exists_desc
+CategoryTheory.Limits.BinaryFan.IsLimit.exists_lift
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.casesOn
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.chgFiber
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.chgFiber_r
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.ctorIdx
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.exists_iso
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.ext
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.ext_iff
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.isLimit
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.isPullback
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.isPullback_of_isTerminal
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.isoOfIsTerminal
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.isoOfIsTerminal_hom
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.map
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.map_r
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.mk
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.mk.inj
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.mk.injEq
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.mk.noConfusion
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.mk.sizeOf_spec
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.noConfusion
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.noConfusionType
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.ofIsTerminal
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.ofIsTerminal_r
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.ofIso
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.ofIso_r
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.pullback
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.pullback_r
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.r
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.rec
+CategoryTheory.MorphismProperty.TrivialBundleWithFiber.recOn
+CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeISup
+CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTrivialBundles
+CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTrivialBundlesWithFiber
+CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTrivialBundlesWithFiber_1
+CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeISup
+CategoryTheory.MorphismProperty.mem_trivialBundles_iff
+CategoryTheory.MorphismProperty.trivialBundles
+CategoryTheory.MorphismProperty.trivialBundles.of_isPullback_of_fac
+CategoryTheory.MorphismProperty.trivialBundlesWithFiber
+CategoryTheory.MorphismProperty.trivialBundlesWithFiber_le_trivialBundles

---

Decrease in strong tech debt: (relative, absolute) = (0.51, 0.00)

Current number	Change	Type (strong)
497	-1	erw
4532	6	backward.defeqAttrib.useBackward
5614	-3	backward.isDefEq.respectTransparency

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5011	1	exposed public sections

Current commit 78cb073b61
Reference commit 14c4b77b0c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).