Mathlib.Data.W.Cardinal

Module docstring

{"# Cardinality of W-types

This file proves some theorems about the cardinality of W-types. The main result is cardinalMk_le_max_aleph0_of_finite which says that if for any a : α, β a is finite, then the cardinality of WType β is at most the maximum of the cardinality of α and ℵ₀. This can be used to prove theorems about the cardinality of algebraic constructions such as polynomials. There is a surjection from a WType to MvPolynomial for example, and this surjection can be used to put an upper bound on the cardinality of MvPolynomial.

Tags

W, W type, cardinal, first order "}

WType.cardinalMk_eq_sum_lift theorem

: #(WType β) = sum fun a ↦ #(WType β) ^ lift.{u} #(β a)

Full source

theorem cardinalMk_eq_sum_lift : #(WType β) = sum fun a ↦ #(WType β) ^ lift.{u} #(β a) :=
  (mk_congr <| equivSigma β).trans <| by
    simp_rw [mk_sigma, mk_arrow]; rw [lift_id'lift_id'.{v, u}, lift_umaxlift_umax.{v, u}]

Cardinality of W-type as a Sum of Powers

Informal description

The cardinality of the W-type `WType β` is equal to the sum over all `a : α` of the cardinality of `WType β` raised to the power of the cardinality of `β a` (lifted to the appropriate universe). In symbols: \[ \#(WType \beta) = \sum_{a \in \alpha} \#(WType \beta)^{\#(\beta a)} \]

WType.cardinalMk_le_of_le' theorem

{κ : Cardinal.{max u v}} (hκ : (sum fun a : α => κ ^ lift.{u} #(β a)) ≤ κ) : #(WType β) ≤ κ

Full source

/-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ` -/
theorem cardinalMk_le_of_le' {κ : CardinalCardinal.{max u v}}
    (hκ : (sum fun a : α => κ ^ lift.{u} #(β a)) ≤ κ) :
    #(WType β) ≤ κ := by
  induction' κ using Cardinal.inductionOn with γ
  simp_rw [← lift_umax.{v, u}] at hκ
  nth_rewrite 1 [← lift_id'.{v, u} #γ] at hκ
  simp_rw [← mk_arrow, ← mk_sigma, le_def] at hκ
  obtain ⟨hκ⟩ := hκ
  exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)

Upper Bound on Cardinality of W-Type via Sum Condition

Informal description

Let $\kappa$ be a cardinal number (in the universe levels $\max(u,v)$) such that the sum $\sum_{a \in \alpha} \kappa^{\#(\beta a)}$ is less than or equal to $\kappa$. Then the cardinality of the W-type $\mathsf{WType}\,\beta$ is at most $\kappa$.

WType.cardinalMk_le_max_aleph0_of_finite' theorem

[∀ a, Finite (β a)] : #(WType β) ≤ max (lift.{v} #α) ℵ₀

Full source

/-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
is at most the maximum of the cardinality of `α` and `ℵ₀` -/
theorem cardinalMk_le_max_aleph0_of_finite' [∀ a, Finite (β a)] :
    #(WType β) ≤ max (lift.{v} #α) ℵ₀ :=
  (isEmpty_or_nonempty α).elim
    (by
      intro h
      rw [Cardinal.mk_eq_zero (WType β)]
      exact zero_le _)
    fun hn =>
    let m := max (lift.{v} #α) ℵ₀
    cardinalMk_le_of_le' <|
      calc
        (Cardinal.sum fun a => m ^ lift.{u} #(β a)) ≤ lift.{v} #α * ⨆ a, m ^ lift.{u} #(β a) :=
          Cardinal.sum_le_iSup_lift _
        _ ≤ m * ⨆ a, m ^ lift.{u} #(β a) := mul_le_mul' (le_max_left _ _) le_rfl
        _ = m :=
          mul_eq_left (le_max_right _ _)
              (ciSup_le' fun _ => pow_le (le_max_right _ _) (lt_aleph0_of_finite _)) <|
            pos_iff_ne_zero.1 <|
              Order.succ_le_iff.1
                (by
                  rw [succ_zero]
                  obtain ⟨a⟩ : Nonempty α := hn
                  refine le_trans ?_ (le_ciSup (bddAbove_range _) a)
                  rw [← power_zero]
                  exact
                    power_le_power_left
                      (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _))

Upper Bound on W-Type Cardinality for Finite Fibers: $\#(\mathsf{WType}\,\beta) \leq \max(\#\alpha, \aleph_0)$

Informal description

For any type family $\beta : \alpha \to \text{Type}$ where each $\beta(a)$ is finite, the cardinality of the W-type $\mathsf{WType}\,\beta$ is at most the maximum of the cardinality of $\alpha$ (lifted to the appropriate universe) and $\aleph_0$. In symbols: \[ \#(\mathsf{WType}\,\beta) \leq \max(\#\alpha, \aleph_0) \]

WType.cardinalMk_eq_sum theorem

: #(WType β) = sum (fun a : α => #(WType β) ^ #(β a))

Full source

theorem cardinalMk_eq_sum : #(WType β) = sum (fun a : α => #(WType β) ^ #(β a)) :=
  cardinalMk_eq_sum_lift.trans <| by simp_rw [lift_id]

Cardinality of W-type as Sum of Powers: $\#(\mathsf{WType}\,\beta) = \sum_{a \in \alpha} \#(\mathsf{WType}\,\beta)^{\#(\beta a)}$

Informal description

The cardinality of the W-type $\mathsf{WType}\,\beta$ is equal to the sum over all $a \in \alpha$ of the cardinality of $\mathsf{WType}\,\beta$ raised to the power of the cardinality of $\beta a$. In symbols: \[ \#(\mathsf{WType}\,\beta) = \sum_{a \in \alpha} \#(\mathsf{WType}\,\beta)^{\#(\beta a)} \]

WType.cardinalMk_le_of_le theorem

{κ : Cardinal.{u}} (hκ : (sum fun a : α => κ ^ #(β a)) ≤ κ) : #(WType β) ≤ κ

Full source

/-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ` -/
theorem cardinalMk_le_of_le {κ : CardinalCardinal.{u}} (hκ : (sum fun a : α => κ ^ #(β a)) ≤ κ) :
    #(WType β) ≤ κ := cardinalMk_le_of_le' <| by simp_rw [lift_id]; exact hκ

Upper Bound on W-Type Cardinality via Power Sum Condition: $\#(\mathsf{WType}\,\beta) \leq \kappa$ when $\sum_{a \in \alpha} \kappa^{\#(\beta a)} \leq \kappa$

Informal description

Let $\kappa$ be a cardinal number such that $\sum_{a \in \alpha} \kappa^{\#(\beta a)} \leq \kappa$. Then the cardinality of the W-type $\mathsf{WType}\,\beta$ satisfies $\#(\mathsf{WType}\,\beta) \leq \kappa$.

WType.cardinalMk_le_max_aleph0_of_finite theorem

[∀ a, Finite (β a)] : #(WType β) ≤ max #α ℵ₀

Full source

/-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
is at most the maximum of the cardinality of `α` and `ℵ₀` -/
theorem cardinalMk_le_max_aleph0_of_finite [∀ a, Finite (β a)] : #(WType β) ≤ max #α ℵ₀ :=
  cardinalMk_le_max_aleph0_of_finite'.trans_eq <| by rw [lift_id]

Upper Bound on W-Type Cardinality for Finite Fibers: $\#(\mathsf{WType}\,\beta) \leq \max(\#\alpha, \aleph_0)$

Informal description

For any type family $\beta : \alpha \to \text{Type}$ where each $\beta(a)$ is finite, the cardinality of the W-type $\mathsf{WType}\,\beta$ is at most the maximum of the cardinality of $\alpha$ and $\aleph_0$. In symbols: \[ \#(\mathsf{WType}\,\beta) \leq \max(\#\alpha, \aleph_0) \]