The set of finite sets is well-founded?

Stream: Is there code for X?

[Rémi Bottinelli]

Hey! I have a set S : set $ set X and I know that all elements of S are finite. Is there an easy way to get a minimal element of S?
Equivalently (I believe), is there something along the lines of is_well_founded_on ({s : set X | s.finite}) (ssubset) ?

Actually, let me ensure I'm not falling into #xy : I have the following code (trying to deal with this ) and I want to drop the fintype assumption in favour of the one in the docstring (last lemma).

import category_theory.filtered
import topology.category.Top.limits
import data.finset.basic
import category_theory.category.basic
import category_theory.full_subcategory
import data.set.finite
import data.fintype.basic
import category_theory.types

universes u v w

open classical
open category_theory

noncomputable theory
local attribute [instance] prop_decidable


def category_theory.functor.eventual_range
  {J : Type u} [category J] [is_cofiltered J] (F : J ⥤ Type v) :=
λ (j : J), ⋂ (i : J) (f : i ⟶ j), set.range (F.map f)

def category_theory.functor.is_mittag_leffler
  {J : Type u} [category J] [is_cofiltered J] (F : J ⥤ Type v) :=
  ∀ (j : J), ∃ (i) (f : i ⟶ j),
             ∀ (i') (f' : i' ⟶ j), set.range (F.map f) ⊆ set.range (F.map f')

lemma category_theory.functor.is_mittag_leffler_iff_eventual_range
  {J : Type u} [category J] [is_cofiltered J] (F : J ⥤ Type v) :
  F.is_mittag_leffler ↔ ∀ (j : J), ∃ (i : J) (f : i ⟶ j), F.eventual_range j = set.range (F.map f) :=
begin
  dsimp [category_theory.functor.eventual_range],
  sorry,
end

