[Merged by Bors] - refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank #22902

xroblot · 2025-03-13T17:30:06Z

Many results using Smith Normal Form for ideals of a finite free ring over a PID are also true in the case of submodules of full rank.

Therefore we generalize the existing proofs to this case (usually the proofs work almost as is) and prove the corresponding results for submodules of full rank in two new files:

LinearAlgebra.FreeModule.Finite.Quotient: we prove in particular that for M a free finite module over a PID R and a submodule N of M of same rank, we have

(M ⧸ N) ≃ₗ[R] Π i, R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R)

LinearAlgebra.FreeModule.Finite.CardQuotient: we prove in particular that if M is a free finite ℤ-module of basis b and N is a submodule of basis bN of the same dimension, then

(b.det ((↑) ∘ bN)).natAbs = Nat.card (M ⧸ N)

The original proofs about ideals are deduced as consequences of the generalized proofs.

github-actions · 2025-03-13T17:31:08Z

PR summary fd99444ffe

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
21 files `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Ideal.Norm.AbsNorm`	2
`Mathlib.LinearAlgebra.FreeModule.Finite.Quotient` (new file)	1340
`Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient` (new file)	1403

Declarations diff

+ AddSubgroup.natAbs_det_basis_change
+ Ideal.finrank_eq_finrank
+ Submodule.exists_smith_normal_form_of_rank_eq
+ Submodule.natAbs_det_basis_change
+ Submodule.natAbs_det_equiv
+ Submodule.smithNormalFormBotBasis
+ Submodule.smithNormalFormBotBasis_def
+ Submodule.smithNormalFormCoeffs
+ Submodule.smithNormalFormCoeffs_ne_zero
+ Submodule.smithNormalFormOfRankEq
+ Submodule.smithNormalFormTopBasis
+ finrank_quotient_eq_sum
+ fintypeQuotientOfFreeOfRankEq
+ quotientEquivDirectSum
+ quotientEquivPiSpan
+ quotientEquivPiZMod

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.

No changes to technical debt.

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

erdOne · 2025-03-13T18:20:32Z

Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean

+theorem Submodule.natAbs_det_basis_change {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ M)
+    (N : Submodule ℤ M) (bN : Basis ι ℤ N) :
+    (b.det ((↑) ∘ bN)).natAbs = Nat.card (M ⧸ N) := by
+  let e := b.equiv bN (Equiv.refl _)
+  calc
+    (b.det (N.subtype ∘ bN)).natAbs = (LinearMap.det (N.subtype ∘ₗ (e : M →ₗ[ℤ] N))).natAbs := by
+      rw [Basis.det_comp_basis]
+    _ = _ := natAbs_det_equiv N e


Can you provide a variant:

{E : Type*} [AddCommGroup E] (N : AddSubgroup E) {ι : Type*} [DecidableEq ι] [Fintype ι] (bN : Basis ι ℤ N) (bE : Basis ι ℤ E) : N.index = (bE.det (bN ·)).natAbs

Thanks!

I also need

{E : Type*} [AddCommGroup E] [Module ℚ E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type*} [DecidableEq ι] [Fintype ι] (b₁ b₂ : Basis ι ℚ E) (h₁ : L₁ = .closure (Set.range b₁)) (h₂ : L₂ = .closure (Set.range b₂)) : L₁.relindex L₂ = |b₂.det b₁| := by

But I think this is too much work and I'm happy to add this myself after this PR is merged.

The first one is easy and I added it. The second one is more work indeed and somehow I think it would make more sense to state in terms of ZLattice over ℚ.

Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean

jcommelin · 2025-03-14T07:16:03Z

Mathlib/LinearAlgebra/FreeModule/Finite/Quotient.lean

+/-- A submodule of full rank of a free finite `ℤ`-module has a finite quotient.
+
+Can't be an instance because of the side condition and more importantly,
+because the choice of `Fintype` instance is non-canonical.


But you could phrase the conclusion as Finite (M ⧸ N) instead, right?

Sure, I just copied the original statement of Ideal.fintypeQuotientOfFreeOfNeBot. So I guess it would make more sense to change both of them. In which case, should I do it in this PR or maybe it's better to do that in a new PR?

A new PR is fine with me.

Mathlib/LinearAlgebra/FreeModule/PID.lean

jcommelin · 2025-03-14T10:49:24Z

Thanks 🎉

bors merge

