The prime-to-p Tate module of the roots of unity

For a commutative monoid E and a natural number p, the prime-to-p Tate module

PrimeToPTateModule p E = lim_{m ≠ 0, (m, p) = 1} μ_m(E)

is the inverse limit of the groups μ_m(E) = rootsOfUnity m E over the nonzero m prime to p, ordered by divisibility, along the power maps μ_m(E) → μ_n(E), ζ ↦ ζ ^ (m / n) for n ∣ m. Concretely, a point is a family (ζ_m)_m of roots of unity with ζ_m ^ (m / n) = ζ_n whenever n ∣ m. It carries the inverse-limit topology, induced from the product of the discrete groups μ_m(E), and is a topological group; for a domain E the levels are finite, so it is compact.

When E is a separably closed field of exponential characteristic p, this is the group written ℤ̂^{(p')}(1): as a profinite group it is ∏_{ℓ ≠ p} ℤ_ℓ, while the twist (1) records the action of automorphisms of E on it. For a local field K with residue characteristic p, the inertia group of K maps to it through the tame character.

Main definitions

• TauCeti.primeToPTateModuleSubgroup p E: the subgroup of compatible families in the product ∏_m μ_m(E).
• TauCeti.PrimeToPTateModule p E: the prime-to-p Tate module, a commutative topological group.
• TauCeti.PrimeToPTateModule.proj m: the projection to the level μ_m(E).
• TauCeti.PrimeToPTateModule.mk: the point with prescribed compatible components.
• TauCeti.PrimeToPTateModule.lift: the homomorphism into the Tate module determined by a compatible family of homomorphisms into the levels.
• TauCeti.PrimeToPTateModule.map: the homomorphism of Tate modules induced by a monoid homomorphism E →* F.
• The instance MulDistribMulAction M (PrimeToPTateModule p E) for a monoid M acting on E by multiplicative maps, componentwise; for the Galois group of E it is the twist (1).

Main results

• TauCeti.PrimeToPTateModule.proj_pow_div: the components of a point are compatible.
• TauCeti.PrimeToPTateModule.ext: a point is determined by its components.
• TauCeti.PrimeToPTateModule.lift_unique: lift is the unique homomorphism with the prescribed components.
• TauCeti.PrimeToPTateModule.continuous_iff: a map into the Tate module is continuous exactly when each of its components is locally constant.
• TauCeti.PrimeToPTateModule.surjective_of_forall_surjective_proj: a continuous map from a compact space is surjective when each of its components is.
• TauCeti.PrimeToPTateModule.exists_forall_isPrimitiveRoot_proj: such a map, surjective at each level, takes a value whose components are all primitive roots of unity.
• TauCeti.PrimeToPTateModule.topologicalClosure_zpowers_eq_top: over a domain, a point whose components are all primitive roots of unity topologically generates the Tate module.
• TauCeti.PrimeToPTateModule.proj_map, TauCeti.PrimeToPTateModule.coe_proj_smul: map and the action are computed componentwise.
• The instances IsTopologicalGroup, T2Space, TotallyDisconnectedSpace, ContinuousConstSMul, and, for a domain, CompactSpace.

def TauCeti.primeToPTateModuleSubgroup (p : ℕ) (E : Type u_1) [CommMonoid E] : Subgroup ((m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) → ↥(rootsOfUnity (↑m) E))

The subgroup of the product ∏_m μ_m(E), over the nonzero m prime to p, consisting of the families (ζ_m)_m compatible along the power maps: ζ_m ^ (m / n) = ζ_n whenever n ∣ m. Its carrier is the prime-to-p Tate module PrimeToPTateModule p E.

Equations

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

theorem TauCeti.mem_primeToPTateModuleSubgroup_iff {p : ℕ} {E : Type u_1} [CommMonoid E] {x : (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) → ↥(rootsOfUnity (↑m) E)} : x ∈ primeToPTateModuleSubgroup p E ↔ ∀ (m n : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), ↑n ∣ ↑m → ↑(x m) ^ (↑m / ↑n) = ↑(x n)

A family of roots of unity lies in the Tate-module subgroup exactly when it is compatible along the power maps.

def TauCeti.PrimeToPTateModule (p : ℕ) (E : Type u_1) [CommMonoid E] : Type u_1

The prime-to-p Tate module lim_{m ≠ 0, (m, p) = 1} μ_m(E) of the roots of unity of E: the compatible families of roots of unity of order prime to p, along the power maps ζ ↦ ζ ^ (m / n). For a separably closed field of exponential characteristic p it is the group ℤ̂^{(p')}(1). It carries the inverse-limit topology.

Equations

• TauCeti.PrimeToPTateModule p E = ↥(TauCeti.primeToPTateModuleSubgroup p E)

@[instance_reducible]

noncomputable instance TauCeti.PrimeToPTateModule.instCommGroup (p : ℕ) (E : Type u_1) [CommMonoid E] : CommGroup (PrimeToPTateModule p E)

Equations

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

noncomputable def TauCeti.PrimeToPTateModule.proj {p : ℕ} {E : Type u_1} [CommMonoid E] (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) : PrimeToPTateModule p E →* ↥(rootsOfUnity (↑m) E)

The projection of the prime-to-p Tate module to its level μ_m(E).

Equations

• TauCeti.PrimeToPTateModule.proj m = (Pi.evalMonoidHom (fun (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) => ↥(rootsOfUnity (↑m) E)) m).comp (TauCeti.primeToPTateModuleSubgroup p E).subtype

theorem TauCeti.PrimeToPTateModule.proj_pow_div {p : ℕ} {E : Type u_1} [CommMonoid E] (x : PrimeToPTateModule p E) {m n : { m : ℕ // m ≠ 0 ∧ m.Coprime p }} (h : ↑n ∣ ↑m) : ↑((proj m) x) ^ (↑m / ↑n) = ↑((proj n) x)

The components of a point of the Tate module are compatible along the power maps.

theorem TauCeti.PrimeToPTateModule.ext {p : ℕ} {E : Type u_1} [CommMonoid E] {x y : PrimeToPTateModule p E} (h : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), (proj m) x = (proj m) y) : x = y

A point of the Tate module is determined by its components.

theorem TauCeti.PrimeToPTateModule.ext_iff {p : ℕ} {E : Type u_1} [CommMonoid E] {x y : PrimeToPTateModule p E} : x = y ↔ ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), (proj m) x = (proj m) y

noncomputable def TauCeti.PrimeToPTateModule.mk {p : ℕ} {E : Type u_1} [CommMonoid E] (x : (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) → ↥(rootsOfUnity (↑m) E)) (hx : x ∈ primeToPTateModuleSubgroup p E) : PrimeToPTateModule p E

The point of the Tate module with prescribed compatible components.

Equations

• TauCeti.PrimeToPTateModule.mk x hx = ⟨x, hx⟩

@[simp]

theorem TauCeti.PrimeToPTateModule.proj_mk {p : ℕ} {E : Type u_1} [CommMonoid E] (x : (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) → ↥(rootsOfUnity (↑m) E)) (hx : x ∈ primeToPTateModuleSubgroup p E) (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) : (proj m) (mk x hx) = x m

The components of mk x hx are the prescribed ones.

theorem TauCeti.PrimeToPTateModule.range_proj {p : ℕ} {E : Type u_1} [CommMonoid E] : (Set.range fun (x : PrimeToPTateModule p E) (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) => (proj m) x) = ↑(primeToPTateModuleSubgroup p E)

The family of components identifies the Tate module with the subgroup of compatible families of the product.

noncomputable def TauCeti.PrimeToPTateModule.lift {p : ℕ} {E : Type u_1} [CommMonoid E] {G : Type u_2} [MulOneClass G] (f : (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) → G →* ↥(rootsOfUnity (↑m) E)) (hf : ∀ (m n : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) (g : G), ↑n ∣ ↑m → ↑((f m) g) ^ (↑m / ↑n) = ↑((f n) g)) : G →* PrimeToPTateModule p E

The homomorphism into the prime-to-p Tate module determined by a family of homomorphisms into the levels μ_m(E) that is compatible along the power maps.

Equations

• TauCeti.PrimeToPTateModule.lift f hf = (MonoidHom.pi f).codRestrict (TauCeti.primeToPTateModuleSubgroup p E) ⋯

@[simp]

theorem TauCeti.PrimeToPTateModule.proj_lift {p : ℕ} {E : Type u_1} [CommMonoid E] {G : Type u_2} [MulOneClass G] (f : (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) → G →* ↥(rootsOfUnity (↑m) E)) (hf : ∀ (m n : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) (g : G), ↑n ∣ ↑m → ↑((f m) g) ^ (↑m / ↑n) = ↑((f n) g)) (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) (g : G) : (proj m) ((lift f hf) g) = (f m) g

The components of lift f hf are the prescribed homomorphisms.

theorem TauCeti.PrimeToPTateModule.lift_unique {p : ℕ} {E : Type u_1} [CommMonoid E] {G : Type u_2} [MulOneClass G] (f : (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) → G →* ↥(rootsOfUnity (↑m) E)) (hf : ∀ (m n : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) (g : G), ↑n ∣ ↑m → ↑((f m) g) ^ (↑m / ↑n) = ↑((f n) g)) (F : G →* PrimeToPTateModule p E) (hF : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), (proj m).comp F = f m) : F = lift f hf

Uniqueness of the lift. A homomorphism into the Tate module whose components are the prescribed homomorphisms f m is lift f hf.

The inverse-limit topology

@[instance_reducible]

noncomputable instance TauCeti.PrimeToPTateModule.instTopologicalSpace {p : ℕ} {E : Type u_1} [CommMonoid E] : TopologicalSpace (PrimeToPTateModule p E)

The inverse-limit topology on the prime-to-p Tate module, induced from the product of the discrete groups μ_m(E).

Equations

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

theorem TauCeti.PrimeToPTateModule.continuous_iff {p : ℕ} {E : Type u_1} [CommMonoid E] {X : Type u_2} [TopologicalSpace X] {f : X → PrimeToPTateModule p E} : Continuous f ↔ ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), IsLocallyConstant fun (x : X) => (proj m) (f x)

A map into the prime-to-p Tate module is continuous exactly when each of its components is locally constant.

theorem TauCeti.PrimeToPTateModule.isLocallyConstant_proj {p : ℕ} {E : Type u_1} [CommMonoid E] (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) : IsLocallyConstant ⇑(proj m)

Each projection of the prime-to-p Tate module is locally constant.

instance TauCeti.PrimeToPTateModule.instIsTopologicalGroup {p : ℕ} {E : Type u_1} [CommMonoid E] : IsTopologicalGroup (PrimeToPTateModule p E)

instance TauCeti.PrimeToPTateModule.instT2Space {p : ℕ} {E : Type u_1} [CommMonoid E] : T2Space (PrimeToPTateModule p E)

instance TauCeti.PrimeToPTateModule.instTotallyDisconnectedSpace {p : ℕ} {E : Type u_1} [CommMonoid E] : TotallyDisconnectedSpace (PrimeToPTateModule p E)

instance TauCeti.PrimeToPTateModule.instCompactSpaceOfIsDomain {p : ℕ} {R : Type u_2} [CommRing R] [IsDomain R] : CompactSpace (PrimeToPTateModule p R)

For a domain, the levels μ_m(E) are finite, so the prime-to-p Tate module is compact: it is a closed subgroup of the product of the finite discrete levels.

theorem TauCeti.PrimeToPTateModule.surjective_of_forall_surjective_proj {p : ℕ} {E : Type u_1} [CommMonoid E] {X : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : X → PrimeToPTateModule p E} (hf : Continuous f) (h : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), Function.Surjective fun (x : X) => (proj m) (f x)) : Function.Surjective f

Surjectivity from the finite levels. A continuous map from a compact space into the prime-to-p Tate module is surjective as soon as each of its components is surjective: the fibres over the components of a point form a directed family of nonempty closed sets, whose intersection is the fibre over the point.

Topological generators

theorem TauCeti.PrimeToPTateModule.exists_forall_isPrimitiveRoot_proj {p : ℕ} {E : Type u_1} [CommMonoid E] {X : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : X → PrimeToPTateModule p E} (hf : Continuous f) (h : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), Function.Surjective fun (x : X) => (proj m) (f x)) (hE : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), ∃ (ζ : E), IsPrimitiveRoot ζ ↑m) : ∃ (x : X), ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), IsPrimitiveRoot ↑((proj m) (f x)) ↑m

