The ring of profinite integers

The profinite integers ℤ̂ = zHat are a profinite group written multiplicatively; this file puts the ring structure on their additive presentation Additive zHat. Multiplication by a is the unique continuous endomorphism of ℤ̂ sending the generator zHat.gen to a, exactly as multiplication by an integer is on ℤ: so a * b is zHat.lift a b, read additively. The unit is the generator, and the casts of natural numbers and integers are its powers.

The ring is commutative, and the multiplication is jointly continuous, so Additive zHat is a compact, totally disconnected topological commutative ring in which the integers are dense (zHat.denseRange_intCast). The defining equations for the product and the unit are recorded as simp lemmas on both sides of the equivalence between zHat and Additive zHat, and the casts are read in zHat by the simp lemmas zHat.toMul_natCast and zHat.toMul_intCast; in the other direction simp reads a power of the generator as a cast through Mathlib's Additive.ofMul_pow and Additive.ofMul_zpow together with zHat.ofMul_gen. Thus a statement about the ring can be rewritten into the language of zHat.lift and back.

This is the ring by which a profinite group is powered: the profinite power of an element x of a profinite group by a : ℤ̂ is zHat.lift x a, and by naturality of the lift (zHat.map_lift) powering first by a and then by b is powering by the product a * b defined here. That power, TauCeti.zpowHat, is developed in TauCeti.Topology.Algebra.Group.Profinite.ZHat.Pow.

Main definitions

• The CommRing (Additive zHat) and IsTopologicalRing (Additive zHat) instances.

Main results

• TauCeti.zHat.toMul_mul, TauCeti.zHat.ofMul_lift: the product is the lift.
• TauCeti.zHat.toMul_one, TauCeti.zHat.toMul_natCast, TauCeti.zHat.toMul_intCast, TauCeti.zHat.ofMul_ofInt: the unit and the casts of integers are the powers of the generator.
• TauCeti.zHat.denseRange_intCast: the integers are dense in the ring.

Implementation notes

The multiplicative notation of zHat is the addition of the ring: the group product of two elements of zHat is their sum in Additive zHat, and the ring product exists only on Additive zHat. There is no second carrier of the profinite integers.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 2.3 and 4.1.

@[instance_reducible]

noncomputable instance TauCeti.zHat.instCommRing : CommRing (Additive ↑zHat.toProfinite.toTop)

The ring of profinite integers. On Additive zHat the product of a and b is zHat.lift a b, the value at b of the continuous endomorphism of ℤ̂ sending the generator to a; the unit is the generator, and the casts of ℕ and ℤ are its powers.

Equations

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

@[simp]

theorem TauCeti.zHat.toMul_mul (a b : Additive ↑zHat.toProfinite.toTop) : Additive.toMul (a * b) = (lift (Additive.toMul a)) (Additive.toMul b)

The product of the ring, read in zHat: (a * b).toMul is the lift of a.toMul at b.toMul.

@[simp]

theorem TauCeti.zHat.ofMul_lift (a b : ↑zHat.toProfinite.toTop) : Additive.ofMul ((lift a) b) = Additive.ofMul a * Additive.ofMul b

The lift of a at b, read in the ring: ofMul (lift a b) is the product ofMul a * ofMul b.

@[simp]

theorem TauCeti.zHat.toMul_one : Additive.toMul 1 = gen

The unit of the ring, read in zHat, is the generator.

@[simp]

theorem TauCeti.zHat.ofMul_gen : Additive.ofMul gen = 1

The generator, read in the ring, is the unit.

@[simp]

theorem TauCeti.zHat.toMul_natCast (n : ℕ) : Additive.toMul ↑n = gen ^ n

The cast of a natural number n, read in zHat, is the n-th power of the generator.

@[simp]

theorem TauCeti.zHat.toMul_intCast (n : ℤ) : Additive.toMul ↑n = gen ^ n

The cast of an integer n, read in zHat, is the n-th power of the generator.

@[simp]

theorem TauCeti.zHat.ofMul_ofInt (z : Multiplicative ℤ) : Additive.ofMul (ofInt z) = ↑(Multiplicative.toAdd z)

The canonical homomorphism from ℤ to the profinite integers is the integer cast of the ring.

theorem TauCeti.zHat.denseRange_intCast : DenseRange Int.cast

The integers are dense in the ring of profinite integers.

instance TauCeti.zHat.instIsTopologicalRingAdditiveCarrierToTopTotallyDisconnectedSpaceToProfinite : IsTopologicalRing (Additive ↑zHat.toProfinite.toTop)

The ring of profinite integers is a topological ring: its additive group is the topological group zHat, and the product is jointly continuous.