How do you formalise hierachies?

Stream: new members

[Mr Proof]

This is a question about categories, not really about groups as such:

Say I want to formalise the group SO(n)

So just like an element x of SO(n) I would write x:SO(n)
But I also want to express that SO(n), SP(n), etc. are lie groups. So I would want to write SO(n):LieGroup. Would LieGroup then be a Type 2?

But I don't think this is how it's done in Lean? Instead would I write a function
isLieGroup:Type->Prop

In other words, I'm just trying to understand how you formalise a hierachy such as A is_a B is_a C is_a D.
e.g. cat is_a mammal is_a animal is_a lifeform.

Secondly if I am defining an "is_a" function which I can define any way I like. I might accidentally add a circular definition e.g. A is_a B is_a C is_a A. And then it's Russel's paradox all over again. And wasn't the whole point of Type theory to avoid such paradoxes?

Perhaps the confusion is that : means "instance of" while "is_a" could also mean "member_of" or "subcategory_of". e.g. my pet cat is an instance of Cat. But Cat is a sub-category of Animal. But Cat is also an instance of the set of Animals.

[Michal Wallace (tangentstorm)]

a partial answer is that you can make a class and prove instance MyClass MyType.

I haven't yet been able to determine whether you can make one class imply (i.e, be a subclass of) another. my attempts so far have failed, but i remain hopeful. :)

[Michal Wallace (tangentstorm)]

oh, actually docs#LieGroup seems to answer both our questions:

class LieGroup{𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2}
 [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [Group G]
  [TopologicalSpace G] [ChartedSpace H G]
extends SmoothMul
 : Prop

[Mr Proof]

I have to be honest and say the Mathlib docs are largely impenetrable to me. :pensive:
I assume they are autogenerated from comments in the code.
Mainly I learn things from examples and the docs are just a list of definitions. Hopefully they will be updated at some point with fleshed out examples for each topic.

I sort of get the idea with classes. I'm just wondering how that's implemented behind the scenes so-to-speak. As I assume the classes are syntactic sugar for something else.

[Michal Wallace (tangentstorm)]

This definition is mostly impenetrable to me, too, but basically everything in parens is something you explicitly supply, and the ones in curly braces and brackets are like prerequisites that have to be true about the explicit ones.

For classes, you can click on the "Instances" expander thing underneath the definition in the docs, and then click the source link in the upper right to see the actual code.

[Damiano Testa]

I find that the online docs are good as a reference, but I would not try to understand how the code works by looking at the docs.

[Damiano Testa]

For mathematical concepts, such as a Lie group, the docs give you information about the concept, not so much the code.

[Damiano Testa]

In fact, looking at the code alone that Michal posted, already gives me a good idea:

[Damiano Testa]

G is "the" Lie group. Since it is manifold, it has charts, and the charts are modelled using some topological space H (likely ℝ^n or some other normed vector space), and since I mentioned ℝ, there had better be some normed field. That is k.

[Damiano Testa]

The actual def Is hidden in the fact that the type is Prop: this is going to be some compatibility of all these structures.

[Edward van de Meent]

Michal Wallace (tangentstorm) said:

I haven't yet been able to determine whether you can make one class imply (i.e, be a subclass of) another. my attempts so far have failed, but i remain hopeful. :)

there are generally three ways:

1. use extends, i.e. class MyClass extends YourClass.

   • you can use this when all non-automatic parameters in MyClass also occur in YourClass. Looking at the mathlib doc you sent, you can't just extend Group G because Group G doesn't depend on 𝕜, while LieGroup does, meaning 𝕜 is not automatic

2. use an instance parameter

   • I can't think of anything that could go wrong with this from the top of my head, but the type signature can get very unwieldy this way.

3. make an explicit instance.

   • this is very similar to option 1, but can be used to make a combination of classes imply another, meaning it is slightly more general. i believe this also has the parameter restriction of that option, but i'm not certain.