Products of nonarchimedean groups and rings

An arbitrary product of nonarchimedean groups is nonarchimedean, and likewise for rings. Mathlib has only the binary case, Prod.instNonarchimedeanGroup; these are the Pi analogues, stated over an unrestricted index type.

No finiteness hypothesis is needed. A neighbourhood of the identity in the product topology contains a box that constrains only finitely many coordinates, so shrinking those finitely many factors to open subgroups and leaving the rest unconstrained produces an open subgroup inside it.

These live in the Pi namespace of the construction they describe rather than in a TauCeti one, following TauCeti/Topology/Algebra/Nonarchimedean/Completion/Basic.lean.

Main results

• Pi.instNonarchimedeanGroup: a product of nonarchimedean groups is nonarchimedean, together with its additive version Pi.instNonarchimedeanAddGroup.
• Pi.instNonarchimedeanRing: a product of nonarchimedean rings is nonarchimedean.

Implementation notes

Mathlib's library_note «non-Archimedean non-instances» explains why the subgroup basis lemmas cannot be instances: they would send typeclass search after an @IsTopologicalAddGroup β ?m1 ?m2 whose topology and group structure are both unknown. That obstruction does not arise here, since every structure on ∀ i, G i is fixed by the corresponding Pi instance, which is also why Mathlib states the binary case as an instance.

References

• Mathlib's Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean, whose Prod.instNonarchimedeanGroup these generalise.

instance Pi.instNonarchimedeanGroup {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), NonarchimedeanGroup (G i)] : NonarchimedeanGroup ((i : ι) → G i)

A product of nonarchimedean groups is nonarchimedean.

instance Pi.instNonarchimedeanAddGroup {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), NonarchimedeanAddGroup (G i)] : NonarchimedeanAddGroup ((i : ι) → G i)

A product of nonarchimedean additive groups is nonarchimedean.

instance Pi.instNonarchimedeanRing {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Ring (R i)] [(i : ι) → TopologicalSpace (R i)] [∀ (i : ι), NonarchimedeanRing (R i)] : NonarchimedeanRing ((i : ι) → R i)

A product of nonarchimedean rings is nonarchimedean.