A point with primitive components. If E has a primitive m-th root of unity for every nonzero m prime to p, and a continuous map f from a compact space into the Tate module is surjective at each level, then some value f x has a primitive m-th root of unity as its level-m component for every m.

theorem TauCeti.PrimeToPTateModule.topologicalClosure_zpowers_eq_top {p : ℕ} {R : Type u_2} [CommRing R] [IsDomain R] {ζ : PrimeToPTateModule p R} (hζ : ∀ (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }), IsPrimitiveRoot ↑((proj m) ζ) ↑m) : (Subgroup.zpowers ζ).topologicalClosure = ⊤

A topological generator. Over a domain, a point of the Tate module whose level-m component is a primitive m-th root of unity for every m generates a dense subgroup.

Functoriality and the action of automorphisms

noncomputable def TauCeti.PrimeToPTateModule.map {p : ℕ} {E : Type u_1} [CommMonoid E] {F : Type u_2} [CommMonoid F] (f : E →* F) : PrimeToPTateModule p E →* PrimeToPTateModule p F

The homomorphism of prime-to-p Tate modules induced by a monoid homomorphism f : E →* F, applying f to each component μ_m(E) → μ_m(F).

Equations

• TauCeti.PrimeToPTateModule.map f = TauCeti.PrimeToPTateModule.lift (fun (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) => (restrictRootsOfUnity f ↑m).comp (TauCeti.PrimeToPTateModule.proj m)) ⋯

