countable fibres, countable target => countable source

Stream: Is there code for X?

[Kevin Buzzard]

I am making a meal of this; it started off fine but I ended up in HEq hell (and escaped from it with rw!). What am I missing? Is the result already in mathlib in some form? Is this proof somehow going the wrong way?

import Mathlib

lemma Countable.of_countable_fibres {X Y : Type*} (f : X → Y) [Countable Y]
    [∀ (y : Y), Countable (f ⁻¹' {y})] : Countable X := by
  let e : X → Σ y, f ⁻¹' {y} := fun x ↦ ⟨f x, x, by simp⟩
  suffices e.Injective from Function.Injective.countable this
  -- ⊢ Function.Injective e
  -- looking good so far
  intro x1 x2 h
  simp [e] at h
  -- now in HEq hell
  obtain ⟨h1, h2⟩ := h
  rw! [h1] at h2
  simpa using h2

FWIW I use this to prove that there are countably many prime ideals in a number field so that I can apply measure-theoretic techniques to the adeles (in FLT we have things like Spec(B)->Spec(A) has finite fibres for finite extensions of Dedekind domains, ultimately reducing countability in the general case to countability of the prime numbers, which mathlib has).

[Sébastien Gouëzel]

import Mathlib

lemma Countable.of_countable_fibres {X Y : Type*} (f : X → Y) [Countable Y]
    [h : ∀ (y : Y), Countable (f ⁻¹' {y})] : Countable X := by
  rw [← Set.countable_univ_iff]
  have : (Set.univ : Set X) = ⋃ y, f ⁻¹' {y} := by ext ;simp
  rw [this]
  have A y : Set.Countable (f ⁻¹' {y}) := h y
  simp [A]

[Ruben Van de Velde]

import Mathlib

lemma Countable.of_countable_fibres {X Y : Type*} (f : X → Y) [Countable Y]
    [h : ∀ (y : Y), Countable (f ⁻¹' {y})] : Countable X := by
  let e := Equiv.sigmaPreimageEquiv f
  rw [e.symm.countable_iff]
  infer_instance

[Sébastien Gouëzel]

Your lemma statement is a little bit strange, because f ⁻¹' {y} is a set, so it would feel more natural to use Set.Countable as a regular assumption, instead of Countable as a typeclass assumption on the subtype.

[Jireh Loreaux]

But also the statement is weird because h should be phrased using Set.countable

[Floris van Doorn]

Here's my version

import Mathlib

open Set
lemma Countable.of_countable_fibres {X Y : Type*} (f : X → Y) [Countable Y]
    [∀ (y : Y), Countable (f ⁻¹' {y})] : Countable X := by
  simp_rw [← Set.countable_univ_iff, ← preimage_univ (f := f), ← Set.iUnion_of_singleton,
    preimage_iUnion, Set.countable_iUnion ‹_›]

[Kevin Buzzard]

Set.Countable is fine, I've not really used countability before. Thanks to all! Indeed I see that we used Set.Finite when stating the fact about extensions of Dedekind domains.

[Ruben Van de Velde]

docs#Set.iUnion_of_singleton shouldn't have of, should it?

[Kevin Buzzard]

I now understand from the proofs that the trick is to move towards Set.Countable rather than working with types.

This now works in FLT and looks really nice:

lemma Countable.of_countable_fibres {X Y : Type*} {f : X → Y} [Countable Y]
    (h : ∀ (y : Y), (f ⁻¹' {y}).Countable) : Countable X := by
  simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion ‹_›]

instance : Countable (HeightOneSpectrum (𝓞 ℚ)) := Countable.of_equiv _
  IsDedekindDomain.HeightOneSpectrum.ratEquiv.symm

instance : Countable (HeightOneSpectrum (𝓞 K)) :=
  Countable.of_countable_fibres <| fun y ↦
  ((preimage_comap_finite (𝓞 ℚ) ℚ K (𝓞 K)) {y} (by simp)).countable