feat(AlgebraicTopology/SimplicialSet): MulStruct.nonempty

[joelriou]

In this PR, we show that for SSet.PtSimplex.MulStruct, it is possible to multiply two SSet.PtSimplex and that left inverses exist.

---

• depends on: feat(AlgebraicTopology/SimplicialSet/KanComplex): MulStruct.assoc #38216
• depends on: feat(AlgebraicTopology/SimplicialSet): more API for SSet.op #38664

[github-actions]

PR summary b71974e752

Import changes exceeding 2%

%	File
+9.47%	Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct	1003	1098	+95 (+9.47%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct	95

---

Declarations diff (regex)

+ RelStruct₀
+ assoc
+ assoc'
+ assocAux
+ exists_left_inverse
+ instance {X : SSet.{u}} [KanComplex X] : KanComplex X.op := by
+ isCompatible_α
+ map_eq_const_equiv₀
+ mulOneEqOfOneMulEq
+ mulOneEqSymm
+ mulOneEqTrans
+ nonempty
+ oneMulEqOfMulOneEq
+ oneMulEqSymm
+ oneMulEqTrans
+ opEquiv
+ opObjEquiv_symm_yonedaEquiv_const
+ opObjEquiv_yonedaEquiv_const
+ stdSimplex.yonedaEquiv_δ_comp
+ stdSimplex.yonedaEquiv_σ_comp
+ stdSimplex.δ_comp_yonedaEquiv_symm
+ stdSimplex.σ_comp_yonedaEquiv_symm
+ α
+ α_castSucc_castSucc_castSucc
+ α_castSucc_succ_succ
+ α_of_gt
+ α_of_lt
+ α_succ_succ_succ
+ δ_opObjEquiv
+ σ_opObjEquiv
++ equiv₀
++ op
++ unop

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 b71974e).

• +38 new declarations
• −0 removed declarations

+SSet.PtSimplex.MulStruct.assoc
+SSet.PtSimplex.MulStruct.assoc'
+SSet.PtSimplex.MulStruct.exists_left_inverse
+SSet.PtSimplex.MulStruct.mulOneEqOfOneMulEq
+SSet.PtSimplex.MulStruct.mulOneEqSymm
+SSet.PtSimplex.MulStruct.mulOneEqTrans
+SSet.PtSimplex.MulStruct.nonempty
+SSet.PtSimplex.MulStruct.oneMulEqOfMulOneEq
+SSet.PtSimplex.MulStruct.oneMulEqSymm
+SSet.PtSimplex.MulStruct.oneMulEqTrans
+SSet.PtSimplex.MulStruct.op
+SSet.PtSimplex.MulStruct.op_map
+SSet.PtSimplex.MulStruct.unop
+SSet.PtSimplex.MulStruct.unop_map
+SSet.PtSimplex.RelStruct.mk.congr_simp
+SSet.PtSimplex.RelStruct₀
+SSet.PtSimplex.RelStruct₀.equiv₀
+SSet.PtSimplex.equiv₀
+SSet.PtSimplex.equiv₀_apply
+SSet.PtSimplex.equiv₀_symm_apply_map
+SSet.PtSimplex.map_eq_const_equiv₀
+SSet.PtSimplex.op
+SSet.PtSimplex.opEquiv
+SSet.PtSimplex.opEquiv_apply_map
+SSet.PtSimplex.opEquiv_symm_apply_map
+SSet.PtSimplex.unop
+SSet.RelativeMorphism.mk.congr_simp
+SSet.boundary.hom_ext_iff
+SSet.instKanComplexOp
+SSet.opObjEquiv_symm_yonedaEquiv_const
+SSet.opObjEquiv_yonedaEquiv_const
+SSet.stdSimplex.yonedaEquiv_δ_comp
+SSet.stdSimplex.yonedaEquiv_σ_comp
+SSet.stdSimplex.δ_comp_yonedaEquiv_symm
+SSet.stdSimplex.σ_comp_yonedaEquiv_symm
+SSet.δ_opObjEquiv
+SSet.σ_opObjEquiv
+SimplexCategory.rev_map

---

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

Current number	Change	Type (strong)
4354	-12	backward.defeqAttrib.useBackward
6979	-7	backward.isDefEq.respectTransparency
3984	-3	backward.isDefEq.respectTransparency.types

No changes to weak technical debt.

Current commit b71974e752
Reference commit 9fb10993c1

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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplicialSet/KanComplex): MulStruct.assoc #38216
• feat(AlgebraicTopology/SimplicialSet): more API for SSet.op #38664
  By Dependent Issues (🤖). Happy coding!