…ank (#22902) Many results using Smith Normal Form for ideals of a finite free ring over a PID are also true in the case of submodules of full rank. Therefore we generalize the existing proofs to this case (usually the proofs work almost as is) and prove the corresponding results for submodules of full rank in two new files: - `LinearAlgebra.FreeModule.Finite.Quotient`: we prove in particular that for `M` a free finite module over a PID `R` and a submodule `N` of `M` of same rank, we have ```lean (M ⧸ N) ≃ₗ[R] Π i, R ⧸ Ideal.span ({smithNormalFormCoeffs b h i} : Set R) ``` - `LinearAlgebra.FreeModule.Finite.CardQuotient`: we prove in particular that if `M` is a free finite `ℤ`-module of basis `b` and `N` is a submodule of basis `bN` of the same dimension, then ```lean (b.det ((↑) ∘ bN)).natAbs = Nat.card (M ⧸ N) ``` The original proofs about ideals are deduced as consequences of the generalized proofs.

mathlib-bors · 2025-03-14T11:01:22Z

Pull request successfully merged into master.

Build succeeded:

As discussed [here](#22902 (comment))

…vProdLpPiLp` (#22993) * feat: scalar tower instances for quotients (#22951) We already have the `SMulCommClass` and `IsScalarTower` versions for `RingQuot`; this develops them for `Con` and `RingCon`, with the eventual aim of replacing `RingQuot` with `RingCon.Quotient`. * chore(Order/Group/Abs): use `@[to_additive]` (#22468) * feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843) This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map. * docs(Data/Real/EReal): fix capitalization error (#22943) Changes `Ereal` to `EReal` in the module docstring for `Data/Real/EReal`. * chore(Ideal/Quotient): change `Fintype` to `Finite` (#22947) As discussed [here](#22902 (comment)) * feat: add `norm_num` extensions for factorials (#8832) Add `norm_num` extensions to evaluate `Nat.factorial`, `Nat.ascFactorial` and `Nat.descFactorial`. Co-authored-by: Eric Wieser <[email protected]> * perf(CategoryTheory/Limits/Shapes): reorder instance arguments (#22968) This PR is in the same spirit as #22953. The problem is that some instances about category theoretical limits have silly side conditions that end up searching through the whole algebraic type class hierarchy. This PR attempts to keep the type class search limited to category theoretical type classes. * feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940) * feat: API for continuous extension of meromorphic functions (#22867) Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/API.20for.20continuous.20extension.20of.20meromorphic.20functions). More material will be provided in upcoming PRs. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. * feat(Data/Complex/Trigonometric): closer upper bound for cos 1 (#22945) cos 1 is approximately 0.5403..., so this bound is fairly tight. Co-authored-by: Vlad Tsyrklevich <[email protected]> * chore: move `List.Lex` lemmas out of the `List.Lex` namespace (#22935) This better matches the naming convention. * working on it. * Added sup_disjSum and inf_disjSum. * Finished one branch. * Finished proof. --------- Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Yury G. Kudryashov <[email protected]> Co-authored-by: Scott Carnahan <[email protected]> Co-authored-by: plp127 <[email protected]> Co-authored-by: Xavier Roblot <[email protected]> Co-authored-by: Sebastian Zimmer <[email protected]> Co-authored-by: JovanGerb <[email protected]> Co-authored-by: Stefan Kebekus <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>

1st commit

838dedf

xroblot changed the title ~~refactor(FreeModu;e/~~ refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank Mar 13, 2025

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 13, 2025

clean up

950fef1

erdOne reviewed Mar 13, 2025

View reviewed changes

xroblot added 3 commits March 13, 2025 22:12

Fix incorrect shake

f79d4df

AddSubgroup version

de6c58f

typos

ad9f038

jcommelin reviewed Mar 14, 2025

View reviewed changes

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 14, 2025

review

fd99444

jcommelin removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 14, 2025

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Mar 14, 2025

mathlib-bors bot changed the title ~~refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank~~ [Merged by Bors] - refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank Mar 14, 2025

mathlib-bors bot closed this Mar 14, 2025

mathlib-bors bot deleted the xfr-refactor_idealquo branch March 14, 2025 11:01

xroblot mentioned this pull request Mar 15, 2025

[Merged by Bors] - chore(Ideal/Quotient): change Fintype to Finite #22947

Closed

mathlib-bors bot pushed a commit that referenced this pull request Mar 15, 2025

chore(Ideal/Quotient): change Fintype to Finite (#22947)

14bdbbd

As discussed [here](#22902 (comment))

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank #22902

[Merged by Bors] - refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank #22902

xroblot commented Mar 13, 2025 •

edited

Loading

github-actions bot commented Mar 13, 2025 •

edited

Loading

Declarations diff

erdOne Mar 13, 2025

erdOne Mar 13, 2025

xroblot Mar 13, 2025

jcommelin Mar 14, 2025

xroblot Mar 14, 2025

jcommelin Mar 14, 2025

jcommelin commented Mar 14, 2025

mathlib-bors bot commented Mar 14, 2025

[Merged by Bors] - refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank #22902

[Merged by Bors] - refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank #22902

Conversation

xroblot commented Mar 13, 2025 • edited Loading

github-actions bot commented Mar 13, 2025 • edited Loading

PR summary fd99444ffe

Import changes for modified files

Declarations diff

erdOne Mar 13, 2025

Choose a reason for hiding this comment

erdOne Mar 13, 2025

Choose a reason for hiding this comment

xroblot Mar 13, 2025

Choose a reason for hiding this comment

jcommelin Mar 14, 2025

Choose a reason for hiding this comment

xroblot Mar 14, 2025

Choose a reason for hiding this comment

jcommelin Mar 14, 2025

Choose a reason for hiding this comment

jcommelin commented Mar 14, 2025

mathlib-bors bot commented Mar 14, 2025

xroblot commented Mar 13, 2025 •

edited

Loading

github-actions bot commented Mar 13, 2025 •

edited

Loading