@[simp]

theorem TauCeti.PrimeToPTateModule.proj_map {p : ℕ} {E : Type u_1} [CommMonoid E] {F : Type u_2} [CommMonoid F] (f : E →* F) (x : PrimeToPTateModule p E) (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) : (proj m) ((map f) x) = (restrictRootsOfUnity f ↑m) ((proj m) x)

The components of map f x are the images under f of the components of x.

@[simp]

theorem TauCeti.PrimeToPTateModule.map_id {p : ℕ} {E : Type u_1} [CommMonoid E] : map (MonoidHom.id E) = MonoidHom.id (PrimeToPTateModule p E)

Mapping the identity homomorphism gives the identity on the prime-to-p Tate module.

@[simp]

theorem TauCeti.PrimeToPTateModule.map_comp {p : ℕ} {E : Type u_1} [CommMonoid E] {F : Type u_2} [CommMonoid F] {G : Type u_3} [CommMonoid G] (g : F →* G) (f : E →* F) : map (g.comp f) = (map g).comp (map f)

Mapping a composite of monoid homomorphisms is the composite of the induced maps on the prime-to-p Tate modules.

theorem TauCeti.PrimeToPTateModule.continuous_map {p : ℕ} {E : Type u_1} [CommMonoid E] {F : Type u_2} [CommMonoid F] (f : E →* F) : Continuous ⇑(map f)

