Skip to content

Instantly share code, notes, and snippets.

@ChrisHughes24
Created July 23, 2020 15:48
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save ChrisHughes24/73d40b1b31f07b81cbec47ef88700a7c to your computer and use it in GitHub Desktop.
Save ChrisHughes24/73d40b1b31f07b81cbec47ef88700a7c to your computer and use it in GitHub Desktop.
import data.dfinsupp
import tactic
universes u v w
variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii → jj → Type w) [Π i j, decidable_eq (β i j)]
variables [Π i j, has_zero (β i j)]
def to_fun (x : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j :=
quotient.lift_on x
(λ x, ⟦dfinsupp.pre.mk
(λ i, show Π₀ j : jj, β i j,
from ⟦dfinsupp.pre.mk
(λ j, x.to_fun (i, j))
(x.pre_support.map prod.snd)
(λ j, (x.3 (i, j)).elim (λ h, or.inl (multiset.mem_map.2 ⟨(i, j), h, rfl⟩)) or.inr)⟧)
(x.pre_support.map prod.fst)
(λ i, or_iff_not_imp_left.2 $ λ h, dfinsupp.ext $ λ j, (x.3 (i, j)).resolve_left
(λ hij, h (multiset.mem_map.2 ⟨(i, j), hij, rfl⟩)))⟧)
(λ a b hab, dfinsupp.ext (λ i, dfinsupp.ext (λ j, hab _)))
def inv_fun (x : Π₀ i, Π₀ j, β i j) : Π₀ (ij : ii × jj), β ij.1 ij.2 :=
quotient.lift_on x
(λ x, ⟦dfinsupp.pre.mk (λ i : ii × jj, quotient.lift_on (x.1 i.1)
(λ x, x.1 i.2)
(λ a b hab, hab _))
(x.pre_support.bind (λ i, (quotient.lift_on (x.1 i)
(λ x, ((x.pre_support.filter (λ j, x.1 j ≠ 0)).map (λ j, (i, j))).to_finset)
(λ a b hab, begin
ext p,
cases a, cases b,
replace hab : a_to_fun = b_to_fun := funext hab,
subst hab,
cases p with p₁ p₂,
simp [and_comm _ (_ = p₂), @and.left_comm _ (_ = p₂)],
specialize b_zero p₂,
specialize a_zero p₂,
tauto,
end)).1))
(λ i, or_iff_not_imp_right.2 begin
generalize hxi : x.1 i.1 = a,
revert hxi,
refine quotient.induction_on a (λ a hxi, _),
assume h,
have h₁ := (a.3 i.2).resolve_right h,
have h₂ := (x.3 i.1).resolve_right (λ ha, begin
rw [hxi] at ha,
exact h ((quotient.exact ha) i.snd),
end),
simp only [exists_prop, ne.def, multiset.mem_bind],
use i.fst,
rw [hxi, quotient.lift_on_beta],
simp only [multiset.mem_erase_dup, multiset.to_finset_val,
multiset.mem_map, multiset.mem_filter],
exact ⟨h₂, i.2, ⟨h₁, h⟩, by cases i; refl⟩
end)⟧)
(λ a b hab, dfinsupp.ext $ λ i, by unfold_coes; simp [hab i.1])
example : (Π₀ (ij : ii × jj), β ij.1 ij.2) ≃ Π₀ i, Π₀ j, β i j :=
{ to_fun := to_fun β,
inv_fun := inv_fun β,
left_inv := λ x, quotient.induction_on x (λ x, dfinsupp.ext (λ i, by cases i; refl)),
right_inv := λ x, quotient.induction_on x (λ x, dfinsupp.ext (λ i, dfinsupp.ext (λ j,
begin
generalize hxi : x.1 i = a,
revert hxi,
refine quotient.induction_on a (λ a hxi, _),
rw [to_fun, inv_fun],
unfold_coes,
simp,
rw [hxi, quotient.lift_on_beta, quotient.lift_on_beta],
end))) }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment