quotient.lift_on_family

Stream: Is there code for X?

[Adam Topaz]

Do we have some construction of the following form? (generalizing lift_on_2, lift_on_3, etc.):

import data.setoid.basic

variables {ι : Type*} {X : ι → Type*} {S : Π i, setoid (X i)}

example {α γ : Type*} {S : setoid α}
  (f : α → γ) (hf) (t : α) : quotient.lift_on' (quotient.mk' t : quotient S) f hf = f t :=
  rfl

def quotient.lift_on_family'
  {γ : Type*} (f : (Π i, X i) → γ)
  (hf : ∀ (a b : Π i, X i), (∀ i, (S i).rel (a i) (b i)) → f a = f b) :
  (Π i, quotient (S i)) → γ := sorry

[Eric Wieser]

docs#quotient.induction_on_pi seems close

[Adam Topaz]

Hrrmmm that's a theorem...

[Adam Topaz]

But yet it's close

[Eric Wieser]

docs#quotient.choice and docs#quotient.fin_choice are the only other things that mention Π i, setoid or the misspelling ∀ i, setoid

[Adam Topaz]

I can't seem to figure out a way to define quotient.lift_on_family' compputably. Is it possible?

[Reid Barton]

I doubt it, but not sure exactly how to prove it

[Eric Wieser]

Presumably it's possible if the index type is finite

[Junyan Xu]

(Π i, quotient (S i)) → quotient (pi_setoid : setoid (Π i, X i)) cannot be defined in ZF without choice, because then Π i, X i could be empty even though X i is nonempty for every i (a choice function is exactly an element of the pi type). In this case, if S i is the equivalence relation that identifies all elements, then quotient (S i) is a singleton for every i and therefore Π i, quotient (S i) is also a singleton, but quotient pi_setoid is empty.

[Junyan Xu]

Just discovered that it's discussed 7 years ago: https://github.com/leanprover/lean/issues/649#issuecomment-107993581

[Yuyang Zhao]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Well-founded.20recursion.20for.20pgames I found a similar problem again a few days ago.

[Yuyang Zhao]

I proved this for [fintype ι] [decidable_eq ι] in #18315.

[Junyan Xu]

Are those list/multiset/finset versions of independent interest? Because if you just want quotient.lift for fintype, you can just do

import data.fintype.basic

variables {ι : Type*} [fintype ι] [decidable_eq ι] {α : ι → Type*} [S : Π i, setoid (α i)]
  {β : Sort*}

def quotient_lift (f : (Π i, α i) → β)
  (h : ∀ (a b : Π i, α i), (∀ i, a i ≈ b i) → f a = f b)
  (q : Π i, quotient (S i)) : β :=
quotient.lift _ h (quotient.fin_choice q)

Note that I changed α : ι → Sort* to Type*, but if you want the Sort version you probably just need to change some Type to Sort in existing code.

[Yuyang Zhao]

I moved quotient.fin_choice things to my new file and proved them without choice. multiset version is used in #18318.

[Junyan Xu]

I agree that removing decidability from docs#direct_sum.sigma_uncurry is a nice application of the multiset version, but I also think you don't really need 330 lines in list/quot.lean. Here is how you might construct docs#quotient.fin_choice without classical.choice in 62 lines: https://gist.github.com/alreadydone/48fcd994d56a129d1eeb347b1e568424
Even though restoring computability is of some interest, I think most people regard it pointless to remove uses of classical.choice in proofs (which doesn't contribute to non-computability) in exchange for a much longer proof.

[Yuyang Zhao]

Actually quotient.fin_choice doesn't depend on most lines in my PR, but then I'll check again to see if it can be golfed.

[Eric Wieser]

Note I just made #18337 to make the changes you're suggesting easier to port/review

[Yuyang Zhao]

In my PR,

• quotient.fin_choice_aux and quotient.fin_choice_aux_eq became list.quotient_choice and list.quotient_choice_mk.
• I proved the dependent recursion principle for quotients indexed by a list.
• Because I need the version for multiset, I had to use quotient.hrec_on (rather than quotient.lift_on) and deal with annoying heq.
• There are also some other simple lemmas.

These make list/quot.lean much longer.

[Eric Wieser]

What's the difference between quotients indexed by lists and quotients indexed by the finite subtype of membership in the lists?

[Yuyang Zhao]

Then I'll try to prove #18318 with the fintype version. If it's ok, I'll remove other versions.

[Junyan Xu]

Alternatively, as a direct approach, you could also use docs#equiv.subtype_quotient_equiv_quotient_subtype (where I think all the hard work had been done) as in my code; here's a draft and you should be able to fill in the sorry using adapted versions of the lemmas in my code.

import data.fintype.basic

variables {ι : Type*} {α : ι → Type*} [S : Π i, setoid (α i)] {β : Sort*}
include S

def quotient.map_pi_mem_multiset_of_list (l : list ι) (m : multiset ι) (h : m ⊆ ↑l) :
  @quotient (Π i ∈ l, α i) pi_setoid → @quotient (Π i ∈ m, α i) pi_setoid :=
quotient.map (λ f i hi, f i $ h hi) (λ f g he i hi, he i $ h hi)

def quotient_choice [decidable_eq ι] {m : multiset ι}
  (f : Π i ∈ m, quotient (S i)) : @quotient (Π i ∈ m, α i) pi_setoid :=
begin
  let := equiv.subtype_quotient_equiv_quotient_subtype
    (λ l : list ι, ↑l = m) (λ s, s = m) (λ i, iff.rfl) (λ _ _, iff.rfl) ⟨m, rfl⟩,
  refine quotient.lift_on this (λ l, _) (λ l₁ l₂ h, _),
  { exact (quotient.fin_choice_aux ↑l $
      λ i hi, f i $ l.2 ▸ hi).map_pi_mem_multiset_of_list _ _ (multiset.subset_of_le l.2.ge) },
  dsimp, sorry,
end

(I found docs#equiv.subtype_quotient_equiv_quotient_subtype when trying to resolve some issues that arised when Remi Bottinelli was working on quiver quotients.)

[Junyan Xu]

Update gist to generalize lemmas and kill the sorry in the multiset version.

[Eric Wieser]

If you're still planning to PR something along these lines, I recommend adding an entry to #port-comments (so that it appears on #port-status) asking people not to port data.fintype.quotient yet

[Johan Commelin]

Any news? Because this comment on #port-status is starting to bubble to the top...

[Eric Wieser]

If we decide to abandon the in-flight mathlib3 changes here, we should remember that we already ported the lemmas in one of these files once, so can recover the proof repairs from the original port

[Eric Wieser]

(the lemmas were moved from a ported file to an unported file, making them disappear from mathlib 4)

[Eric Wieser]

Cc @Yuyang Zhao about which mathlib3 PRs are salvageable

[Pol'tta / Miyahara Kō]

I created !4#3971 which ports Data.Fintype.Quotient.
At the moment, #18315 is dependent PR of this PR.
Does this PR seems to takes long time?
If so, we had better forward-port #18315 later.

[Yuyang Zhao]

Sorry for missing the message. I've been very busy recently. I will try to update the PR when I have time. If it blocks too many PRs, just ignore it and I will make a new mathlib4 PR later.

[Eric Wieser]

I'm leaning towards either:

• Merge everything into mathlib3 pretty much as is, throw away Mathlib.Data.Multiset.Pi in mathlib4 and re-port it from scratch
• Throw away the mathlib3 PRs, redo them in future in mathlib4

[Kevin Buzzard]

We need to get on, there is serious port momentum at the minute.

[Eric Wieser]

I don't understand this argument. There are 749 files that are yet to port. What makes the 7 blocked by port-status#data/fintype/quotient special?

[Mauricio Collares]

There are seven open mathlib4 PRs blocked on it, not just any seven files: !4#3971, !4#3972, !4#3976, !4#3980, !4#3989, !4#3991, !4#4112

[Mauricio Collares]

There was another thread in the PR reviews stream about it, but I can't link to it because I'm on mobile (edit: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2318417.20and.20port-status.23data.2Ffintype.2Fquotient)

[Eric Wieser]

Ah apologies, I thought I was looking there

[Pol'tta / Miyahara Kō]

For the moment, I've excluded #18315 from dependents of !4#3971.