normal form for pullback of Inf of topologies

Stream: mathlib4

[Kevin Buzzard]

We have docs#induced_iInf, tagged @[simp], meaning that the simp normal form for induced g (⨅ i, t i) is ⨅ i, induced g (t i).

We apparently have no such lemma for sInf though:

import Mathlib.Topology.Order

variable {α β : Type*} {g : β → α}

/-
@[simp]
theorem induced_iInf {ι : Sort w} {t : ι → TopologicalSpace α} :
    (⨅ i, t i).induced g = ⨅ i, (t i).induced g := ...
-/

open TopologicalSpace

example {ι : Sort*} {t : ι → TopologicalSpace α} :
    induced g (⨅ i, t i) = ⊥ := by
  simp
  -- ⊢ ⨅ i, induced g (t i) = ⊥
  sorry


-- no corresponding lemma for sInf though

example {s : Set (TopologicalSpace α)} :
    induced g (sInf s) = ⊥ := by
  simp -- simp made no progress

The proof of induced_iInf is (gc_coinduced_induced g).u_iInf, and the analogous u_sInf lemma docs#GaloisConnection.u_sInf would rewrite induced g (sInf s) to ⨅ a ∈ s, induced g a. In the application this came up with, I wanted the answer to be sInf ((induced g) '' s). Whether or not this is the simp normal form doesn't really bother me, but what bothers me is that I need to prove induced_sInf but right now I don't know whether it should say

theorem induced_sInf {s : Set (TopologicalSpace α)} :
    induced g (sInf s) = sInf ((induced g) '' s) := by
  rw [sInf_eq_iInf', sInf_image', induced_iInf]

or

theorem induced_sInf' {s : Set (TopologicalSpace α)} :
    induced g (sInf s) = ⨅ a ∈ s, induced g a := by
  rw [(gc_coinduced_induced g).u_sInf]

and I also don't know whether it should be @[simp] or not. This was brought up here (which was my application) and I guess this is the question which is blocking progress here. Does anyone have an opinion on this? @Eric Wieser or @Yury G. Kudryashov maybe?

[Yaël Dillies]

The ⨅ a ∈ s, _ spelling is the preferred one

[Eric Wieser]

My argument for why we should prefer the sInf (f '' s) spelling is that we can also uses it in conditionally-complete lattices; so a more universally-applicable rule is "use sInf on the RHS if you used it on the LHS".

[Floris van Doorn]

Good point. I also like the spelling ⨅ a ∈ s, _ better myself, but it's a footgun in conditionally-complete lattices.

[Kevin Buzzard]

Eric Wieser said:

My argument for why we should prefer the sInf (f '' s) spelling is that we can also uses it in conditionally-complete lattices; so a more universally-applicable rule is "use sInf on the RHS if you used it on the LHS".

But this is a question specifically about topological spaces, which are a complete lattice. Does this make any difference here?

I really don't have an opinion on this stuff, I just thought I could try and make progress with #16895 by figuring out what I'm supposed to be doing on this point.

[Matthew Ballard]

Since you are keying off docs#TopologicalSpace.induced, I think it is fine as a simp lemma here.

[Kevin Buzzard]

But which one?

[Matthew Ballard]

The former

[Matthew Ballard]

You could even have both with different priorities

[Matthew Ballard]

Clarification: both means the former and a more generic sInf one

[Eric Wieser]

Kevin Buzzard said:

I really don't have an opinion on this stuff, I just thought I could try and make progress with #16895 by figuring out what I'm supposed to be doing on this point.

I think probably we can make an arbitrary decision in that PR, and clean up later if we decide on a clearer convention.