The homomorphism of Tate modules induced by a monoid homomorphism is continuous.

@[instance_reducible]

noncomputable instance TauCeti.PrimeToPTateModule.instSMul {p : ℕ} {E : Type u_1} [CommMonoid E] {M : Type u_2} [Monoid M] [MulDistribMulAction M E] : SMul M (PrimeToPTateModule p E)

A monoid acting on E by multiplicative maps acts on the prime-to-p Tate module componentwise. For the absolute Galois group of a field acting on a separable closure E, this is the action recorded by the Tate twist (1) in ℤ̂^{(p')}(1).

Equations

• TauCeti.PrimeToPTateModule.instSMul = { smul := fun (g : M) => ⇑(TauCeti.PrimeToPTateModule.map (MulDistribMulAction.toMonoidHom E g)) }

theorem TauCeti.PrimeToPTateModule.smul_def {p : ℕ} {E : Type u_1} [CommMonoid E] {M : Type u_2} [Monoid M] [MulDistribMulAction M E] (g : M) (x : PrimeToPTateModule p E) : g • x = (map (MulDistribMulAction.toMonoidHom E g)) x

The action of g on the prime-to-p Tate module is the map induced by the action of g on E.

@[simp]

theorem TauCeti.PrimeToPTateModule.coe_proj_smul {p : ℕ} {E : Type u_1} [CommMonoid E] {M : Type u_2} [Monoid M] [MulDistribMulAction M E] (g : M) (x : PrimeToPTateModule p E) (m : { m : ℕ // m ≠ 0 ∧ m.Coprime p }) : ↑↑((proj m) (g • x)) = g • ↑↑((proj m) x)

The components of g • x are obtained by letting g act on the components of x.

@[instance_reducible]

noncomputable instance TauCeti.PrimeToPTateModule.instMulDistribMulAction {p : ℕ} {E : Type u_1} [CommMonoid E] {M : Type u_2} [Monoid M] [MulDistribMulAction M E] : MulDistribMulAction M (PrimeToPTateModule p E)

Equations

• TauCeti.PrimeToPTateModule.instMulDistribMulAction = { toSMul := TauCeti.PrimeToPTateModule.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_one := ⋯, smul_mul := ⋯ }

instance TauCeti.PrimeToPTateModule.instContinuousConstSMul {p : ℕ} {E : Type u_1} [CommMonoid E] {M : Type u_2} [Monoid M] [MulDistribMulAction M E] : ContinuousConstSMul M (PrimeToPTateModule p E)