Modular Group as a mutual inductive type

[lane-core]

This is a construction of the Modular Group PSL2(Z) utilizing a mutual inductive type. I will quote from the preamble of the Type declaration to contextualize the formalization presented here. This will serve as a base for future modules I will be adding to this folder.

To summarize the construction, we have E and S on the 𝓢 side, with little S
taking elements from the other type 𝓡. Then we have little R and R² in 𝓡,
taking elements from 𝓢 to construct its members; hence 𝓡 is strictly
dependent on 𝓢, and 𝓢 has the zero-level constructors, while successors for
both must be strictly alternating between types. Having a canonical S and E,
we obtain canonical representations of the words R/R² by right-composition
with the identity element. Thus we can form SR/SR² and R²S/RS evidently,
and achieve the ability to form every possible word in PSL₂ℤ generated by
the elements S and R in this type in irreducible form. Also to note, we can
interpret the action of η and θ constructors as essentially a representation
of the identity element from the left rather than the right side. The overall
methodology I pursued was to keep as few cases as possible for each branch
of pattern matching, so as to express the most efficient construction possible.

My overall intentions for this series of modules is as follows:
 1. Provide a base for research into the formalization of the Modular Group
  by purely synthetic/symbolic methods; 𝓜 can then be composed with other
  types to research specific fields of interest
 2. Studying the relationship between modular forms and Gosper's bihomographic
  algorithm originally presented in his continued fraction arithmetic paper
 3. On the basis of (2), develop a new formalization of rational and real
  arbitrary-precision arithmetic with a type formalized along the lines of
  Bertot and Niqui's work in the QArith libraries. Where the approach will
  differ here is the use of symbolic rather than analytic methods of
  computing that arithmetic, acting directly upon symbolic representations
  of matrices in 𝓜 and canonical representatives in ℚ or ℝ rather than
  translating between them and natural number or integer types.
 4. Investigate whatever connections are appropriate for the subjects pursued
  above with Univalent mathematics in general.

[martinescardo]

Thanks. I'll ask @UlrikBuchholtz to help to review this.

[lane-core]

Thank you!

[martinescardo]

Here are some requests and suggestions before @UlrikBuchholtz completes his review:

• In order to convince Ulrik and me that you did implement the modular group, and not some random group, I think you should state and prove its universal property, namely that it is presented by generators S and T and relations S^2 = 1 and (ST)^3=1, as discussed here.

  In TypeTopology you can state this by saying that for any other group G with elements s and t satisfying the above identities there is a unique homomorphism from your group to G that maps S to s and T to t. I guess you have already developed enough material here to be able to prove this (you already have some induction principles which are close to this). I suggest that you add a new file UniversalProperty with this.

• Please move the whole tree ModularGroup from source to Groups.

• Please add an index file inside the directory ModularGroup. In that index file, add a brief explanation in English saying in which order the files should be read, and briefly mentioning what they do (for example, you can follow the convention of the file Quotient.index).

• Please import ModularGroup.index from Groups.index.

• I will have more mundane suggestions later in my own review of the code.

Thanks!

[lane-core]

I will be working on this! Thanks.

[martinescardo]

Maybe the directory ModularGroup can be renamed to just Modular, given that it will be imported as Groups.Modular if you move it to Groups.

[lane-core]

Two things:

