CompleteGroupAlgebra

Stream: Is there code for X?

[张守信(Shouxin Zhang)]

Consider the traditional definition of the completed group algebra, I ended up trying the following Lean 4 code implementation:

import Mathlib

open CategoryTheory Opposite

universe u v

variable (G : ProfiniteGrp.{u}) (R : Type v) [CommRing R]

noncomputable def completeGroupAlgebraFunctor : OpenNormalSubgroup G ⥤ AlgebraCat R where
  obj N := AlgebraCat.of R (MonoidAlgebra R (G ⧸ N.toSubgroup))
  map {N₁ N₂} (f : N₁ ⟶ N₂) :=
    AlgebraCat.ofHom <| MonoidAlgebra.mapDomainAlgHom R R <|
      (QuotientGroup.map N₁.toSubgroup N₂.toSubgroup (MonoidHom.id G) f.le)
  map_id := by simp
  map_comp {X Y Z} f g := by ext x y; simp

noncomputable abbrev cGA := AlgebraCat.HasLimits.limitCone (completeGroupAlgebraFunctor G R)

Is this correct? I'm a bit unsure if mathematically it should be (OpenNormalSubgroup G)ᵒᵖ ⥤ AlgebraCat R. Clearly, it's mathematically unlikely to construct a functor (OpenNormalSubgroup G)ᵒᵖ ⥤ AlgebraCat R. But how do we represent the 'inverse' nature of the inverse limit?

[Kevin Buzzard]

What a mathematician calls an "inverse limit" we just call a "limit" in Lean, so take the limit :-)

I think you're right that the functor is covariant. If you added "op" then for two normal subgroups $N_1\subseteq N_2$ you would have to give a map from $R[G/N_2]$ to $R[G/N_1]$ and these maps would have to satisfy a bunch of axioms: good luck with that, I don't think you'd be able to fill in the sorries.

[Filippo A. E. Nuccio]

But in your definition you end up building the raw underlying ring without a topology, right?

[Jz Pan]

Filippo A. E. Nuccio said:

But in your definition you end up building the raw underlying ring without a topology, right?

I think the above definition itself has no topology if each piece AlgebraCat.of R (MonoidAlgebra R (G ⧸ N.toSubgroup)) has no topology given.

[Filippo A. E. Nuccio]

Sure, but

• if those pieces have a natural topology (eg coming from the coefficient ring) it would be important to store it
• even endowing each piece with the discrete topology, the whole "completed" group algebra c/would carry the projective limit topology.

[Jz Pan]

For maximal generality, I want R be only CommSemiring. Do we have analogue of AlgebraCat for Semiring? If not, then I think I have to drop category theory approach.

[Jz Pan]

@Nailin Guan

[Jz Pan]

Jz Pan said:

Do we have analogue of AlgebraCat for Semiring

Then ModuleCat also needs modification...

[Nailin Guan]

Those categories are far from good, if you insist having CommSemiring or even Semiring, I prefer to make a force construction and then verify it is limit in the good case.

[Jz Pan]

Nailin Guan said:

Those categories are far from good

I don't agree. The construction of limit does not require subtraction, so Semi is good enough.

[Nailin Guan]

It is about the category itself, not the construction.

[Adam Topaz]

SemiRingCat has all limits (just like any algebraic category)

[Jz Pan]

Adam Topaz said:

SemiRingCat has all limits (just like any algebraic category)

But it does not have algebra structure over a CommSemiring. What I want is SemiAlgebraCat which allow Semiring over a CommSemiring. I've played it a little bit at #24599 but seems that it breaks something.

[Adam Topaz]

what breaks? why don’t you just make SemiAlgebraCat as a new type

[Jz Pan]

Adam Topaz said:

what breaks?

Seems that some Ring instance is missing, or is not definitionally equal to the existing one.

why don’t you just make SemiAlgebraCat as a new type

Then I need to copy contents of 4 files from AlgebraCat folder...

[Jz Pan]

The first error occurred at Mathlib/Algebra/BrauerGroup/Defs, it complained that NonUnitalNonAssocRing carrier is not found:

universe u v

section test

variable (K : Type u) [Field K] (R : AlgebraCat.{v} K)

#synth NonUnitalNonAssocRing R.carrier -- This runs correctly

end test

/-- `CSA` is the set of all finite dimensional central simple algebras over field `K`, for its
  generalisation over a `CommRing` please find `IsAzumaya` in `Mathlib.Algebra.Azumaya.Defs`. -/
structure CSA (K : Type u) [Field K] extends AlgebraCat.{v} K where
  /-- Any member of `CSA` is central. -/
  [isCentral : Algebra.IsCentral K carrier]
  /-- Any member of `CSA` is simple. -/
  [isSimple : IsSimpleRing carrier] -- but here it complains `NonUnitalNonAssocRing carrier` is not found
  /-- Any member of `CSA` is finite-dimensional. -/
  [fin_dim : FiniteDimensional K carrier]

