Some missing prod stuff

Stream: Is there code for X?

[Bernd Losert]

I search around and I couldn't find these guys:

import data.prod
import order.filter.basic

open filter
open_locale filter

variables {α β γ : Type*}

def prod.dup (x : α) : α × α := (x, x)

def prod.mk' (f : α → β) (g : α → γ) (x : α) : β × γ :=
prod.map f g (prod.dup x)

lemma prod.mk'_fst_snd : prod.mk' (@prod.fst α β) (@prod.snd α β) = id :=
begin
  funext,
  unfold prod.mk',
  unfold prod.dup,
  simp,
end

lemma filter.prod_map_fst_snd_eq {f : filter (α × β)} :
  f ≤ filter.map prod.fst f ×ᶠ map prod.snd f :=
begin
  unfold filter.prod,
  have hle₁ : f ≤ comap prod.fst (map prod.fst f), from le_comap_map,
  have hle₂ : f ≤ comap prod.snd (map prod.snd f), from le_comap_map,
  exact le_inf hle₁ hle₂,
end

Would anyone be against adding these to mathlib?

[Eric Wieser]

So mk' f g x = (f x, g x)?

[Eric Wieser]

That's similar to docs#linear_map.prod and docs#add_monoid_hom.prod, so should probably be called function.prod or pi.prod

[Adam Topaz]

Do we have docs#prod.lift ?

[Adam Topaz]

Your prod.mk is just prod.lift f g x, for a correctly defined prod.lift...

[Eric Wieser]

Doesn't lift usually go in the other direction? (in which case lift is just prod.rec)

[Adam Topaz]

No, look at e.g. docs#category_theory.limits.prod.lift

[Adam Topaz]

Do we even have docs#prod.rec ?

[Eric Wieser]

I think we want something like:

def pi.prod {α} {β γ : α → Type*}
  (f : Π a, β a) (g : Π a, γ a) (a) : β a × γ a :=
(f a, g a)

[Eric Wieser]

prod.rec is built-in like most .recs

[Eric Wieser]

I think lift goes the other way outside category_theory, eg docs#quotient.lift, docs#tensor_algebra.lift.

[Adam Topaz]

It is well know that quotient.lift should be called quotient.desc.

[Adam Topaz]

lift is a general word used for limits, and products are limits.

[Eric Wieser]

My understanding was that foo.lift was for building maps out of foo from "simpler" maps

[Eric Wieser]

But your proposed prod.lift builds a map into prod

[Eric Wieser]

Maybe that naming convention is bad, but that was the pattern I recall us having right now

[Adam Topaz]

I think of lift outside of the CT library more as "get the thing given by the universal property"

[Adam Topaz]

Whatever that universal property might be.

[Eric Wieser]

What's the universal property of prod? Isn't it prod.rec?

[Eric Wieser]

Or are there multiple universal properties?

[Reid Barton]

This is some weird type theory thing about "positive" and "negative" types.

[Reid Barton]

In category theory, the universal property of the product is that mapping into the product is the same as mapping into both factors.

[Bernd Losert]

The way I see it, since prod is a negative type, there should be a prod.corec that would be what I called prod.mk'.

[Eric Wieser]

I PR'd prod.mk' as pi.prod in #11877, and found some downstream foo.prods that could be reimplemented using pi.prod.

[Bernd Losert]

I will make a PR for filter.prod_map_fst_snd_eq then.

[Eric Wieser]

It should probably not have eq in the name since the statement is about le!

[Bernd Losert]

Yes, you're right.

[Bernd Losert]

I think mathlib is also missing α × (β × γ) ↔ (α × β) × γ. Or maybe this exists for pi, and I just can't find it.

[Kevin Buzzard]

Does that even typecheck? Can you give a #mwe ?

[Yaël Dillies]

docs#equiv.prod_assoc

[Bernd Losert]

Ah, nice. Thanks.

[Bernd Losert]

I was looking for this lemma

lemma filter.prod_map_rlassoc (f : filter α) (g : filter β) (h : filter γ) :
  map (equiv.prod_assoc α β γ).inv_fun (f ×ᶠ (g ×ᶠ h)) = (f ×ᶠ g) ×ᶠ h := sorry

but I could not find it. Would someone confirm that mathlib does have this? Also, proving this is turning into a challenge.

[Bernd Losert]

The set version of this lemma is also missing and I need it to prove the filter version above.

[Yaël Dillies]

I think we have neither.

[Yaël Dillies]

Is this some kind of general result about monads?

[Bernd Losert]

I don't think so. In my mind, these are just "lifted" versions of prod_assoc.

[Bernd Losert]

It's probably possible to get the set and filter versions of prod_assoc via applicative.seq?

[Yaël Dillies]

It's also true for finset. So I guess the criterion is a functor with a notion of product.

[Bernd Losert]

Monoidal functors perhaps? https://en.wikipedia.org/wiki/Monoidal_functor

[Bernd Losert]

Applicatives are basically what those are.

[Yaël Dillies]

Sounds like it.

[Kevin Buzzard]

@Bernd Losert I did half of it, the other half is just mutatis mutandis:

import tactic
import order.filter.basic

open_locale filter

open filter

variables (α β γ : Type*)

