Coordinatizing continuum-sized torsion-free Abelian groups

This file formalizes the coordinatization lemma used in Section 2 of the paper. A torsion-free Abelian group of cardinality continuum embeds in the rational direct sum of continuum rank in a way whose image contains every standard basis vector.

structure Wallace.RationalCoordinatization (G : Type) [AddCommGroup G] : Type

The witness form of the paper's coordinatization lemma.

• embedding : G →+ RationalTriangularPreprocess.ContinuumRationalGroup

  An additive embedding of G into the continuum-indexed rational direct sum.

• embedding_injective : Function.Injective ⇑self.embedding
• basisPreimage : TriangularPreprocess.ContinuumIndex → G

  A chosen preimage in G of every standard basis vector.

• embedding_basisPreimage (i : TriangularPreprocess.ContinuumIndex) : self.embedding (self.basisPreimage i) = Finsupp.single i 1

theorem Wallace.RationalCoordinatization.mk_divisibleHull {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : Cardinal.mk (DivisibleHull G) = Cardinal.continuum

Localizing a continuum-sized torsion-free group by the positive integers does not change its cardinality.

theorem Wallace.RationalCoordinatization.rank_divisibleHull {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : Module.rank ℚ (DivisibleHull G) = Cardinal.continuum

The divisible hull has rational dimension continuum.

noncomputable def Wallace.RationalCoordinatization.continuumBasis {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : Module.Basis TriangularPreprocess.ContinuumIndex ℚ (DivisibleHull G)

A rational basis of the divisible hull indexed by the canonical continuum type.

Equations

• Wallace.RationalCoordinatization.continuumBasis hcard = (Module.Free.chooseBasis ℚ (DivisibleHull G)).reindex (Classical.choice ⋯)

noncomputable def Wallace.RationalCoordinatization.basisNumerator {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) (i : TriangularPreprocess.ContinuumIndex) : G

A numerator in G representing a vector of the chosen basis of the divisible hull.

Equations

• Wallace.RationalCoordinatization.basisNumerator hcard i = Classical.choose ⋯

noncomputable def Wallace.RationalCoordinatization.basisDenominator {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) (i : TriangularPreprocess.ContinuumIndex) : ℕ+

The positive denominator attached to basisNumerator.

Equations

• Wallace.RationalCoordinatization.basisDenominator hcard i = Classical.choose ⋯

theorem Wallace.RationalCoordinatization.basisFraction {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) (i : TriangularPreprocess.ContinuumIndex) : DivisibleHull.mk (basisNumerator hcard i) (basisDenominator hcard i) = (continuumBasis hcard) i

theorem Wallace.RationalCoordinatization.denominator_smul_basis {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) (i : TriangularPreprocess.ContinuumIndex) : ↑↑(basisDenominator hcard i) • (continuumBasis hcard) i = ↑(basisNumerator hcard i)

noncomputable def Wallace.RationalCoordinatization.integralBasis {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : Module.Basis TriangularPreprocess.ContinuumIndex ℚ (DivisibleHull G)

Rescale the chosen rational basis so that every basis vector is literally the image of an element of the original group.

Equations

• Wallace.RationalCoordinatization.integralBasis hcard = (Wallace.RationalCoordinatization.continuumBasis hcard).isUnitSMul ⋯

theorem Wallace.RationalCoordinatization.integralBasis_apply {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) (i : TriangularPreprocess.ContinuumIndex) : (integralBasis hcard) i = ↑(basisNumerator hcard i)

noncomputable def Wallace.RationalCoordinatization.canonicalEmbedding {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : G →+ RationalTriangularPreprocess.ContinuumRationalGroup

The additive embedding furnished by the rescaled basis.

Equations

• Wallace.RationalCoordinatization.canonicalEmbedding hcard = (↑(Wallace.RationalCoordinatization.integralBasis hcard).repr).toAddMonoidHom.comp (DivisibleHull.coeAddMonoidHom G)

theorem Wallace.RationalCoordinatization.canonicalEmbedding_injective {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : Function.Injective ⇑(canonicalEmbedding hcard)

theorem Wallace.RationalCoordinatization.canonicalEmbedding_basisNumerator {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) (i : TriangularPreprocess.ContinuumIndex) : (canonicalEmbedding hcard) (basisNumerator hcard i) = Finsupp.single i 1

noncomputable def Wallace.RationalCoordinatization.ofCardinalityContinuum {G : Type} [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : RationalCoordinatization G

Torsion-free coordinatization lemma (paper, Section 2). Every torsion-free Abelian group of cardinality continuum embeds in ℚ^(𝔠) and its image contains ℤ^(𝔠), expressed by the preimage of every standard basis vector.

Equations

• One or more equations did not get rendered due to their size.