But in the test code above, #synth NonUnitalNonAssocRing R.carrier works correctly. So I don't know what's wrong in it.

[Christian Merten]

Depending on your application, it might be easier to put algebraic structures on docs#InverseSystem.limit instead (which we should have anyway). Especially if you want to have a topology on the limit, it is probably easier to hook up to the rest of the library if you don't go via category theory.

[Andrew Yang]

cf FLT#428

[Jz Pan]

Whoops, we already have inverse limits of sets in mathlib? That's cool. Seems that we also have direct limits of
various algebraic structures in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Colimit/DirectLimit.html but we don't have inverse limits of them yet.

[Jz Pan]

I've reinventing the wheel at https://acmepjz.github.io/lean-iwasawa/docs/Iwasawalib/Algebra/CompleteGroupAlgebra/Basic.html :man_facepalming:

[Adam Topaz]

Why does InverseSystem.limit use docs#Set.Iio ?

[Christian Merten]

Adam Topaz said:

Why does InverseSystem.limit use docs#Set.Iio ?

This is a question for @Junyan Xu. I think the original application is some cardinality result, which relates cardinalities of various "sub" limits.

In applications, we can just use WithTop and the limit at \top though.

[Adam Topaz]

yeah, but then you have to deal with going back and forth from WithTop, and in particular you need to specify where Top goes in F, which means you need some junk value...

[Adam Topaz]

I think using CategoryTheory.Functor.sections is the better approach if you want the "standard" type underlying the limit.

[Junyan Xu]

