feat(Algebra/Module): presentation of the PiTensorProduct

[joelriou]

Given a presentation of a finite number of R-modules M i, we obtain a presentation of the module ⨂[R] i, M i.

---

• depends on: feat(LinearAlgebra): generators of pi tensor products #26464

This PR continues the work from #18527.

Original PR: #18527

[joelriou]

Comments from Original PR #18527

This section contains 1 comment(s) from the original PR, excluding bot comments.

---

@github-actions (2024-11-01 16:05 UTC):

PR summary 69d7fa46b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.PiTensorProduct	-879
Mathlib.LinearAlgebra.PiTensorProduct.Basic	879
Mathlib.LinearAlgebra.PiTensorProduct.Generators (new file)	956
Mathlib.LinearAlgebra.PiTensorProduct.Finite (new file)	958
Mathlib.Algebra.Module.Presentation.PiTensor (new file)	1000

---

Declarations diff

+ Nat.card_compl_add_card
+ Nat.card_singleton_compl
+ Presentation.piTensor
+ _root_.MultilinearMap.ext_of_span_eq_top
+ embedding
+ embedding_apply_of_neq
+ embedding_apply_self
+ eq_presInd_var
+ equivTensorPiTensorComplSingleton
+ equivTensorPiTensorComplSingleton_symm_tmul
+ equivTensorPiTensorComplSingleton_tprod
+ ext_of_span_eq_top
+ extendCompSingleton_restriction
+ extendComplSingleton
+ extendComplSingleton_of_neq
+ extendComplSingleton_self
+ finite
+ isPresentationCore_induction_step
+ isPresentation_induction_step
+ isPresentation_of_isEmpty
+ presInd
+ presInd_var
+ submodule_span_eq_top
+ sumSingletonComplEquiv
+ sumSingletonComplEquiv_inl
+ sumSingletonComplEquiv_inr
+++ piTensor

You can run this locally as follows

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

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

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

---

Increase in tech debt: (relative, absolute) = (7.00, 0.01)

Current number	Change	Type
915	7	erw

Current commit 69d7fa46b0
Reference commit 4a5bed5fc9

You can run this locally as

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

[github-actions]

PR summary 501992c195

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.PiTensorProduct	-894
Mathlib.Data.Set.ComplSingletonLift (new file)	143
Mathlib.LinearAlgebra.PiTensorProduct.Basic	894
Mathlib.LinearAlgebra.PiTensorProduct.Generators (new file)	971
Mathlib.Algebra.Module.Presentation.PiTensor (new file)	1017
Mathlib.LinearAlgebra.PiTensorProduct.Finite (new file)	1020

---

Declarations diff

+ Presentation.piTensor
+ _root_.MultilinearMap.ext_of_span_eq_top
+ card_compl_add_card
+ card_singleton_compl
+ complSingletonLift
+ complSingletonLift_of_neq
+ complSingletonLift_restriction
+ complSingletonLift_self
+ embedding
+ embedding_apply_of_neq
+ embedding_apply_self
+ eq_presInd_var
+ equivTensorPiTensorComplSingleton
+ equivTensorPiTensorComplSingleton_symm_tmul
+ equivTensorPiTensorComplSingleton_tprod
+ ext_of_span_eq_top
+ finite
+ isPresentationCore_induction_step
+ isPresentation_induction_step
+ isPresentation_of_isEmpty
+ presInd
+ presInd_var
+ submodule_span_eq_top
+ sumSingletonComplEquiv
+ sumSingletonComplEquiv_inl
+ sumSingletonComplEquiv_inr
+++ piTensor

You can run this locally as follows

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

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

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

---

Increase in tech debt: (relative, absolute) = (5.00, 0.01)

Current number	Change	Type
843	5	erw

Current commit 90465826b7
Reference commit 501992c195

You can run this locally as

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

---

note: file Mathlib/LinearAlgebra/PiTensorProduct.lean` was renamed to `Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(LinearAlgebra): generators of pi tensor products #26464
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.