lemma filter.prod_map_rlassoc (f : filter α) (g : filter β) (h : filter γ) :
  map (equiv.prod_assoc α β γ).inv_fun (f ×ᶠ (g ×ᶠ h)) = (f ×ᶠ g) ×ᶠ h :=
begin
  ext U,
  simp only [mem_map, mem_prod_iff],
  split, -- can't see how to do it any other way
  { rintro ⟨tα, hα, tβγ, hβγ, hαβγ⟩,
    rw mem_prod_iff at hβγ,
    rcases hβγ with ⟨tβ, hβ, tγ, hγ, hβγ⟩,
    refine ⟨tα.prod tβ, _, tγ, hγ, _⟩,
    { rw mem_prod_iff,
      refine ⟨tα, hα, tβ, hβ, rfl.subset⟩ },
    { rintros ⟨⟨a, b⟩, c⟩ ⟨⟨ha, hb⟩, hc⟩,
      exact @hαβγ ⟨a, b, c⟩ ⟨ha, hβγ (⟨hb, hc⟩ : (b, c) ∈ tβ.prod tγ)⟩ } },
  { -- same again
    sorry }
end

[Kevin Buzzard]

I would love to see a proof using all that monadery stuff.

[Yaël Dillies]

I fear that the answer to the monadic stuff is that "It's what defines an associative functor" or however it's called and that what you're proving is precisely that set and filter are associative functors or however they are called.

[Kevin Buzzard]

If you're talking about applicative functors and your claim is true then no doubt this is just the sort of thing which people like Johannes Hoelzl and @Simon Hudon were doing years and years ago.

[Simon Hudon]

If you're using finset with applicative functions, indeed you need associativity and commutativity in order to map an effect to every element of the set. If you're looking at set and not finset, you need the operator of your applicative functor to be a big operator, applicable to arbitrary sets. I've never seen something like that though

[Patrick Massot]

Ok, you succeeded again to trick me into playing with filters.

import order.filter.bases

open_locale filter

open filter equiv

variables (α β γ : Type*)

lemma filter.has_basis.equiv {α : Type*} {ι ι' : Sort*} {p : ι → Prop} {s : ι → set α}
  {f : filter α} (h : f.has_basis p s) (e : ι' ≃ ι) : f.has_basis (p ∘ e) (s ∘ e) :=
⟨by simp [h.mem_iff, e.exists_congr_left]⟩

lemma filter.prod_map_rlassoc (f : filter α) (g : filter β) (h : filter γ) :
  map (prod_assoc α β γ) ((f ×ᶠ g) ×ᶠ h) = f ×ᶠ (g ×ᶠ h) :=
begin
  rw map_eq_comap_of_inverse (prod_assoc α β γ).self_comp_symm (prod_assoc α β γ).symm_comp_self,
  apply ((((basis_sets f).prod $ basis_sets g).prod $ basis_sets h).comap _).eq_of_same_basis,
  convert ((basis_sets f).prod (((basis_sets g)).prod (basis_sets h))).equiv (prod_assoc _ _ _) ;
  { ext, simp [and_assoc] },
end

Note that I modified slightly the statement since I didn't see the point of going against equiv.prod_assoc.

[Eric Wieser]

Does that first lemma generalize to surjective e?

[Patrick Massot]

Sure

[Patrick Massot]

I wrote this lemma very quickly since it's a complete tautology that is exactly what is needed here.

[Patrick Massot]

Do you mean the surjective case is already there?

[Patrick Massot]

Let's do it for Eric:

lemma filter.has_basis.comp_of_surjective {α : Type*} {ι ι' : Sort*} {p : ι → Prop} {s : ι → set α}
  {f : filter α} (h : f.has_basis p s) {g : ι' → ι} (hg : surjective g) :
  f.has_basis (p ∘ g) (s ∘ g) :=
⟨begin
  intros t,
  rw h.mem_iff,
  split,
  { rintros ⟨i, hi, ht⟩,
    rcases hg i with ⟨i', rfl⟩,
    exact ⟨i', hi, ht⟩ },
  { rintros ⟨i', hi', ht⟩,
    exact ⟨g i', hi', ht⟩ }
end⟩

lemma filter.has_basis.equiv {α : Type*} {ι ι' : Sort*} {p : ι → Prop} {s : ι → set α}
  {f : filter α} (h : f.has_basis p s) (e : ι' ≃ ι) : f.has_basis (p ∘ e) (s ∘ e) :=
h.comp_of_surjective e.surjective

[Patrick Massot]

Now the required lemma has a more complicated proof, but it looks shorter on screen :stuck_out_tongue_wink:

[Patrick Massot]

#12002

[Eric Wieser]

Well you didn't have to write it so long!

lemma has_basis.comp_of_surjective (h : l.has_basis p s) {g : ι' → ι} (hg : function.surjective g) :
  l.has_basis (p ∘ g) (s ∘ g) :=
⟨λ t, h.mem_iff.trans hg.exists⟩

[Eric Wieser]

(apologies, it was unkind of me to trick you into proving the surjective case without telling you that I had docs#function.surjective.exists in mind as the proof)

[Kevin Buzzard]

So in fact it's now a one-liner. I really like these kinds of questions, it's the community at its best.