Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(topology/algebra/infinite_sum): Extract none from a sum over option types #19150

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

feat(topology/algebra/infinite_sum): Extract none from a sum over option types #19150

wants to merge 2 commits into from

Conversation

dtumad
Copy link
Collaborator

@dtumad dtumad commented Jun 4, 2023 •
edited by eric-wieser

This PR gives lemmas for separating a sum over option α into the value at none plus a sum over α

Open in Gitpod

@dtumad dtumad added the awaiting-review The author would like community review of the PR label Jun 4, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 4, 2023
@jcommelin
Copy link
Member

I think you want s/some/sum/ in the PR title, right?

@eric-wieser eric-wieser changed the title feat(topology/algebra/infinite_sum): Extract none from a some over option types feat(topology/algebra/infinite_sum): Extract none from a sum over option types Jun 5, 2023
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 5, 2023
@dtumad
Copy link
Collaborator Author

dtumad commented Jun 6, 2023

I also added versions for sum types when adding the has_sum versions of lemmas, since it's very similar to the case of option, just combining lemmas about sums over set.range and subtype.

@dtumad dtumad added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 6, 2023
urkud
urkud reviewed Jun 21, 2023
View reviewed changes
src/topology/algebra/infinite_sum/basic.lean
@@ -164,6 +164,11 @@ begin
exact if_neg hb'
end

lemma has_sum_singleton (f : β → α) (b : β) : has_sum (f ∘ coe : ({b} : set β) → α) (f b) :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add it for a [unique] type, not just a singleton.

urkud
urkud reviewed Jun 21, 2023
View reviewed changes
src/topology/algebra/infinite_sum/basic.lean
@@ -313,6 +318,16 @@ lemma has_sum.compl_add {s : set β} (ha : has_sum (f ∘ coe : sᶜ → α) a)
has_sum f (a + b) :=
ha.add_is_compl is_compl_compl.symm hb

lemma has_sum.sum_t {f : β ⊕ γ → α} {a_inl a_inr : α} (h_inl : has_sum (f ∘ sum.inl) a_inl)
Copy link
Member

@urkud urkud Jun 21, 2023 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are two ways to state this lemma: starting with β ⊕ γ → α and starting with two functions and combining them using sum.elim. Please add the second version too (the proof should be by application of this version). I'm not sure about the naming convention for this kind of lemmas. sum_dom? I would ask on Zulip.

urkud
urkud reviewed Jun 21, 2023
View reviewed changes
src/topology/algebra/infinite_sum/basic.lean
has_sum.add_is_compl (set.is_compl_range_inl_range_inr)
(sum.inl_injective.has_sum_range_iff.2 h_inl) (sum.inr_injective.has_sum_range_iff.2 h_inr)

lemma has_sum.option {f : option β → α} {a_some : α} (hf : has_sum (f ∘ option.some) a_some) :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please make it protected.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, please add summable versions of your lemmas (with iff versions whenever we can apply summable.comp_injective).

@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 21, 2023
@semorrison semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@dtumad @jcommelin @urkud @eric-wieser @semorrison