Large groups

[lowasser]

Real addition will give us our first large group, but we have to define what that looks like.

The biggest issue I see is the inverse laws: if x : type-Large-Group G l, and neg-Large-Group G x : type-Large-Group G l, then we have to express that mul-Large-Group G x (neg-Large-Group G x) is the identity, but we have a few options:

1. An identity exists at every universe level.
2. The group has to come equipped with a mechanism for raising any element's universe level.
3. We accept some notion of similarity, and bake that into the group. As a corollary, we need to show that similarity is preserved by the group operation.

I suppose 2 comes with a free 3, but nevertheless, we should probably figure out what this should look like.

[EgbertRijke]

I'd keep the definition as simple as possible. A large group is a large semigroup equipped with a unit element at lzero and an inverse function that preserves the level, satisfying the usual axioms of a group.

All other stuff is reasonable to put on as extra structure, but you can define structured large groups for when you incorporate those.

[lowasser]

What axiom is it that the inverse function satisfies?

It can't be that e.g. mul-Large-Group G x (inv-Large-Group G x) = unit-Large-Group G, because the left and right sides of that equation are at different universe levels. That's the problem I'm getting at.

[lowasser]

(My suggestions above are all attempts at "what is the simplest way to resolve this issue," which are less simple than I'd like, but I don't yet have better ideas.)

[lowasser]

Drilling down to a particular example: you can show {l : Level} → (x : ℝ l) → sim-ℝ (add-ℝ x (neg-ℝ x)) zero-ℝ, but they're not equal, because add-ℝ x (neg-ℝ x) : ℝ l and zero-ℝ : ℝ lzero. So you either have to bake a notion of similarity into the definition of the group, or...one of the other alternatives, having an identity at every universe level, or a notion of raising universe levels, or something I'm not seeing.

[EgbertRijke]

That's a very good point!

One could introduce large monoids first, have a predicate on the elements of large monoids that they are multiplicative units, and then states that xx^-1 is a multiplicative unit.

This would avoid having to introduce level raising operations and sameness relations across levels.

But the issue with this is that the predicate of being a multiplicative unit is a large predicate

[fredrik-bakke]

That's a very good point!

One could introduce large monoids first, have a predicate on the elements of large monoids that they are multiplicative units, and then states that xx^-1 is a multiplicative unit.

This would avoid having to introduce level raising operations and sameness relations across levels.

But the issue with this is that the predicate of being a multiplicative unit is a large predicate

Does it follow from this that units are unique, and that raising a unit is still a unit? I think that should be true in a large group, so that what you have isn't just a sequence of groups indexed by universes.

My instinct would be to add a large equivalence relation to the structure, require that every pair of units are similar, and ask that the equivalence relation is "semitorsorial". I.e., that for every y : G l1, is-prop (Σ (x : G l2), (x ~ y))

[fredrik-bakke]

On closer thought, I would also expect a "large group" to have group monomorphisms G l1 -> G (l1 u l2), so maybe it's better to just call what you have a "stratified large group" and forget about all the extra coherence conditions?

[lowasser]

The presence of that group monomorphism implies something I don't think follows from the usual group axioms exactly: the existence of elements at each universe level.

I don't hate the approach of stratification that at every universe level a group is formed, but I do think some coherence conditions are called for.