Skip to content

[Merged by Bors] - feat(Algebra): auxiliary lemmas for flatness over semirings#20265

Closed
alreadydone wants to merge 1 commit intomasterfrom
Semiring_Flat_aux
Closed

[Merged by Bors] - feat(Algebra): auxiliary lemmas for flatness over semirings#20265
alreadydone wants to merge 1 commit intomasterfrom
Semiring_Flat_aux

Conversation

@alreadydone
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone commented Dec 27, 2024

Open in Gitpod

@alreadydone alreadydone added the t-algebra Algebra (groups, rings, fields, etc) label Dec 27, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 27, 2024

PR summary bd84f8e34c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ congr
+ directSumRight_comp_rTensor
+ exists_fg_le_eq_rTensor_subtype
+ exists_fg_le_subset_range_rTensor_inclusion
+ exists_fg_le_subset_range_rTensor_subtype
+ lTensor_comp_cancelBaseChange
+ lmap
+ lmap_apply
+ lmap_injective
+ lmap_lof
+ mapRange_injective
+ of_equiv
+ small
+ tensorProduct_isLocalizedModule

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

@alreadydone alreadydone mentioned this pull request Dec 27, 2024
Closed
4 tasks
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jan 2, 2025

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 2, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 2, 2025
@alreadydone
feat(Algebra): auxiliary lemmas for flatness over semirings (#20265)
758574f
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 2, 2025

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

@mathlib-bors mathlib-bors bot changed the title feat(Algebra): auxiliary lemmas for flatness over semirings [Merged by Bors] - feat(Algebra): auxiliary lemmas for flatness over semirings Jan 2, 2025
@mathlib-bors mathlib-bors bot closed this Jan 2, 2025
@mathlib-bors mathlib-bors bot deleted the Semiring_Flat_aux branch January 2, 2025 11:43
@eric-wieser eric-wieser mentioned this pull request Mar 4, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Mar 5, 2025
@xyzw12345 @eric-wieser
feat(Algebra/DirectSum): getting a map between directsums by giving t…
6cd25d2 
…he map on components (#22354)

This PR defines the map obtained between `DirectSum`s by giving the component-wise mapping. More specifically, it creates a homomorphism `DirectSum.map f : (⨁ i, α i) →+ ⨁ i, β i` from the component-wise map `f : ∀(i : ι), α i →+ β i`. We also proved some basic properties of this function. This construction is expected to be used in things related to graded rings.

The linear version of this map was added already in #20265.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
imbrem pushed a commit that referenced this pull request Mar 6, 2025
@xyzw12345 @eric-wieser @imbrem
feat(Algebra/DirectSum): getting a map between directsums by giving t…
8e0fe13 
…he map on components (#22354)

This PR defines the map obtained between `DirectSum`s by giving the component-wise mapping. More specifically, it creates a homomorphism `DirectSum.map f : (⨁ i, α i) →+ ⨁ i, β i` from the component-wise map `f : ∀(i : ι), α i →+ β i`. We also proved some basic properties of this function. This construction is expected to be used in things related to graded rings.

The linear version of this map was added already in #20265.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@alreadydone @jcommelin