Coercion from finset of subtype to finset

Stream: Is there code for X?

[Gareth Ma]

Hi, I am not sure what the correct way to express this is:

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fintype.Basic

open Nat Int Finset

example [DecidableEq α] [Fintype α] (s : Finset α) (a : α) (h : a ∈ s) :
    a ∈ (univ.subtype (· ∈ s) : Finset α) := by
  sorry

This is my first time dealing with subtypes and stuff

[Gareth Ma]

It gives the error

type mismatch
  Finset.subtype (fun x => x ∈ s) univ
has type
  Finset { x // x ∈ s } : Type ?u.16
but is expected to have type
  Finset α : Type ?u.16

i.e. there's no coercion between the types

[Yakov Pechersky]

That's right, I don't think we have a Finset subtype -> Finset basetype conversion for this or other "functorial" types

[Yakov Pechersky]

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fintype.Basic

open Nat Int Finset

variable {α : Type*}

example [DecidableEq α] [Fintype α] (s : Finset α) (a : α) (h : a ∈ s) :
    a ∈ (((univ.subtype (· ∈ s)).image (↑))) := by simp [h]

[Yakov Pechersky]

Or

example [DecidableEq α] [Fintype α] (s : Finset α) (a : α) (h : a ∈ s) :
    a ∈ (((univ.subtype (· ∈ s)).map (Function.Embedding.subtype _))) := by simp [h]

[Gareth Ma]

Oh god :hide: just .image Subtype.val works though :) Thanks :)

[Gareth Ma]

It feels like this should be in Mathlib or somewhere though?

[Gareth Ma]

or does no one find subtypes useful

[Kyle Miller]

Do you know about docs#Finset.attach ? I think that's more canonical that univ.subtype ...

[Kyle Miller]

example [DecidableEq α] (s : Finset α) (a : α) (h : a ∈ s) :
    a ∈ s.attach.image (↑) := by
  simp [h]

[Yakov Pechersky]

There's also this generalization, which doesn't require Fintype

lemma foo [DecidableEq α] (s t : Finset α) (hst : s ⊆ t) (a : α) (h : a ∈ s) :
    a ∈ (((t.subtype (· ∈ s)).map (Function.Embedding.subtype _))) := by
  simp [h, hst h]

[Gareth Ma]

Kyle's code also doesn't require fintype

[Gareth Ma]

haha

[Yakov Pechersky]

and DecidableEq is too strong, [DecidablePred (· ∈ s)] is enough

[Yakov Pechersky]

Yes, anything that doesn't mention univ

[Gareth Ma]

Yakov Pechersky said:

and DecidableEq is too strong, [DecidablePred (· ∈ s)] is enough

I thought Finset \a requires DecidableEq \a

[Gareth Ma]

failed to synthesize instance DecidableEq α :(

[Kyle Miller]

You don't need decidable at all:

example (s : Finset α) (a : α) (h : a ∈ s) :
    a ∈ s.attach.map (Function.Embedding.subtype _) := by
  simp [h]

[Yakov Pechersky]

I meant for this:

lemma foo (s t : Finset α) (hst : s ⊆ t) (a : α) (h : a ∈ s) [DecidablePred (· ∈ s)] :
    a ∈ (((t.subtype (· ∈ s)).map (Function.Embedding.subtype _))) := by
  simp [h, hst h]

[Kyle Miller]

It's the image operation that needs decidable equality, since the way it works is it applies the function and then removes duplicates.

[Eric Wieser]

s.map (.subtype _) is about the same length and easier to prove thing about than s.image subtype.val

[Gareth Ma]

Ah but map takes an injective function instead, I see

[Gareth Ma]

Aha okay,. I am getting a hang of it now. For future reference:

example (s : Finset α) [DecidableEq α] [DecidablePred (· ∈ s)]  :
    (univ : Finset { x // x ∈ s }).map (.subtype _) = s := by
  rw [univ_eq_attach, attach_map_val]

/- Don't write this! Extra predicate bad. -/
example (s : Finset α) [DecidablePred (· ∈ s)] : s.attach = s.subtype (· ∈ s) := by
  ext a
  simp only [mem_attach, mem_subtype, coe_mem]

[Gareth Ma]

I will ask here since it's vaguely related: Does any of these results exist? For context, I am trying to prove that there is an ordered isomorphism between Fin n and Fin s where s.card = n. Without the "ordered" in OrderedIso, there's equivFinOfCardEq already.

[Gareth Ma]

import Mathlib

open Nat Int Finset Fintype

theorem Function.Embedding.fintype_of_fintype [Fintype β] (f : α ↪ β) : Fintype α := by
  apply fintypeOfFinsetCardLe (Fintype.card β)
  intro s
  rw [←card_coe s]
  refine card_le_of_embedding ⟨fun x ↦ f x, fun a b h ↦ ?_⟩
  ext
  exact (EmbeddingLike.apply_eq_iff_eq _).mp h

theorem OrderEmbedding.OrderEmbedding_comp_OrderIso
    {α β γ : Type*} [LE α] [PartialOrder β] [PartialOrder γ]
    (f : α ≃o β) (g : β ↪o γ) : α ↪o γ := {
  toFun := g.toFun ∘ f.toFun
  inj' := g.inj'.comp f.injective
  map_rel_iff' := by simp
}

noncomputable example [LinearOrder ι] (n : ℕ) (f : ι ↪ Fin n) : ι ↪o Fin n := by
  have h₁ : Fintype ι := f.fintype_of_fintype
  have h₂ : ι ≃o _ := (@monoEquivOfFin ι h₁ _ (Fintype.card ι) rfl).symm
  have h₃ : Fintype.card ι ≤ Fintype.card (Fin n) := card_le_of_embedding f
  rw [Fintype.card_fin] at h₃
  apply OrderEmbedding.OrderEmbedding_comp_OrderIso h₂
  exact Fin.castLEEmb h₃

(And also some help with how to name the results would be appreciated...)

[Gareth Ma]

(deleted)

[Eric Wieser]

That first one is rejected by #lint

[Gareth Ma]

Oh, I didn't know about that

[Eric Wieser]

The second is f.toOrderHom.como g or similar

[Gareth Ma]

The second one is f.toOrderEmbedding.trans g

[Gareth Ma]

Okay I golfed a bit

noncomputable def Function.Embedding.fintype_of_fintype [Fintype β] (f : α ↪ β) : Fintype α := by
  refine fintypeOfFinsetCardLe (Fintype.card β) (fun s ↦ ?_)
  rw [←card_coe s]
  refine card_le_of_embedding ⟨fun x ↦ f x, fun a b h ↦ ?_⟩
  exact Subtype.ext $ (EmbeddingLike.apply_eq_iff_eq _).mp h

noncomputable example [LinearOrder ι] (n : ℕ) (f : ι ↪ Fin n) : ι ↪o Fin n := by
  have h₁ : Fintype ι := f.fintype_of_fintype
  have h₂ : ι ↪o _ := (@monoEquivOfFin ι h₁ _ (Fintype.card ι) rfl).symm.toOrderEmbedding
  have h₃ : Fintype.card ι ≤ Fintype.card (Fin n) := card_le_of_embedding f
  rw [Fintype.card_fin] at h₃
  exact h₂.trans $ Fin.castLEEmb h₃

[Gareth Ma]

I can't seem to find the first one. What should it be named?

[Kyle Miller]

The first one is docs#Fintype.ofInjective