feat(topology/constructions): distributivity of products over sums #1059
Conversation
|
Looks great. |
| @@ -444,6 +444,13 @@ calc (α × (β ⊕ γ)) ≃ ((β ⊕ γ) × α) : prod_comm _ _ | |||
| @[simp] theorem prod_sum_distrib_apply_right {α β γ} (a : α) (c : γ) : | |||
| prod_sum_distrib α β γ (a, sum.inr c) = sum.inr (a, c) := rfl | |||
|
|
|||
| def sigma_prod_distrib {ι : Type*} (α : ι → Type*) (β : Type*) : | |||
There was a problem hiding this comment.
Should we call this sigma_prod and also have prod_sigma?
There was a problem hiding this comment.
Usually distributivity lemmas have the equality the other way around. Then it will be consistent with sum_mul.
There was a problem hiding this comment.
@rwbarton What's your opinion on this issue?
There was a problem hiding this comment.
I wrote the equivalence this way because (although it's hard to tell in the case of Set/Type) the forward map is the one which exists in any category and even replacing - x β with any functor: colim F(A_i) -> F(colim A_i). You can sort of see this when I prove that this is a homeomorphism for topological spaces: the forward map (as defined here) is obviously continuous but to prove the reverse map is continuous it's easiest to show the forward map is open (after proving a bunch of stuff about open maps and sigma).
Of course it does not really matter in the end which way the equivalence points because it is an equivalence, but at least on paper I find it a useful habit to keep maps written in the "natural" direction.
There was a problem hiding this comment.
I did notice the existing sum_prod_distrib and prod_sum_distrib are written in the opposite direction. I don't really have a strong opinion about which way these equivalences go but I suppose for consistency they should all go the same way.
|
Let's get this merged @sgouezel @PatrickMassot |
|
Checking again, any comments from topology maintainers @sgouezel @PatrickMassot ? This looks good to me, except for the merge conflict -- let's get it in before there are more of those. |
| variables [topological_space α] [topological_space β] [topological_space γ] | ||
|
|
||
| /-- A open embedding is an embedding with open image. -/ | ||
| def open_embedding (f : α → β) : Prop := embedding f ∧ is_open (range f) |
There was a problem hiding this comment.
Given that we have is_open_map, I think is_open_embedding would be better. (I know it is impossible to have perfect coherence here, since we already have embedding and continuous, say -- but I think I would also prefer is_embedding, by the way).
There was a problem hiding this comment.
I copied open_embedding from the existing closed_embedding so for now I think this is the "most consistent" name. But we can certainly discuss what to do about is_ prefixes in general.
|
What is the status of this PR? |
|
I think we are waiting only for trivial decisions (fixing a docstring typo, and choosing consistent names). @rwbarton? |
Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
jcommelin
added
the
ready-to-merge
…eanprover-community#1059) * feat(topology/constructions): distributivity of products over sums * Update src/topology/maps.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Reverse direction of sigma_prod_distrib
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list