Cocountable and cocardinal

Stream: mathlib4

[Josha Dekker]

I would like to generalise cofinite to cocountable and in fact cocardinal for any cardinal. cofinite is defined through Filter.comk, for cocountable we recently introduced Filter.ofCountableUnion to provide an analogous tool.

I actually want to do the analogous thing forcocardinal, which is the filter generated by the sets that have complements of a given cardinality. I have the proofs working, but I'm not sure if this is the preferred way of writing this, so please let me know!

import Mathlib.Order.Filter.CountableInter

variable {α : Type*}

open Set Filter

def cocountable : Filter α := ofCountableUnion Set.Countable
  (fun _ hs hs2 ↦ Countable.sUnion hs hs2)  (fun _ ht _ a => Countable.mono a ht)

/-- Construct a filter with cardinal intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the cardinal intersection property. -/
def Filter.ofCardinalInter {c : Cardinal} (hc : Cardinal.aleph0 ≤ c) (l : Set (Set α))
    (hp : ∀ S : Set (Set α), (Cardinal.mk S ≤ c) → S ⊆ l → ⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α where
  sets := l
  univ_sets := by
    apply @sInter_empty α ▸ hp _ ?_ (empty_subset _)
    simp_all only [Cardinal.mk_eq_zero, zero_le]
  sets_of_superset := h_mono _ _
  inter_sets {s t} hs ht := by
    apply sInter_pair s t ▸ hp _ (ge_trans hc Cardinal.mk_le_aleph0)
      (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)

def Filter.ofCardinalUnion {c : Cardinal} (hc : Cardinal.aleph0 ≤ c) (p : Set α → Prop)
    (hUnion : ∀ S : Set (Set α), (Cardinal.mk S ≤ c) → (∀ s ∈ S, p s) → p (⋃₀ S))
    (hmono : ∀ t, p t → ∀ s ⊆ t, p s) : Filter α := by
  refine .ofCardinalInter hc {s | p sᶜ} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
  · rw [mem_setOf_eq, compl_sInter]
    exact hUnion _ (ge_trans hSc Cardinal.mk_image_le) (ball_image_iff.2 hSp)
  · exact hmono _ ht _ (compl_subset_compl.2 hsub)

-- Of course, this would generalise to CardinalInterFilter under a suitable definition for these.
instance Filter.countableInter_ofCardinalnter {c : Cardinal} (hc : Cardinal.aleph0 ≤ c) (l : Set (Set α))
    (hp : ∀ S : Set (Set α), (Cardinal.mk S ≤ c) → S ⊆ l → ⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
    CountableInterFilter (Filter.ofCardinalInter hc l hp h_mono) where
  countable_sInter_mem := fun _ hS a ↦ hp _ (ge_trans hc (Countable.le_aleph0 hS)) a

def cocardinal {c : Cardinal} (hc : Cardinal.aleph0 ≤ c) : Filter α := by
  apply ofCardinalUnion hc (fun _ ↦ Cardinal.mk _ ≤ c)
  · intro _ _ _
    exact hc
  · intro _ _ _ _
    simp_all only [Cardinal.mk_eq_aleph0]

[Josha Dekker]

I can also make a PR for this, but I'm not sure where to put these (cocountable should probably go to Order.Filter.CountableInter, but I'm not sure about the other ones).

[Josha Dekker]

This is now #10515, I'm happy to hear feedback! As the file for Cofinite.lean says that we should have versions for other cardinalities, do we want them all in the same file (or even in one more general def?) or does the way I currently do it (putting cofinite, cocountable and cocardinal in different places) look fine?

[Yury G. Kudryashov]

What files about cardinals do you have to import for the general definition?

[Josha Dekker]

currently I'm importing Mathlib.Order.Filter.CountableInter, I think that passed shake (but running shake on my device very often tells me that all imports are fine, and then CI tells me otherwise, so let's see..)

[Yury G. Kudryashov]

Could you please add mem_cocardinal lemma that unfolds the definition?

[Yury G. Kudryashov]

You're using too many _s in the definition.

[Yury G. Kudryashov]

I mean, it's OK to use them in the proof but not on the first apply line of def cocardinal.

[Josha Dekker]

Yury G. Kudryashov said:

You're using too many _s in the definition.

Yes, I agree. Should I just fill in the necessary terms there to make it look better?

[Yury G. Kudryashov]

Yes, please. And add mem_cocardinal to be 100% sure that you've defined what you wanted.

[Josha Dekker]

