-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(data/dfinsupp): Add an equivalence between (Π₀ i j, β i j) and (Π₀ ij, β ij.1 ij.2) #3515
Conversation
…Π₀ ij, β ij.1 ij.2) This is very much a work in progress. Submitting this commit so others can try and flesh out the proofs.
src/data/dfinsupp/prod.lean
Outdated
let js : multiset jj := quotient.lift_on (fi.to_fun i) | ||
dfinsupp.pre.pre_support | ||
(λ a b H, begin | ||
/- This is unprovable, I think lift_on is the wrong approach, or I need to return a clever quotient -/ | ||
sorry | ||
end), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
an alternative is to invoke the axiom of choice:
let js : multiset jj := quotient.lift_on (fi.to_fun i) | |
dfinsupp.pre.pre_support | |
(λ a b H, begin | |
/- This is unprovable, I think lift_on is the wrong approach, or I need to return a clever quotient -/ | |
sorry | |
end), | |
let js : multiset jj := dfinsupp.pre.pre_support (quotient.out (fi.to_fun i)), |
but that still makes the following sorry
hard to prove.
exact ⟦{ | ||
to_fun := λ i, ⟦ { | ||
to_fun := λ j, fij.to_fun (i, j), | ||
pre_support := fij.pre_support.map prod.snd, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
well this doesn't transfer easily when replacing ι₁ × ι₂ by a sigma type
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I had assumed it would be fine, but the comment you made in the other PR looked convincing
Closed in favor of #18316. |
Similar to
equiv.Pi_curry
/finsupp_prod_equiv
, but fordfinsupp
.Unlike
finsupp_prod_equiv
in 92b9a00, this aims to not require[add_comm_monoid _]
This is very much a work in progress. Submitting this commit so others can try and flesh out the proofs.