[Merged by Bors] - feat(logic/equiv, topology/homeomorph): split a product at a coordinate #16210

alreadydone · 2022-08-23T04:40:51Z

Add equiv.pi_split_at and homeomorph.pi_split_at: for every "coordinate" i : α, the bijection/homeomorphism between a product Π j : α, β j of types/topological spaces and the binary product of the type/space β i at that coordinate and the product Π j : {j // j ≠ i}, β j over all other coordinates.
Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of @[simps] to generate lemmas in which type casts are automatically removed.

Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.

P.S. equiv.pi_split_at could alternatively be defined as

(equiv.pi_equiv_pi_subtype_prod _ β).trans $
  (equiv.Pi_subsingleton (λ j : {j // j = i}, β j) ⟨i, rfl⟩).prod_congr $ equiv.refl _

but it slows down decl post-processing of homeomorph.pi_split_at from 0.6-0.7s to ~3.0s, so I don't go for that.

j-loreaux · 2022-10-03T21:43:36Z

While you're at it, can you also provide the homeomorphism version of pi_equiv_pi_subtype_prod to complete the parallelism?

alreadydone · 2022-10-03T22:24:28Z

While you're at it, can you also provide the homeomorphism version of pi_equiv_pi_subtype_prod to complete the parallelism?

Sure; just pushed!

j-loreaux · 2022-10-04T14:26:23Z

maintainer merge

github-actions · 2022-10-04T14:26:41Z

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

dupuisf · 2022-10-04T14:27:32Z

bors r+

…te (#16210) + Add `equiv.pi_split_at` and `homeomorph.pi_split_at`: for every "coordinate" `i : α`, the bijection/homeomorphism between a product `Π j : α, β j` of types/topological spaces and the binary product of the type/space `β i` at that coordinate and the product `Π j : {j // j ≠ i}, β j` over all other coordinates. + Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of `@[simps]` to generate lemmas in which type casts are automatically removed. Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.

bors · 2022-10-04T16:27:20Z

Build failed (retrying...):

Run tests

…te (#16210) + Add `equiv.pi_split_at` and `homeomorph.pi_split_at`: for every "coordinate" `i : α`, the bijection/homeomorphism between a product `Π j : α, β j` of types/topological spaces and the binary product of the type/space `β i` at that coordinate and the product `Π j : {j // j ≠ i}, β j` over all other coordinates. + Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of `@[simps]` to generate lemmas in which type casts are automatically removed. Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.

bors · 2022-10-04T18:24:19Z

Build failed:

Run tests

j-loreaux · 2022-10-05T16:35:38Z

@alreadydone FYI: this build failed.

alreadydone · 2022-10-05T16:41:35Z

Thanks! Could #16812 be merged soon? It seems it's causing the failure.

alreadydone · 2022-10-06T14:33:35Z

CI succeeded again. Could anyone put it on the queue?

j-loreaux · 2022-10-06T15:07:28Z

maintainer merge

github-actions · 2022-10-06T15:07:43Z

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

semorrison · 2022-10-07T01:20:23Z

bors merge

…te (#16210) + Add `equiv.pi_split_at` and `homeomorph.pi_split_at`: for every "coordinate" `i : α`, the bijection/homeomorphism between a product `Π j : α, β j` of types/topological spaces and the binary product of the type/space `β i` at that coordinate and the product `Π j : {j // j ≠ i}, β j` over all other coordinates. + Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of `@[simps]` to generate lemmas in which type casts are automatically removed. Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.

bors · 2022-10-07T04:13:32Z

Build failed (retrying...):

Lint mathlib

…te (#16210) + Add `equiv.pi_split_at` and `homeomorph.pi_split_at`: for every "coordinate" `i : α`, the bijection/homeomorphism between a product `Π j : α, β j` of types/topological spaces and the binary product of the type/space `β i` at that coordinate and the product `Π j : {j // j ≠ i}, β j` over all other coordinates. + Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of `@[simps]` to generate lemmas in which type casts are automatically removed. Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.

bors · 2022-10-07T09:18:12Z

Build failed (retrying...):

Build mathlib

…te (#16210) + Add `equiv.pi_split_at` and `homeomorph.pi_split_at`: for every "coordinate" `i : α`, the bijection/homeomorphism between a product `Π j : α, β j` of types/topological spaces and the binary product of the type/space `β i` at that coordinate and the product `Π j : {j // j ≠ i}, β j` over all other coordinates. + Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of `@[simps]` to generate lemmas in which type casts are automatically removed. Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.

bors · 2022-10-08T00:19:42Z

Pull request successfully merged into master.

Build succeeded:

equiv/homeomorph.pi/fun_split_at

3c6c13a

alreadydone added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Aug 23, 2022

alreadydone mentioned this pull request Aug 23, 2022

[Merged by Bors] - feat(topology/homotopy/homotopy_group): group and comm_group instances for π_n #15681

Closed

1 task

satisfy unused_argument linter

d81caa5

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 28, 2022

j-loreaux self-assigned this Oct 3, 2022

alreadydone added 2 commits October 3, 2022 18:23

homeomorph.pi_equiv_pi_subtype_prod

99ef62d

Merge remote-tracking branch 'origin/master' into pi_split_at

db7d422

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 4, 2022

Merge remote-tracking branch 'origin/master' into pi_split_at

98b1e15

alreadydone added awaiting-review The author would like community review of the PR and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Oct 6, 2022

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 7, 2022

bors bot changed the title ~~feat(logic/equiv, topology/homeomorph): split a product at a coordinate~~ [Merged by Bors] - feat(logic/equiv, topology/homeomorph): split a product at a coordinate Oct 8, 2022

bors bot closed this Oct 8, 2022

bors bot deleted the pi_split_at branch October 8, 2022 00:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(logic/equiv, topology/homeomorph): split a product at a coordinate #16210

[Merged by Bors] - feat(logic/equiv, topology/homeomorph): split a product at a coordinate #16210

alreadydone commented Aug 23, 2022 •

edited

Loading

j-loreaux commented Oct 3, 2022

alreadydone commented Oct 3, 2022

j-loreaux commented Oct 4, 2022

github-actions bot commented Oct 4, 2022

dupuisf commented Oct 4, 2022

bors bot commented Oct 4, 2022

bors bot commented Oct 4, 2022

j-loreaux commented Oct 5, 2022

alreadydone commented Oct 5, 2022 •

edited

Loading

alreadydone commented Oct 6, 2022

j-loreaux commented Oct 6, 2022

github-actions bot commented Oct 6, 2022

semorrison commented Oct 7, 2022

bors bot commented Oct 7, 2022

bors bot commented Oct 7, 2022

bors bot commented Oct 8, 2022

[Merged by Bors] - feat(logic/equiv, topology/homeomorph): split a product at a coordinate #16210

[Merged by Bors] - feat(logic/equiv, topology/homeomorph): split a product at a coordinate #16210

Conversation

alreadydone commented Aug 23, 2022 • edited Loading

j-loreaux commented Oct 3, 2022

alreadydone commented Oct 3, 2022

j-loreaux commented Oct 4, 2022

github-actions bot commented Oct 4, 2022

dupuisf commented Oct 4, 2022

bors bot commented Oct 4, 2022

bors bot commented Oct 4, 2022

j-loreaux commented Oct 5, 2022

alreadydone commented Oct 5, 2022 • edited Loading

alreadydone commented Oct 6, 2022

j-loreaux commented Oct 6, 2022

github-actions bot commented Oct 6, 2022

semorrison commented Oct 7, 2022

bors bot commented Oct 7, 2022

bors bot commented Oct 7, 2022

bors bot commented Oct 8, 2022

alreadydone commented Aug 23, 2022 •

edited

Loading

alreadydone commented Oct 5, 2022 •

edited

Loading