1. Would you like me to use the Group definition of is-hom to do so (in which case I'm using the Group instance of the modular group to conduct the proofs), or may I follow the example of CoNaturals.UniversalProperty and define the type of homomorphisms directly from 𝓜 to the arbitrary Group?

2. Some time after submitting this PR I realized that there could be a fair generalization of my mutual inductive definition of the modular group to Hecke groups, namely by using a single constructor on the R side that is labeled by an element of Fin n (where the chosen 'n' identifies a specific Hecke group). I can finish my formalization work here, but if this is something I want to take on I'd be thoughtful about how techniques I develop for the Modular Group in these series of modules can be generalized to the Hecke groups.

[martinescardo]

1. Please use the Group definition of is-hom.
2. There are lot of instances in TypeTopology where we first proved something, and then something more general (an example is InjectiveTypes.MathematicalStructures and InjectiveTypes.MathematicalStructuresMoreGeneral). I am in favour, in your case, of doing the same thing.

[martinescardo]

Just to make official what I requested before: please state and prove the universal property before we review this in more detail. Thanks.

[lane-core]

just to update you on the status, I've started work on this. so far I've defined an induction principle based on generators S and T (T being defined as SR, which reduces to T in this representation). I've used it to define a function from Group PSL2Z to an arbitrary group, and it has the requisite is-hom properties. For fun I also defined one by case matching instead of the induction function and shown functional equivalence between the two. I am now where I must prove uniqueness, and this is the point where I have to become clever because I am actively expanding my knowledge at this stage. I'll submit a force push when its ready.

[martinescardo]

I wonder if there has been any progress regarding the work of this PR.

[lane-core]

Yes I will submit an update by this week

[lane-core]

Wanted to give a quick update, I did a lot of refactoring of my Universal Property file, I am currently running into an issue when I assume an arbitrary hom f of a group G. I must prove that f converts our canonical S into our S from G, but try as I might to use the homomorphism property of f, I cannot split up our S such that applying the homomorphic property does not just recreate the original proof goal (after eliminating the unit that is generated from splitting S into S * E. Would you have me update the PR with the current state of the proof?

[martinescardo]

Sure, you can update the PR!

[ayberkt]

Any updates on this @lane-core?

[lane-core]

Hi @martinescardo, I realize I've left this PR open even after promising to complete the required revisions; I hope that you won't mind the length of what follows, but I want to write a thoughtful summary of my experience and what my endeavors eventually led to, which I hope explains and mitigates my considerable absence somewhat. Don't think for a moment I wasn't appreciative that you were interested in reviewing this contribution. Rather I hope you'll agree with me that that the path I was led onto will be much more fruitful for any future contributions I might submit towards your consideration in the long run; I am deeply interested in your thoughts on the below, specifically towards the end, because I am aware of work of yours that touches upon exact real arithmetic, and I've been able to surmise some interesting connections here due to my idiosyncratic journey in this subject.

To summarize where I left off working on this PR: my difficulty began when I found that I could prove most of the cases required to show an equivalence between types, except for the base case, where I had hit a wall. I had proven a lemma of the form:

hom-is-prop : (f : Γ → 𝔾) → is-prop (is-hom PSL₂Z G f)
where Γ is my mutually inductive type and 𝔾 is the generic group presented by generators and quotient identities

I had shown that the homomorphism between the group characterized by the generators S, T along with their corresponding quotienting axioms and my construction was a unique map. However when it came to being able to show:

Γ-homo-is-unique : ∃! f ꞉ (Γ → 𝔾) , is-hom PSL₂Z G f

I found certain difficulty. I had chosen an unfortunate approach, which was to try to derive straightaway that f = h where h was the map from 𝔾 → Γ. To do that require me to define some lemmas:

f-S : Π x ꞉ Γ , f (s (x)) ＝ ｓ (f x)
f-T : Π x ꞉ Γ , f (t (x)) ＝ ｔ (f x)

where the special character letters are functions encoding left-composition of their corresponding symbols in the generic group. The snag was: due to my choice of having two base unit constructors in my type, namely E and S, I was playing ring-around-the-rosie trying to demonstrate the base cases for all these lemmas. An immediate solution was obvious: refactor the type so that we have a canonical unit constructor upon which we layer the other (mutual) constructors, and then this issue goes away. Then I'd rewrite the modules, which I foresaw would be a bit tedious but trivial given the familiarity I gained with this sort of construction.

I was not satisfied with an immediate solution however. I saw that my hack-and-slash adventures with type theory had reached a limit, and that it was better for me to digest a more sophisticated approach to the subject. Namely, catching up to the big ideas in univalent mathematics and to thoroughly digest the fundamentals of homotopy type theory beyond elementary DTT, which has been enriching, illuminating, and deeply fascinating.

An important and influential line of investigation on my part has come from attempting to understand certain constructions from graphical theories of computation, specifically the school of Lafont, Mazza, and so on, applying thinking from HoTT in this domain in relation to the new potential interpretations given to the aspects of proof theory that these graphical methods generalize. This has been a fruitful and lively avenue for me to investigate, and it is currently leading me towards an exploration of Braided/Ribbon categories in particular.

As I began to imagine the possible ways to investigate my current focus of research, I was reminded me of this pull request. I observed that this construction as an instructive and elementary example that will benefit from a certain approach I've stumbled onto. This week I will recode this set of modules, and soon after I'll continue onto Hecke Groups-- specifically because the notion of a mutually inductive type generating a universe of elements by constructors formed with vectors (Fin i -> Hecke j for some i, j), whose target is its own ever-expanding domain, forms an intriguing example for me to explore at the present moment.

Forgive me if I am just rediscovering some observation in a paper I don't know of yet, in which case, kindly point me to that direction if anything comes to mind, but I'd share my current thinking on this specifically to see if anything comes to mind for you: I believe there is a way to interpret Hecke groups that offers illuminating analogies for fundamental concerns in type-theoretic semantics, and can serve to connect this field to the rich literature on Modular/Hecke groups.

To start with, lets examine the action of S, and consider this thought experiment: we begin by interpreting S as an interpretation of not in the booleans, which has the quality that composing it twice gives the identity in PSL2Z. Now lets turn to consider the action of S in SL2Z, which has the quotienting rule equating S^4 to the identity. I believe that one can interpret the S generators here as 2-braids in a 3-dimensional space, where:

S ~ not: 0 crosses under 1
S^2 ~ id: 0 crosses under 1, which crosses over back to 0; note that the twisting here has the characteristic that one cannot pull the wires back to being straight, they are threaded between each other.

While S^2 is observationally equivalent to id from the perspective of the signal traversing the wire, in the ambient context one can strictly distinguish a signal traversing this pathway's twists from that path taking no twists. We achieve a return to the original identity by the time we reach S^4 if we interpret S^3 as an application of an unraveling where we pull the wire back and under, and do so again at S^4 such that we are left with a pair of parallel wires; this now expresses S^0 = id in the appropriate sense. Likewise, if we are to begin from some word whose head is T and left-compose it with S^-1, we would perform a twist of 1 under 0, with an analogous procedure for computing the action of the positive S^1 inverse to this negative S^-1. (to be honest, I think there is another, perhaps more accurate way of presenting this inverse twisting, but I'm presenting this way for simplicity, and because I'd like to work out how that works) So here we see an interpretation of PSL2Z as a truncation of this 3rd dimension to 2 dimensions, where twisted wires are free to be pulled back to running parallel.

There is a degree of subtlety for how to characterize the action of ST in this interpretation. I believe the answer lies in interpreting the fact that elements of Hecke group q are isomorphic to the products of the cyclic groups 2 and q. Fundamentally, each word may be interpreted within an ambient space of braidings between indices numbered up to 2 * q (in the modular group's case, we consider braidings from Fin 6 -> Fin 6, as the group is isomorphic to C2*C3 -> C2*C3).

For simplification of this interpretation, let's return to the Modular Group case (PSL2Z).

In the Monoid composed by these group elements, each of the words actually demarcates a specific linear path taken through this chain of composed elements, which are interpreted here by string diagrams expressing braidings/permutation sets between the elements of C2*C3 formed by unique compositions of S, R. Or in other words, we consider a subset of the automorphisms of C2*C3 (of some number of twists parallel composed with id2, with the twisted braiding in one of three positions and the trivial braids filling the other slots). But there is another way to characterize what is happening here: we consider that what we have here are mutually paramaterized diagrams, which on one side is a 2-braid whose wires are paramaterized over 3-braids; this is the "S" side. Vice versa on words whose head is R we can turn to consider 3-braids whose wires are paramaterized over 2-braids.

Under this interpretation, we see very well why we can form a canonical presentation of elements in PSL2Z: because the twists/braidings are in a 2d space, there is only one way to arrive at a given word which expresses a specific path comprised of various twists and untwists along these mutually paramaterized diagrams, and this is exactly why the composable words in PSL2Z can be shown to form a set. Whereas, I conjecture based on the immediate implication of this characterization I've presented, SL2Z may be most elegantly presented by a type that forms a higher hlevel than a set, because there are a number of distinct presentations in the monoid corresponding to the 'same sort' of semantic object. This is due to the fact that its twists are formed in a 3d space in contrast, such that there are multiple nontrivial paths to the same 'state' or semantic element. In other words, we can place each word in an equivalence class of semantic elements (and it is these equivalence classes which form the set given by the group SL2Z). Each of the elements of the equivalence class is related by an invariant property, and one may arrive at some representative within this equivalence class beginning from any root word. Put another way: the number of ways that

The richer structure of SL2Z a propos PSL2Z is due to the fact that one has multiple pathways to each of these classes beginning from any specific state. This multiplicity is necessitated because the action of elements in SL2Z specifically serves to braid the wires in such a way that they cannot be untangled unless one applies an on-the-nose inverse to undo the actions that led to the state presented by a given word in SL2Z. I consider it analogous to how one can compute arithmetic operations between any particular element of the integers in the arithmetic defined by the equivalence class construction, no matter what particular representation within each equivalence class one chooses, but in a strict sense one distinguishes between (p, q) and (p + 1, q + 1). SL2Z enumerates all the elements of the equivalence class, while PSL2Z is the semantic set denoted by these classes.

It's exactly why we can characterize any path with a unique matrix: the integer entries of this matrix are themselves interpretable as representatives of an equivalence class, so we have a family of matrices of the form [(a + j) (b + k); (c + l) (d + m)] corresponding to any [a b; c d] where the constraint imposed on j, k, l, m is that they must be of a form that does not move a, b, c, d outside their respective equivalence classes and which preserves determinant 1. The operation of both constraints together preserves an upper bound for the possible words which presents a given semantic element expressible in this group. I have evidence that this kind of procedure is possible in every case I've attempted thus far, but what began me learning HoTT was needing to learn more sophisticated methods to derive a general recursive procedure. I would go into more detail on this point but this is getting long enough as it is.

I'd rather draw your attention to this: this analogy suggests that we can characterize PSL2Z as the set truncation of SL2Z in the univalent sense. It also has the benefit of relating this family of Hecke groups deeply to the graphical theories I mentioned earlier; in fact, under this interpretation you'd have that certain PROs present a sort of 'degenerate' case of Hecke Groups, because, for example, in interaction nets we can characterize the diagram generated by elementary commutation rewrite rule of the interaction of opposite nodes as a function composed by the parallel composition id1 + not + id1, a morphism from 4 -> 4. And well, if this all works out to be a good interpretation, my current research suggests that we would immediately have a pathway towards applying the graphical methods of this discipline to the mathematical objects under consideration in this PR, and even to more fundamental matters in type theory than that. Albeit, I don't feel confident enough in the clarity of my present results to speculate about those possibilities at the present moment without progressing a little farther in this research trajectory of mine.

Given the above meditation I am tempted to begin straightaway with formalizing Hecke groups under the lines I've indicated above, refactoring my presentation the modular group as a specific case in which I apply general lemmas from the former. So consider that I am resuming work on this PR, but I'm curious about your thoughts on the above given the realms I know your work has explored in the past and presently as well. Specifically, I wonder if you might discern some relation to your work on Discrete Graphic Monoids that I saw in the repo.

Finally, thank you for reading this comment, which turned out to be much longer than I initially expected.

[martinescardo]

Thanks for the discussion. I am happy for you to take the approach you suggest, if you think it will be more fruitful.

I am pinging @UlrikBuchholtz in case he has something to remark about this.