order_iso.map_supr

Stream: Is there code for X?

[Eric Wieser]

I can't find this: can anyone see a golfing strategy?

lemma order_iso.map_supr {ι : Sort*} {α : Type*} {β : Type*}
  [complete_lattice α] [complete_lattice β] (f : α ≃o β)
  (x : ι → α) : f (⨆ i, x i) = ⨆ i, f (x i) :=
begin
  apply le_antisymm,
  { rw le_supr_iff,
    intros b hb,
    rw ←order_iso.le_symm_apply,
    apply supr_le,
    intro i,
    rw order_iso.le_symm_apply,
    exact hb i },
  { rw ←order_iso.symm_apply_le,
    rw le_supr_iff,
    intros b hb,
    rw order_iso.symm_apply_le,
    apply supr_le,
    intro i,
    rw order_iso.le_iff_le,
    exact hb i },
end

lemma order_iso.map_infi {ι : Sort*} {α : Type*} {β : Type*}
  [complete_lattice α] [complete_lattice β] (f : α ≃o β)
  (x : ι → α) : f (⨅ i, x i) = ⨅ i, f (x i) :=
order_iso.map_supr f.dual _

[Eric Wieser]

aha, docs#monotone.le_map_supr helps

[Kevin Buzzard]

Note issue #408

[Eric Wieser]

I don't see the connection all that well here

[Eric Wieser]

PR'd a shorter version of the above as #10451

[Kevin Buzzard]

I guess maybe I'm conflating two similar but different things. Both are of the form "if things are isomorphic then they're the same to mathematicians" and it's a shame that there's not some general machine which will write such proofs

[Eric Wieser]

I don't see how a general machine could write the proof I needed

[Reid Barton]

there's another ingredient involved here, namely, the sup is determined by <= (by Yoneda) even though Lean calls it extra data

[Eric Wieser]

I can see a general machine using order_iso.map_supr

[Reid Barton]

lemma order_iso.map_supr {ι : Sort*} {α : Type*} {β : Type*}
  [complete_lattice α] [complete_lattice β] (f : α ≃o β)
  (x : ι → α) : f (⨆ i, x i) = ⨆ i, f (x i) :=
begin
  have : ∀ y, f (⨆ i, x i) ≤ y ↔ (⨆ i, f (x i)) ≤ y,
  { rw function.surjective.forall f.surjective, simp },
  apply le_antisymm, { rw this }, { rw ←this }
end

[Kevin Buzzard]

The principle I want to invoke is that if A and B are isomorphic structures via f then all constructions in A which only use the structure are mirrored in B via f

[Reid Barton]

(btw it seems like a bug that the parentheses are needed in (⨆ i, f (x i)) ≤ y)

[Kevin Buzzard]

They'd be needed with ∀, right?

[Reid Barton]

Yes, but surely with ⨆ the purpose is exactly to compare it using <=

[Eric Wieser]

Do you prefer that proof to this one in the PR?

lemma order_iso.map_supr  {ι : Sort*} {α : Type*} {β : Type*}
  [complete_lattice α] [complete_lattice β] (f : α ≃o β) (x : ι → α) :
  f (⨆ i, x i) = ⨆ i, f (x i) :=
begin
  refine le_antisymm _ f.monotone.le_map_supr,
  rw ←order_iso.le_symm_apply,
  refine le_trans _ f.symm.monotone.le_map_supr,
  simp_rw f.symm_apply_apply,
end

[Eric Wieser]

Reid Barton said:

(btw it seems like a bug that the parentheses are needed in (⨆ i, f (x i)) ≤ y)

This has been complained about repeatedly, no one has bothered to fix it

[Yaël Dillies]

There should be a galois_connection version of this lemma.

[Reid Barton]

Kevin's Principle strikes again!

[Eric Wieser]

Right, it's docs#galois_connection.l_supr

[Eric Wieser]

Although I can't prove the lemma as early if I prove it using that

[Yury G. Kudryashov]

You can also use something like eq_of_forall_ge_iff $ λ b, by simp only [supr_le, f.surjective.forall] (untested)

[Eric Wieser]

I think PR comments on #10451 are probably the place for golfing suggestions