Before we generalize AlgebraCat maybe we should first generalize CategoryTheory.Preadditive and ModuleCat (they both require AddCommGroup now).
The error with IsSimpleRing in CSA is because TwoSidedIdeal currently requires NonUnitalNonAssocRing. TwoSidedIdeal is currently just a wrapper around RingCon, and I think we should redefine it to be {I : Ideal R // I.IsTwoSided} (they're the same over a ring by docs#TwoSidedIdeal.orderIsoIsTwoSided; for semirings there will be a map from RingCon R to TwoSidedIdeal R, and taking the RingCon generated by an ideal is a left inverse), but you'd need to generalize Ideal to allow non-unital and non-associative semirings to achieve the same level of generality. Or maybe we can drop TwoSidedIdeal and just use RingCon.

[Junyan Xu]

Why does docs#InverseSystem.limit use docs#Set.Iio?

yeah, but then you have to deal with going back and forth from WithTop, and in particular you need to specify where Top goes in F, which means you need some junk value...

My original motivation for introducing this is to carry out some transfinite recursive construction which requires taking the inverse limit at a limit ordinal (not dissimilar to the small object argument @Joël Riou carried out in a more categorical setting). Indeed in order to retrieve the final construction I needed to use WithTop (see Field.Emb.Cardinal.embFunctor).

[Junyan Xu]

I think it would be beneficial to generalize Direct/InverseSystem to use (co)filtered indexing categories instead of a preorder. This has been discussed in #mathlib4 > Directed systems @ 💬 and #23339 and #23364 are relevant PRs (indeed docs#DirectLimit may be redefined using the colimit type as Quot is almost as nice as Quotient when it comes to defeq, and we just need to show if the indexing category is filtered then equality in the quotient is given by the specific equivalence relation (CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_quot_rel)). Special cases like docs#InverseSystem.limit could be given a more specific name.

[Jz Pan]

Junyan Xu said:

The error with IsSimpleRing in CSA is because TwoSidedIdeal currently requires NonUnitalNonAssocRing

The question is that I think I already added the relevant instances (see the code above variable (K : Type u) [Field K] (R : AlgebraCat.{v} K); #synth NonUnitalNonAssocRing R.carrier which can be inferred correctly), but seems that it's not recognized by [isSimple : IsSimpleRing carrier].

[Jz Pan]

Andrew Yang said:

cf FLT#428

Interesting, the Algebra and AlgHom version is missing in that PR.

[Kevin Buzzard]

@Jz Pan please feel free to PR! I just merged that one. The review process in FLT is infinitely lighter than in mathlib, and both you and @Junyan Xu would be welcome to experiment. What we need in FLT is the existence of deformation rings. If we could get these before my talk at Big Proof on 9th June, this would be awesome!

[Jz Pan]

Kevin Buzzard said:

Jz Pan please feel free to PR! I just merged that one. The review process in FLT is infinitely lighter than in mathlib, and both you and Junyan Xu would be welcome to experiment. What we need in FLT is the existence of deformation rings. If we could get these before my talk at Big Proof on 9th June, this would be awesome!

In my https://acmepjz.github.io/lean-iwasawa/docs/Iwasawalib/Algebra/CompleteGroupAlgebra/Basic.html it's algebra version. The typeclass is automatically inferred from algebra structure of Pi (I use abbrev instead of def so the typeclass is passthrough). Also in my application I need the concepts of directed and cofinal/coinitial. It turns out that I also need inverse limit of general rings, not only group algebras, which I will refactor later.

[Junyan Xu]

What we need in FLT is the existence of deformation rings. If we could get these before my talk at Big Proof on 9th June, this would be awesome!

Are there some specific sorries for these?

[Kevin Buzzard]

The situation is that I had a student working on this, but unfortunately they have now got a job so have no time to continue. I'll ask them what the situation is.

[Kevin Buzzard]

ok so their WIP work is all in the WIP PR FLT#481 which will need a lot of disentangling (there are conflicts, and it's +2500, I'm currently trying to get it compiling), and the student will not be working on it any more.

[Notification Bot]

A message was moved from this topic to #FLT > Deformation rings by Kevin Buzzard.

[Jz Pan]

Do we have this in mathlib?

import Mathlib

open scoped TensorProduct

variable (R : Type*) [CommRing R] (G H : Type*) [Group G] [Group H]

noncomputable example : MonoidAlgebra R G ⊗[R] MonoidAlgebra R H ≃ₐ[R] MonoidAlgebra R (G × H) :=
  sorry

It should come from docs#finsuppTensorFinsupp.

Actually I need PiTensorProduct version. (Which is used to prove $\mathbb{Z}_p[[\Z_p^d]]\cong\mathbb{Z}_p[[X_1,\cdots,X_d]]$ from one-variable result.)

[Jz Pan]

Oh, there is a "TODO: generalize to MonoidAlgebra" in module docstring

[张守信(Shouxin Zhang)]

Jz Pan said:

Oh, there is a "TODO: generalize to MonoidAlgebra" in module docstring

I had Gemini generate a proof that looked like some trivial verification of the definition. If the infrastructure on lib was complete, I might be able to try to solve this problem. :grinning_face_with_smiling_eyes:

[Jz Pan]

We also don't have topology on MonoidAlgebra or Finsupp :man_facepalming:

[Jz Pan]

Topology on MvPowerSeries is via docs#MvPowerSeries.WithPiTopology.instTopologicalSpace

[Jz Pan]

So we even can't state there exists an isomorphism of topological rings $\mathbb{Z}_p[[\Gamma]]\cong\mathbb{Z}_p[[X]]$ (missing topological space structure on each piece $\mathbb{Z}_p[[\Gamma/\Gamma^{p^n}]]$)

[Jz Pan]

BTW, an unrelated note: seems that we don't have compact open topology (we don't need it yet), and it conflicts with the default instance docs#Pi.topologicalSpace Sorry, it's docs#ContinuousMap.compactOpen

[Kevin Buzzard]

$\Z_p[[X]]$ has got three distinct natural topologies on it ($p$-adic, $X$-adic, $(p,X)$-adic) and all are used in the literature, so it's not surprising that there are difficulties here in mathlib, where only one "canonical" topology is supposed to be allowed on any type.

[Jz Pan]

Kevin Buzzard said:

$\Z_p[[X]]$ has got three distinct natural topologies on it ($p$-adic, $X$-adic, $(p,X)$-adic) and all are used in the literature, so it's not surprising that there are difficulties here in mathlib, where only one "canonical" topology is supposed to be allowed on any type.

No worries, the docs#MvPowerSeries.WithPiTopology.instTopologicalSpace is scoped so it's not the only "canonical" one. It is the product topology, and in fact equal to the $(p,X)$-adic toploogy.

The point is that the polynomial ring $\Z_p[X]$ also has these 3 topologies, different one gives different completion ($p$-adic completion is $\Z_p\langle X\rangle$ while $X$-adic and $(p,X)$-adic completions are $\Z_p[[X]]$ --- only as a ring! as topological rings $X$-adic and $(p,X)$-adic topology are different). I need to use $X$-adic or $(p,X)$-adic completion, not sure.

... And we don't have topologies on polynomial rings yet, even scoped one.

[Kevin Buzzard]

Let's thnk about this question! For $\Z_p[[\Gamma]]\cong\Z_p[[X]]$ to be right I guess it boils down to the following question. Consider the obvious inclusion $\Z_p[[X]]\to\prod_n(\Z_p[X]/\left((1+X)^{p^n}-1\right)$. Give $\Z_p[X]/\left((1+X)^{p^n}-1\right)\cong\Z_p^{p^n}$ the only sensible topology; it's both the $p$-adic and the $(p,X)$-adic topology! It's also the $\Z_p$-module topology BTW. What is the induced topology on $\Z_p[[X]]$ as a subset of the product?

[Jz Pan]

Kevin Buzzard said:

What is the induced topology on $\Z_p[[X]]$ as a subset of the product?

It's the (p,X)-adic topology.

[Jz Pan]

Let's read my stupid blueprint (online version at https://acmepjz.github.io/lean-iwasawa/blueprint/sect0004.html#Iwasawa-alg-isom-finite-level)

2025-05-14 175617.png

2025-05-14 175645.png

2025-05-14 175708.png

[Jz Pan]

Kevin Buzzard said:

Consider the obvious inclusion

I think it requires Weierstrass division, fortunately it's already in an open PR.

[Jz Pan]

But that indeed looks promising. Maybe I can work out a version without topology first.

[Yakov Pechersky]

Do we have any instances that show that something is a Z_p module, other than the concrete Z_p[X] and the like?

[Jz Pan]

Yakov Pechersky said:

Do we have any instances that show that something is a Z_p module, other than the concrete Z_p[X] and the like?

You mean modules which do not start with $\Z_p$, for example inverse limits of $\Z/p^n\Z$? (Or in fact $\Z/p^n\Z$ itself is also a $\Z_p$-module.)

[Jz Pan]

Properties of (1 + X) ^ n - 1 is implemented in https://acmepjz.github.io/lean-iwasawa/docs/Iwasawalib/RingTheory/Polynomial/OneAddXPowSubOne.html.

[Kevin Buzzard]

@Jz Pan Re your blueprint proof, the sentence in the second screenshot starting "It's easy to see that..." is false (if I understood it correctly), e.g. 4 choose 2 is 6 and more generally p^n choose p^m will give you problems (as will other choices of i).

[Jz Pan]

Kevin Buzzard said:

the sentence in the second screenshot starting "It's easy to see that..." is false (if I understood it correctly)

Sorry, that's indeed incorrect. Will be fixed soon.

[Filippo A. E. Nuccio]

Jz Pan said:

But that indeed looks promising. Maybe I can work out a version without topology first.

This is indeed the approach taken by Serre Classes des corps cyclotomiques (Sém. Bourbaki, exp 174 ), Section 6: but a bit of topology is required to show that taking the limit gives an isomorphism.

[Antoine Chambert-Loir]

Jz Pan said:

... And we don't have topologies on polynomial rings yet, even scoped one.

Polynomials are function with finite unspecified support, so I believe the natural topology on polynomial rings would be the inductive limit topology of the product topologies on polynomials of given degree. At least that topology has the merit of making continuous the evaluation maps $R[X]\to R$, $f\mapsto f(a)$.

[Aaron Liu]

That's great! What's the topology on polynomials of a given degree?

[Kevin Buzzard]

I guess Antoine means "polynomials of at most a given degree", because these are just R^n with the product topology.

[Aaron Liu]

Then I think this gives you "the finest topology which makes Polynomial.update continuous"

[Aaron Liu]

I'm not sure how this makes the evaluation continuous... got my limits mixed up

[Jz Pan]

I think the question reduced to: what is the topology on docs#Finsupp (or docs#DFinsupp, i.e. coproducts of abelian groups)? Should it be the finest topology such that docs#Finsupp.single is continuous, or the coarsest topology such that docs#Finsupp.linearCombination (corresponding to evaluation maps for polynomials) is continuous?

[Jz Pan]

Note that the finest topology definition seems to be finer then the subspace topology of product topology.

[Jz Pan]

Seems that the coarsest topology definition is the correct one, see https://math.stackexchange.com/questions/5095/what-are-the-product-and-coproduct-in-the-category-of-topological-groups. But it said that "However, it is hard to describe this topology explicitly (and thus, for instance, proving separation axioms)."

Maybe I should stick to an ad-hoc scoped "piTopology"...

[Jz Pan]

Not that the second coarsest topology definition is at least as fine as the first finest topology definition, since you can consider the linearCombination into the first one.

[Kevin Buzzard]

Note that Andrew Yang's work on TopModuleCat has a generalisation of this: the adjoint to the forgetful functor from topological modules to topological spaces takes a type I with a topology and then gives a topology to the free module on I (which I couldn't figure out how to express directly). I maintainer merged the PR yesterday, sorry for no precise link, on mobile

[Kevin Buzzard]

#23490

[Antoine Chambert-Loir]

I had explained this property on my blog.

https://freedommathdance.blogspot.com/2024/04/the-topology-on-ring-of-polynomials-and.html

[Antoine Chambert-Loir]

This description is inspired by what is done for test functions in distribution theory. Evaluation is continuous, but I do not claim that it is the coarsest topology that would guarantee the continuity of evaluations. (Unless it is trivially true, I'd guess it unlikely to hold in general.)

[Aaron Liu]

It is not the coarsest topology that makes evaluation continuous, because some polynomials evaluate the same on all inputs

[Jz Pan]

I think it is the coarsest topology that makes linear combination continuous.