[Merged by Bors] - feat: product of subalgebras by YaelDillies · Pull Request #20202 · leanprover-community/mathlib4

YaelDillies · 2024-12-23T15:40:44Z

From FLT

Co-authored-by: Andrew Yang

From FLT

github-actions · 2024-12-23T15:41:40Z

PR summary 5c22d73571

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Algebra.Subalgebra.Pi` (new file)	917

Declarations diff

+ mem_pi
+ pi
+ pi_mono
+ pi_toSubmodule
+ pi_top
- coe_copy
- coe_pi

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

eric-wieser · 2024-12-24T19:09:10Z

Mathlib/Algebra/Algebra/Subalgebra/Pi.lean

+  {t : Set ι} {s s₁ s₂ : ∀ i, Subalgebra R (S i)} {x : ∀ i, S i}
+
+/-- The product of subalgebras as a subalgebra. -/
+@[simps coe toSubsemiring]


Does this generate something in terms of Subsemiring.pi?

Subsemiring.pi doesn't exist!

Then this toSemiring lemma is probably pretty useless.

It does generate something which makes (Subalgebra.pi s t).toSubsemiring simplify further. I think it's better to have it than not

eric-wieser · 2024-12-24T19:09:58Z

Mathlib/Algebra/Algebra/Subalgebra/Pi.lean

+@[simp] lemma pi_toSubmodule : toSubmodule (pi t s) = .pi t fun i ↦ (s i).toSubmodule := rfl
+
+@[simp]
+lemma pi_top (t : Set ι) : pi t (fun i ↦ (⊤ : Subalgebra R (S i))) = ⊤ :=


Is the bot version true as well?

No, the bottom R-subalgebra is always the copy of R inside the algebra, and the copy of R inside ∀ i, S i is the diagonal of the product of the copies of R inside each S i.

Ruben-VandeVelde

maintainer merge

assuming @eric-wieser has no further comments

github-actions · 2025-01-10T13:30:52Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

jcommelin

Thanks 🎉

bors merge

From FLT Co-authored-by: Andrew Yang

mathlib-bors · 2025-01-10T19:41:38Z

Pull request successfully merged into master.

Build succeeded:

From FLT Co-authored-by: Andrew Yang

* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...

YaelDillies added 2 commits December 23, 2024 15:40

feat: product of subalgebras

f44d867

From FLT

mk_all

72a9f2f

YaelDillies added t-algebra Algebra (groups, rings, fields, etc) FLT part of the ongoing formalization of Fermat's Last Theorem labels Dec 23, 2024

eric-wieser reviewed Dec 24, 2024

View reviewed changes

YaelDillies added 2 commits December 25, 2024 11:57

fix

2d6de78

rename variables

5c22d73

Ruben-VandeVelde approved these changes Jan 10, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 10, 2025

jcommelin reviewed Jan 10, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Jan 10, 2025

mathlib-bors bot pushed a commit that referenced this pull request Jan 10, 2025

feat: product of subalgebras (#20202)

111b4c0

From FLT Co-authored-by: Andrew Yang

mathlib-bors bot changed the title ~~feat: product of subalgebras~~ [Merged by Bors] - feat: product of subalgebras Jan 10, 2025

mathlib-bors bot closed this Jan 10, 2025

mathlib-bors bot deleted the subalgebra_pi branch January 10, 2025 19:41

grunweg pushed a commit that referenced this pull request Jan 11, 2025

feat: product of subalgebras (#20202)

93dcbfd

From FLT Co-authored-by: Andrew Yang

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: product of subalgebras#20202

[Merged by Bors] - feat: product of subalgebras#20202
YaelDillies wants to merge 4 commits intomasterfrom
subalgebra_pi

YaelDillies commented Dec 23, 2024

Uh oh!

github-actions bot commented Dec 23, 2024 •

edited

Loading

Declarations diff

Uh oh!

eric-wieser Dec 24, 2024 •

edited

Loading

Uh oh!

YaelDillies Dec 24, 2024

Uh oh!

eric-wieser Dec 25, 2024

Uh oh!

YaelDillies Dec 26, 2024

Uh oh!

eric-wieser Dec 24, 2024

Uh oh!

YaelDillies Dec 25, 2024

Uh oh!

Ruben-VandeVelde left a comment

Uh oh!

github-actions bot commented Jan 10, 2025

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

YaelDillies commented Dec 23, 2024

Uh oh!

github-actions bot commented Dec 23, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5c22d73571

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser Dec 24, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Dec 24, 2024

Choose a reason for hiding this comment

Uh oh!

eric-wieser Dec 25, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Dec 26, 2024

Choose a reason for hiding this comment

Uh oh!

eric-wieser Dec 24, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Dec 25, 2024

Choose a reason for hiding this comment

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jan 10, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Dec 23, 2024 •

edited

Loading

eric-wieser Dec 24, 2024 •

edited

Loading