[Merged by Bors] - feat: LocallyConstant.piecewise'

[dagurtomas]

We define a variant of LocallyConstant.piecewise which defines a locally constant map on a subset given locally constant maps on two closed subsets covering it, that agree on the intersection.

• depends on: [Merged by Bors] - feat: two missing lemmas about restricting continuous maps #6616

Co-authored-by: Anatole Dedecker @ADedecker

---

[ADedecker]

What do you think of the following implementation?

noncomputable def piecewise' {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
    (h₂ : IsClosed C₂) (f₁ : LocallyConstant C₁ Z) (f₂ : LocallyConstant C₂ Z)
    [DecidablePred (· ∈ C₁)] (hf : ∀ x (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, hx.1⟩ = f₂ ⟨x, hx.2⟩) :
    LocallyConstant C₀ Z :=
  letI : ∀ j : C₀, Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) Iff.rfl
  piecewise (h₁.preimage continuous_subtype_val) (h₂.preimage continuous_subtype_val)
    (by simpa [eq_univ_iff_forall] using h₀)
    (f₁.comap (restrictPreimage C₁ ((↑) : C₀ → X)))
    (f₂.comap (restrictPreimage C₂ ((↑) : C₀ → X))) <| by
      rintro ⟨x, hx₀⟩ ⟨hx₁ : x ∈ C₁, hx₂ : x ∈ C₂⟩
      simp_rw [coe_comap_apply _ _ continuous_subtype_val.restrictPreimage]
      exact hf x ⟨hx₁, hx₂⟩

It requires changing f.toFun to f in the definition of piecewise (we always use the coercion instead of .toFun, so we should stick to it), as well as adding the following after Continuous.codRestrict:

theorem Continuous.restrict {f : α → β} {s : Set α} {t : Set β} (h1 : MapsTo f s t)
    (h2 : Continuous f) : Continuous (h1.restrict f s t) :=
  (h2.comp continuous_subtype_val).codRestrict _

theorem Continuous.restrictPreimage {f : α → β} {s : Set β} (h : Continuous f) :
    Continuous (s.restrictPreimage f) :=
  h.restrict _

I can see a few disadvantages:

• it's noncomputable (for bad reasons: Lean thinks it has to decide if some map is continuous in LocallyConstant.comap, but the map we use is always continuous)
• unfolding this definition will be a bit harder. A way to make sure that this doesn't cause any problem is to add enough lemmas so that unfolding is no longer necessary.

[dagurtomas]

I like it! I tried it on my Nöbeling branch and it works well by adding a simple lemma about applying piecewise'. I'll implement the changes and push them here.

[ADedecker]

Nice! By the way I opened #6616 with the two continuity lemmas on restrictions.

[ADedecker]

Also could you add a comment saying that the two piecewise constructions should be generalized to ContinuousMap? We don't have a nice way to make the translation (I think?) so it's not really useful for now, but just adding a TODO would be nice.

[dagurtomas]

Regarding the noncomputability: LocallyConstant.comap is only noncomputable because you can comap along noncontinuous maps for some reason, right? Does anyone want to do this? Can we maybe have both versions, where one is computable and only accepts continuous maps?

[dagurtomas]

Regarding the noncomputability: LocallyConstant.comap is only noncomputable because you can comap along noncontinuous maps for some reason, right? Does anyone want to do this? Can we maybe have both versions, where one is computable and only accepts continuous maps?

There is a comment about this next to the definition of comap

[ADedecker]

Finally let me just mention that I think these two constructions could be made way nicer if we developed some gluing API. I'll try to find some time to post my thoughts in greater detail about this on Zulip, but what I imagine would be a proposition expressing that a given topological space is the gluing of a family of topological space (as a property on, not as a construction) that would allow to do this kind of constructions more systematically.

[ADedecker]

Regarding the noncomputability: LocallyConstant.comap is only noncomputable because you can comap along noncontinuous maps for some reason, right? Does anyone want to do this? Can we maybe have both versions, where one is computable and only accepts continuous maps?

There is a comment about this next to the definition of comap

Indeed I think that would be a good idea, but maybe it's better to keep that aside for anther PR? Especially since I think we definitely want Johan's opinion on this kind of chance to see if it would mess with LTE.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: two missing lemmas about restricting continuous maps #6616
  By Dependent Issues (🤖). Happy coding!

[ADedecker]

Sorry for the delay. I made a few comments, but I think I shouldn't be the one merging that since I've made rather big suggestions (besides, I won't have time to take care of it in the near future). I'll un-assign myself, and you can ask for another review on Zulip after taking my review into account.

[riccardobrasca]

Thanks!

bors d+

[bors]

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[dagurtomas]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style