Grace/Cumulus/Real/Embedding.g17

Open in Workbench Download source

Imports

Order

Declarations

Source

1-- The rational embedding into the Dedekind reals: the cut map is strictly2-- monotone and injective, reflects the order, and ℚ is dense in ℝ3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Real.Embedding9import Order1011-- The canonical map q ↦ { p ∈ ℚ | p < q } as a set-valued graph.12def rationalEmbedding : Set :=13  { p ∈ ℚ × ℝ |14    ∃ q ∈ ℚ, p = (q ↦ rationalCut(q)) }1516theorem rationalEmbedding.relates (q x : Set)17  shows relates(rationalEmbedding, q, x) ↔18    (q ∈ ℚ ∧ x = rationalCut(q))19proof20  constructor21  . intro related22    unfold relates at related23    simp [rationalEmbedding.membership] at related24    rcases related with ⟨bounded, r, rRational, shape⟩25    obtain ⟨qShape, xShape⟩ := orderedPair.injective with shape26    constructor27    . rw qShape28      exact rRational29    . rw qShape30      exact xShape31  . intro data32    rcases data with ⟨qRational, rfl⟩33    have qTyped : Rational(q) by exact qRational34    unfold relates35    apply rationalEmbedding.membership.backward36    constructor37    . apply product.pair at q, rationalCut(q), ℚ, ℝ38      . exact qRational39      . exact rationalCut.real with qTyped40    . refine ⟨q, qRational, rfl⟩4142theorem rationalEmbedding.total43  shows TotalBetween(rationalEmbedding, ℚ, ℝ)44proof45  intros q qRational46  have qTyped : Rational(q) by exact qRational47  witness rationalCut(q)48  constructor49  . exact rationalCut.real with qTyped50  . apply rationalEmbedding.relates.backward at q, rationalCut(q)51    refine ⟨qRational, rfl⟩5253theorem rationalEmbedding.functional54  shows Functional(rationalEmbedding)55proof56  intros q x qx y qy57  have xData := rationalEmbedding.relates.forward with qx58  have yData := rationalEmbedding.relates.forward with qy59  rcases xData with ⟨_, xShape⟩60  rcases yData with ⟨_, yShape⟩61  rw [xShape, yShape]62  rfl6364theorem rationalEmbedding.function65  shows rationalEmbedding : ℚ → ℝ66proof67  constructor68    intros p hp69    simp [rationalEmbedding.membership] at hp70    rcases hp with ⟨bounded, witnesses⟩71    exact bounded72  . constructor73    . exact rationalEmbedding.functional74    . exact rationalEmbedding.total7576theorem rationalEmbedding.value (q : Set)77  requires qRational : Rational(q)78  shows rationalEmbedding(q) = rationalCut(q)79proof80  apply FunctionBetween.apply_value at rationalEmbedding, ℚ, ℝ, q, rationalCut(q)81  . exact rationalEmbedding.function82    exact qRational83  . apply rationalEmbedding.relates.backward at q, rationalCut(q)84    constructor85      exact qRational86    . rfl8788-- Equality of lower cuts reflects equality of rationals.  Connectedness of89-- the rational order leaves only the two strict cases, and strict monotonicity90-- makes either case incompatible with equal cuts.91theorem rationalCut.injective (q r : Set)92  requires qRational : Rational(q)93  requires rRational : Rational(r)94  requires equalCuts : rationalCut(q) = rationalCut(r)95  shows q = r96proof97  by_contra distinct98  have qInQ := qRational99  have rInQ := rRational100  have connected := rationalLess.connected_on101  have comparison := connected with q, qInQ, r, rInQ, distinct102  rcases comparison with qLessR | rLessQ103  . have strict := rationalCut.strict_mono at q, r with104      qRational, rRational, qLessR105    rcases strict with ⟨_, _, proper⟩106    have unequal := ProperSubset.ne with proper107    exact unequal with equalCuts108  . have strict := rationalCut.strict_mono at r, q with109      rRational, qRational, rLessQ110    rcases strict with ⟨_, _, proper⟩111    have unequal := ProperSubset.ne with proper112    apply unequal113    rw equalCuts114    rfl115116theorem rationalEmbedding.injective117  shows InjectiveBetween(rationalEmbedding, ℚ, ℝ)118proof119  constructor120  . exact rationalEmbedding.function121  . intros q qInQ r rInQ x xInR qx rx122    have qData := rationalEmbedding.relates.forward with qx123    have rData := rationalEmbedding.relates.forward with rx124    rcases qData with ⟨_, qShape⟩125    rcases rData with ⟨_, rShape⟩126    have equalCuts : rationalCut(q) = rationalCut(r) by rwa ← qShape127    exact rationalCut.injective with equalCuts128129-- The cut embedding reflects the order.130theorem rationalCut.lt_of_cut_lt (p q : Rational)131  requires less : RealLess(rationalCut(p), rationalCut(q))132  shows p < q133proof134  have order := rationalLess.trichotomy at p, q135  cases order with below | rest136  . exact below137  . exfalso138    cases rest with equal | above139    . rw equal at less140      exact RealLess.irreflexive with less141    . have reversed := rationalCut.strict_mono with above142      have cycle := RealLess.transitive with less, reversed143      exact RealLess.irreflexive with cycle144145-- The rationals are dense in the reals: between two reals lies a rational146-- cut. A real is a lower cut; a rational of y missing from x, pushed up147-- once inside y, has a cut strictly between the two.148theorem rationalCut.between (x y : Real)149  requires less : x < y150  shows ∃ q ∈ ℚ, x < rationalCut(q) ∧ rationalCut(q) < y151proof152  obtain ⟨typedX, typedY, inclusion⟩ :=153    realLess.characterization.forward with less154  have cutX := Real.characterization.forward with typedX155  have cutY := Real.characterization.forward with typedY156  obtain ⟨r, rInY, rMissing⟩ := ProperSubset.missing with inclusion157  obtain ⟨s, sInY, rLessS⟩ := DedekindCut.no_greatest with cutY, rInY158  have rationalsX := DedekindCut.subset_rationals with cutX159  have rationalsY := DedekindCut.subset_rationals with cutY160  have rInQ := rationalsY with r, rInY161  have sInQ := rationalsY with s, sInY162  have cutS := rationalCut.real at s with sInQ163  have transitive := rationalLess.transitive_on164  witness s165  refine ⟨sInQ, ?_, ?_⟩166  . apply realLess.characterization.backward167    refine ⟨typedX, cutS, ?_⟩168    constructor169    . intros p pInX170      have pInQ := rationalsX with p, pInX171      have pLessR := DedekindCut.lt_missing with cutX, pInX, rInQ, rMissing172      have pLessS := transitive with173        p, pInQ, r, rInQ, s, sInQ, pLessR, rLessS174      exact rationalCut.membership.backward with ⟨pInQ, pLessS⟩175    . intro same176      apply rMissing177      rw same178      exact rationalCut.membership.backward with ⟨rInQ, rLessS⟩179  . apply realLess.characterization.backward180    refine ⟨cutS, typedY, ?_⟩181    constructor182    . intros p pInCut183      obtain ⟨pInQ, pLessS⟩ := rationalCut.membership.forward with pInCut184      exact DedekindCut.downward with cutY, sInY, pInQ, pLessS185    . intro same186      have sInCut : s ∈ rationalCut(s)187        rw same188        exact sInY189      obtain ⟨_, selfLess⟩ := rationalCut.membership.forward with sInCut190      have irreflexive := rationalLess.irreflexive_on191      exact irreflexive with s, sInQ, selfLess192