/--
There is probably a nice general argument along the lines of:
* If J is cofiltered, then so is J/j (the comma category) for any j.
* The functor F : J ⥤ Type v defines a functor J/j ⥤ (F.obj j) by sending (f : i ⟶ j) to set.range $ F.map f
* The image of a cofiltered category is cofiltered
-/
lemma category_theory.functor.ranges_directed_of_is_cofiltered
  {J : Type u} [category J] [is_cofiltered J] (F : J ⥤ Type v) (j : J) :
  directed_on (⊇) (set.range (λ ( f : Σ' (i : J), i ⟶ j), set.range (F.map f.2))) :=
begin
  rintros _ ⟨⟨i,ij⟩,rfl⟩ _ ⟨⟨k,kj⟩,rfl⟩,
  let l := is_cofiltered.min i k,
  let li := is_cofiltered.min_to_left i k,
  let lk := is_cofiltered.min_to_right i k,
  let m := is_cofiltered.eq (li ≫ ij) (lk ≫ kj),
  let ml := is_cofiltered.eq_hom (li ≫ ij) (lk ≫ kj),
  refine ⟨set.range (F.map $ ml ≫ li ≫ ij), _⟩,
  simp only [set.mem_range, exists_prop],
  refine ⟨⟨⟨m, ml ≫ li ≫ ij⟩, rfl⟩, ⟨_, _⟩⟩,
  { dsimp [superset], simp_rw [functor.map_comp, types_comp],
    change (F.map ij ∘ F.map li) ∘ F.map ml with F.map ij ∘ (F.map li ∘ F.map ml),
    apply set.range_comp_subset_range, },
  { dsimp [superset],
    simp_rw [category_theory.is_cofiltered.eq_condition, functor.map_comp, types_comp],
    change is_cofiltered.eq_hom (li ≫ ij) (lk ≫ kj) with ml,
    change (F.map kj ∘ F.map lk) ∘ F.map ml with F.map kj ∘ (F.map lk ∘ F.map ml),
    apply set.range_comp_subset_range, },
end

-- Probably exists somewhere
lemma directed_on_min {J : Type u} {s : set J} [preorder J] (h : directed_on (≥) s)
  (m ∈ s) (min : ∀ (a ∈ s), a ≤ m → a = m) : ∀ a ∈ s, m ≤ a :=
begin
  rintro a as,
  obtain ⟨x, xs, xm, xa⟩ := h m H a as,
  cases (min x xs xm),
  exact xa,
end

/--
With enough `well_founded`-fu, one could probably weaken the `fintype` hypothesis to
\```
  ∀ (j i : J) (f : i ⟶ j), (set.range $ F.map f).finite
\```
-/
lemma category_theory.functor.is_mittag_leffler_of_fintype
  {J : Type u} [category.{w} J] [is_cofiltered J] (F : J ⥤ Type v)
  [Π (j : J), fintype (F.obj j)] :
  F.is_mittag_leffler :=
begin
  rintro j,
  haveI : nonempty (Σ' i, i ⟶ j) := ⟨⟨j,𝟙 j⟩⟩,
  let f := function.argmin
             (λ (f : Σ' i, i ⟶ j), set.range (F.map f.2))
             (finite.well_founded_of_trans_of_irrefl has_ssubset.ssubset),
  refine ⟨f.1, f.2, λ i' f', _⟩,
  refine directed_on_min (F.ranges_directed_of_is_cofiltered j)
         (set.range (F.map f.2)) ⟨f,rfl⟩ _
         (set.range (F.map f')) ⟨⟨i',f'⟩,rfl⟩,
  rintro _ ⟨g,rfl⟩ klef,
  cases lt_or_eq_of_le klef,
  { exfalso,
    exact function.not_lt_argmin (λ (f : Σ' i, i ⟶ j), set.range (F.map f.2)) _ g h, },
  { exact h, },
end

[Eric Wieser]

I assume by minimal you mean something weaker than "in docs#lower_bounds"? otherwise S := {{1, 2}, {2,3}] is a problem.

[Eric Wieser]

Or did you also mean "every finite set is in S"?

[Rémi Bottinelli]

Indeed, I need an element of the set with nothing below it, essentially.

[Yaël Dillies]

Probably you want set (finset \a), rather?

[Junyan Xu]

∀ (j i : J) (f : i ⟶ j), (set.range $ F.map f).finite

Notice that if you take f to be the identity you'd be able to show all F.obj j are finite from this. Maybe you want to assume ∀ j, ∃ i (f : i ⟶ j), (set.range $ F.map f).finite instead.

Also, category_theory.functor.is_mittag_leffler_of_fintype should use finite instead of fintype.

[Junyan Xu]

You should be able to deduce well-foundedness of finset α from docs#multiset.well_founded_lt and the order embedding from finset α to multiset α (does this exist?).

[Eric Wieser]

I would guess the order embedding is trivial to construct but doesn't exist

[Eric Wieser]

The fact that we have that result for multiset suggests we should have it in mathlib for finset, XY problems aside

[Yaël Dillies]

I was about to write the same thing!

[Eric Wieser]

The proof of the multiset lemma is a single line, subrelation.wf (λ _ _, multiset.card_lt_of_lt) (measure_wf multiset.card)

[Eric Wieser]

I would guess you can directly copy that using docs#finset.card_lt_of_ssubset

[Eric Wieser]

... if that existed

[Yaël Dillies]

docs#finset.card_lt_card

[Yaël Dillies]

The naming is all over the place.

[Rémi Bottinelli]

Yaël Dillies said:

Probably you want set (finset \a), rather?

Well, I really wanted the set of finite sets since it's a range, but Junyan's comment makes me reconsider the stupidity of what I asked for

[Rémi Bottinelli]

Re finite vs fintype: does that mean that nonempty_section_of_fintype_inverse_system should be corrected too?

[Rémi Bottinelli]

Rémi Bottinelli said:

Yaël Dillies said:

Probably you want set (finset \a), rather?

Well, I really wanted the set of finite sets since it's a range, but Junyan's comment makes me reconsider the stupidity of what I asked for

Mmh, I think the proof would indeed work with the \forall j \exists i (f : i \--> j), … version

[Kevin Buzzard]

Hey! I have a set S : set $ set X and I know that all elements of S are finite. Is there an easy way to get a minimal element of S?

Take an element of minimal cardinality?

[Junyan Xu]

Seems going through finset is still easier because we have docs#set.finite.to_finset_ssubset.
But we don't seem to have the fact that a strict subset of a finite set has strictly less cardinality (neither docs#nat.card nor docs#cardinal.mk).

[Rémi Bottinelli]

Kevin Buzzard said:

Hey! I have a set S : set $ set X and I know that all elements of S are finite. Is there an easy way to get a minimal element of S?

Take an element of minimal cardinality?

Yeah, I'm probably gonna take this approach

[Rémi Bottinelli]

I went with the following, which is not too bad as far as I can tell:

lemma category_theory.functor.is_mittag_leffler_of_exists_finite_range
  {J : Type u} [category.{w} J] [is_cofiltered J] (F : J ⥤ Type v)
  (h : ∀ (j : J), ∃ i (f : i ⟶ j), (set.range (F.map f)).finite ) :
  F.is_mittag_leffler :=
begin
  rintro j,
  suffices : ∃ (f : Σ' i, i ⟶ j), ∀ (f' : Σ' i, i ⟶ j),
               set.range (F.map f'.2) ≤ set.range (F.map f.2) →
                 set.range (F.map f'.2) = set.range (F.map f.2),
  { obtain ⟨⟨i, f⟩, fmin⟩ := this,
    refine ⟨i, f, λ i' f', _⟩,
    refine directed_on_min (F.ranges_directed_of_is_cofiltered j) _ ⟨⟨i, f⟩,rfl⟩ _ _ ⟨⟨i',f'⟩,rfl⟩,
    simp only [set.mem_range, psigma.exists, forall_exists_index],
    rintro _ k g rfl gf,
    exact fmin ⟨k,g⟩ gf, },

  let fins := subtype { f : Σ' i, i ⟶ j | (set.range (F.map f.2)).finite },
  haveI : nonempty fins := by { obtain ⟨i,f,fin⟩ := h j, exact ⟨⟨⟨i,f⟩,fin⟩⟩, },
  let fmin := function.argmin (λ (f : fins), f.prop.to_finset.card) nat.lt_wf,
  use fmin.val,
  rintro g gf,
  cases lt_or_eq_of_le gf,
  { have gfin : (set.range (F.map g.2)).finite := fmin.prop.subset gf,
    refine ((λ (f : fins), f.prop.to_finset.card).not_lt_argmin nat.lt_wf ⟨g, gfin⟩ _).elim,
    exact finset.card_lt_card (set.finite.to_finset_ssubset.mpr h_1), },
  { assumption, },
end

[Yaël Dillies]

#17950