Cardinal bounds for the transfinite construction

The estimates are stated against one ambient infinite cardinal θ. The successor target is controlled by its explicit dense set of finite linear combinations, followed by the generic sequence encoding of metric closure.

theorem ScottishBook155.CardinalControl.adjunctionSpace_mk_le {M N : Type u} [NormedAddCommGroup M] [NormedSpace ℝ M] [PseudoMetricSpace N] (V : M → N) (a : M) (y : N) (H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (θ : Cardinal.{u}) (hθ : Cardinal.aleph0 ≤ θ) (hM : Cardinal.mk M ≤ θ) (hN : Cardinal.mk N ≤ θ) (hR : Cardinal.lift.{u, 0} (Cardinal.mk ℝ) ≤ θ) : Cardinal.mk (AdjunctionSpace V a y H hattach) ≤ θ

The underlying metric adjunction has no more points than the source and target used to generate it.

theorem ScottishBook155.CardinalControl.sigma_mk_le {ι : Type u} {G : ι → Type u} (θ : Cardinal.{u}) (hθ : Cardinal.aleph0 ≤ θ) (hι : Cardinal.mk ι ≤ θ) (hG : ∀ (i : ι), Cardinal.mk (G i) ≤ θ) : Cardinal.mk (Sigma G) ≤ θ

A family whose index and every fiber have size at most θ has a sigma type of size at most θ.

theorem ScottishBook155.CardinalControl.directLimitCarrier_mk_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (θ : Cardinal.{u}) (hθ : Cardinal.aleph0 ≤ θ) (hι : Cardinal.mk ι ≤ θ) (hG : ∀ (i : ι), Cardinal.mk (G i) ≤ θ) : Cardinal.mk (NormedDirectLimit.Carrier G f) ≤ θ

The algebraic normed direct limit is no larger than the sigma type of its components, because every direct-limit point has a one-component representative.

theorem ScottishBook155.CardinalControl.completedDirectLimit_mk_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (θ : Cardinal.{u}) (hθ : Cardinal.aleph0 ≤ θ) (hι : Cardinal.mk ι ≤ θ) (hG : ∀ (i : ι), Cardinal.mk (G i) ≤ θ) (hpow : θ ^ Cardinal.aleph0 = θ) : Cardinal.mk (NormedDirectLimit.CompletedCarrier G f) ≤ θ

Completing a normed direct limit preserves the bound θ whenever θ is closed under countable powers.

theorem ScottishBook155.CardinalControl.protectedEnvelope_mk_le {P N : Type u} [MetricSpace P] [Nonempty P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (θ : Cardinal.{u}) (hθ : Cardinal.aleph0 ≤ θ) (hN : Cardinal.mk N ≤ θ) (hP : Cardinal.mk P ≤ θ) (hR : Cardinal.lift.{u, 0} (Cardinal.mk ℝ) ≤ θ) (hpow : θ ^ Cardinal.aleph0 = θ) : Cardinal.mk ↥(ProtectedEnvelope P N j) ≤ θ

The protected envelope has cardinality at most θ when its two generating types do and θ is closed under countable powers.