That's a good point, I'll add that and other basic API tomorrow! Do you think that the current definition (in particular the way I'm writing hc) is fine?

[Yury G. Kudryashov]

Yes, this is the standard way of assuming that a cardinal is infinite.

[Josha Dekker]

Great! I'd also like to define a CardinalInterFilter at some point, which I could do in tandem with cocardinal, or I can do it in a later PR. What would you say?

[Yury G. Kudryashov]

If you want your definition to give cofinite for c = aleph0, then you can use < instead of ≤. Then you'll need Order.succ aleph0 to get cocountable etc.

[Josha Dekker]

I have to stop for today, but I'll give it a go tomorrow!

[Yury G. Kudryashov]

OTOH, it will be much easier to define the filter of sets that are complement of something of cardinality strictly less than continuum.

[Josha Dekker]

My thought was to get cofinite for c < aleph0, so that cocardinal exactly picks up where cofinite stops. I could deduce cocountable as a special case of cocardinal if we like that?

[Yury G. Kudryashov]

You can't get < version from ≤ version but you can get ≤ version from < version.

[Josha Dekker]

I was a bit unclear, what I meant was that, when you would like to have c < aleph0, you use cofinite, whereas if you would like to have c >= aleph0, you use cocardinal.

On second thought I do agree it is better to go for full generality indeed and define hc in terms of Cardinal.aleph0 < c. I'll do that as well tomorrow, thank you

[Yury G. Kudryashov]

I'm surprised that you never use docs#Cardinal.mul_lt_of_lt or something like that.

[Yury G. Kudryashov]

#s < c, not aleph0 < c

[Josha Dekker]

Yury G. Kudryashov said:

#s < c, not aleph0 < c

yes, you're right!

[Yury G. Kudryashov]

I think that some of these _ are filled with something you didn't want to have there.

[Yury G. Kudryashov]

That's why the proof doesn't need advanced lemmas about cardinals.

[Josha Dekker]

Yury G. Kudryashov said:

That's why the proof doesn't need advanced lemmas about cardinals.

Let me make _-free proofs tomorrow, thank you for pointing this out!

[Josha Dekker]

I've rewritten in terms of < and removed most of the _, but I'm having trouble closing the last sorry (I'd think the result should be true at least, it is a rather basic statement about cardinalities but I sometimes get confused by these)

open Set Filter

universe u

variable {α : Type*}

namespace Filter

/-- Construct a filter with cardinal intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the cardinal intersection property. -/
def ofCardinalInter {c : Cardinal} (hc : Cardinal.aleph0 ≤ c) (l : Set (Set α))
    (hp : ∀ S : Set (Set α), (Cardinal.mk S < c) → S ⊆ l → ⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α where
  sets := l
  univ_sets := by
    apply @sInter_empty α ▸ hp ∅ ?_ (empty_subset l)
    rw [Cardinal.mk_eq_zero]
    exact gt_of_ge_of_gt hc Cardinal.aleph0_pos
  sets_of_superset := fun {x y} a a_1 ↦ h_mono x y a a_1
  inter_sets {s t} hs ht := by
    apply sInter_pair s t ▸ hp {s, t} ?_
    · exact insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩
    · exact gt_of_ge_of_gt hc (Cardinal.lt_aleph0_of_finite _)

/-- Construct a filter sets whose complements satisfy a property that is stable under unions
with a certain cardinality. -/
def ofCardinalUnion {c : Cardinal} (hc : Cardinal.aleph0 ≤ c) (p : Set α → Prop)
    (hUnion : ∀ S : Set (Set α), (Cardinal.mk S < c) → (∀ s ∈ S, p s) → p (⋃₀ S))
    (hmono : ∀ t, p t → ∀ s ⊆ t, p s) : Filter α := by
  refine .ofCardinalInter hc {s | p sᶜ} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ hmono sᶜ ht tᶜ (compl_subset_compl.2 hsub)
  rw [mem_setOf_eq, compl_sInter]
  exact hUnion (compl '' S) (lt_of_le_of_lt Cardinal.mk_image_le hSc) (ball_image_iff.2 hSp)

/-- The filter defined by all sets that have a complement with at most cardinality `c`. -/
def cocardinal {c : Cardinal} (hc : Cardinal.aleph0 ≤ c) : Filter α := by
  apply ofCardinalUnion hc (fun s ↦ Cardinal.mk s < c)
  · intro s hS hSc
    apply lt_of_le_of_lt
    apply Cardinal.mk_sUnion_le
    apply Cardinal.mul_lt_of_lt hc hS
    sorry
  · exact fun _ hSc _ ht ↦ lt_of_le_of_lt (Cardinal.mk_le_mk_of_subset ht) hSc

[Josha Dekker]

Yury G. Kudryashov said:

Yes, please. And add mem_cocardinal to be 100% sure that you've defined what you wanted.

If you add

@[simp]
theorem mem_cocardinal {s : Set α} {c : Cardinal} {hc : Cardinal.aleph0 ≤ c} :
    s ∈ @cocardinal α c hc ↔ Cardinal.mk (sᶜ : Set α) < c := Iff.rfl

below the def of cocardinal, you get this! I'll make the commit when I closed the last sorry!

[Josha Dekker]

I've added this to #10515 by the way, build is only failing because of the sorry, as far as I can tell.

[Josha Dekker]

Josha Dekker said:

I've added this to #10515 by the way, build is only failing because of the sorry, as far as I can tell.

I can close the goal if I assume that c is a regular cardinal (I've committed this change now) as I then have access to Cardinal.iSup_lt_of_isRegular. Is that the right approach, or is there some proof possible where cocardinal only needs to assume hc : Cardinality.aleph0 ≤ c?

[Yury G. Kudryashov]

I don't know

[Yury G. Kudryashov]

Possibly, the "lt" idea was not as good as I thought.

[Yury G. Kudryashov]

Note that you get a filter for any infinite cardinal, just not a c-intersection filter for some c.

[Josha Dekker]

Yes, that is true. The point is of course to build a specific cocardinal filter that will then have a nice CardinalInterFilter property. For this, we need the iSup of c values, all at most c, to be equal to c again, for which we need to assume that c is regular (at least, based on current tools in Mathlib. I'm not too familiar with all mathematical nuances here)