Sort = Prop or Type

Stream: mathlib4

[Kevin Buzzard]

Eric W suggested that #14483 should be a product over a Sort not a Type, because the theorem in question is true in that generality. But the statement is a result about finprod and I reduce it to a question about Fintype which only works for types for some reason. I can prove the result for Props individually but is that the way to prove theorems for Sorts?

import Mathlib.GroupTheory.GroupAction.BigOperators
import Mathlib.Algebra.BigOperators.Finprod

theorem typey_smul_finprod {α β : Type*} [Monoid α] [CommMonoid β]
    [MulDistribMulAction α β]
    {γ : Type*} [Finite γ] {f : γ → β} (r : α) :
    r • ∏ᶠ x : γ, f x = ∏ᶠ x : γ, r • (f x) := by
  cases nonempty_fintype γ
  simp only [finprod_eq_prod_of_fintype, Finset.smul_prod]

theorem proppy_smul_finprod {α β : Type*} [Monoid α] [CommMonoid β]
    [MulDistribMulAction α β]
    {γ : Prop} [Finite γ] {f : γ → β} (r : α) :
    r • ∏ᶠ x : γ, f x = ∏ᶠ x : γ, r • (f x) := by
  cases em γ
  · aesop
  · case inr h =>
      simp [h, smul_one r]

theorem sorty_smul_finprod {α β : Type*} [Monoid α] [CommMonoid β]
    [MulDistribMulAction α β]
    {γ : Sort*} [Finite γ] {f : γ → β} (r : α) :
    r • ∏ᶠ x : γ, f x = ∏ᶠ x : γ, r • (f x) := by
  sorry -- now what?!

[Eric Wieser]

One option is:

theorem sorty_smul_finprod {α β : Type*} [Group α] [CommMonoid β]
    [MulDistribMulAction α β]
    {γ : Sort*}  {f : γ → β} (r : α) :
    r • ∏ᶠ x : γ, f x = ∏ᶠ x : γ, r • (f x) :=
   (MulDistribMulAction.toMulEquiv _ _).map_finprod _

[Eric Wieser]

Which trades [Monoid α] [Finite α] for [Group α]

[Eric Wieser]

But that's not really the answer to your question

[Eric Wieser]

Perhaps:

theorem smul_finprod {α β : Type*} [Monoid α] [CommMonoid β]
    [MulDistribMulAction α β]
    {γ : Sort*} {f : γ → β} (h : (f ∘ PLift.down).mulSupport.Finite) (r : α) :
    r • ∏ᶠ x : γ, f x = ∏ᶠ x : γ, r • (f x) :=
  (MulDistribMulAction.toMonoidHom _ _).map_finprod_plift _ h

[Eric Wieser]

Your lemma is then smul_finprod (Set.toFinite _)

[Yaël Dillies]

Also docs#PLift is sad that you forgot about it

[Kevin Buzzard]

I didn't forget about it, I just assumed it ate a Prop but looking now I see it eats a Sort

[Yaël Dillies]

Yes, I see its point as precisely allowing the kind of proof you're trying to do here

[Eric Wieser]

I couldn't see a way to directly use PLift here, the API for finprod didn't have the tool I wanted to use it

[Kevin Buzzard]

Is it not possible to write the recursor which says "if you've done it for Prop and for Type u, you've done it for Sort u"? docs#Sort.rec ? (edit: nope)

[Yakov Pechersky]

Sort isn't an inductive type

[Eric Wieser]

I don't think it's even possible to state what you're asking for; the motive would have to quantify over universes

[Yakov Pechersky]

And you can't condition on universe levels iiuc or selectively quantify over them

[Kevin Buzzard]

I spent some time on the tube trying to reconcile the confusion above with mathlib, which doesn't seem to have any such nonsense.

TL;DR: I'd like this:

import Mathlib.GroupTheory.GroupAction.BigOperators
import Mathlib.Algebra.BigOperators.Finprod

open Function

lemma sorty_finprod_eq_of_bijective {α β : Sort*} {M : Type*} [CommMonoid M] {f : α → M}
    {g : β → M} (e : α → β) (he₀ : Bijective e) (he₁ : ∀ (x : α), f x = g (e x)) :
    ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j := sorry

The details: my interpretation of Eric's comment above

Eric Wieser said:

I couldn't see a way to directly use PLift here, the API for finprod didn't have the tool I wanted to use it

was "the best way to do this is to actually make the right API for finprod", so I tried to figure this out. I think I got the first step right:

import Mathlib.GroupTheory.GroupAction.BigOperators
import Mathlib.Algebra.BigOperators.Finprod

variable {α β : Type*} {γ : Sort*} -- the game is to get the below working with Sort

variable [Monoid α] [CommMonoid β] [MulDistribMulAction α β]

-- a theorem which might be missing
theorem finprod_plift_up (f : PLift γ → β) :
    ∏ᶠ i : γ, f (PLift.up i) = ∏ᶠ j : PLift γ, f j := by
  sorry

-- a theorem which might be missing
theorem finprod_plift_down (f : γ → β) :
    ∏ᶠ j : PLift γ, f (PLift.down j) = ∏ᶠ i : γ, f i := by
  sorry

-- the theorem I want
theorem smul_finprod [Finite γ] {f : γ → β} (r : α) :
    r • ∏ᶠ x : γ, f x = ∏ᶠ x : γ, r • (f x) := by
  cases nonempty_fintype (PLift γ) -- seems to be the idiomatic approach
  rw [← finprod_plift_down, ← finprod_plift_down (fun x ↦ r • f x),
    finprod_eq_prod_of_fintype, finprod_eq_prod_of_fintype, Finset.smul_prod]

Now proving the two sorried theorems looks very easy: we have theorems like docs#PLift.up_bijective and docs#PLift.down_bijective, the equiv docs#Equiv.plift, and the usual lemmas like docs#finprod_eq_of_bijective and docs#finprod_comp etc etc saying that if two types biject then the products over them are equal. But they really do only apply to types! Are those latter two lemmas not formalised in the correct generality?

I tried changing the types to sorts in finprod_comp, and then Lean demanded that I changed the types to sorts in finprod_eq_of_bijective, but then I ran into trouble because the latter proof uses docs#finprod_mem_univ which uses Set which won't eat a Sort :-(

[Yury G. Kudryashov]

Is it (MulDistribMulAction.toMonoidHom α β).map_finprod_plift f (Set.to_finite _)?

[Eric Wieser]

Yes, that's what I wrote above