Implementation sublattice related to subgroup

Stream: general

[Matúš Behun]

Hello, I am working on my diploma thesis. I am trying to implement sublattice definition into mathlib library. I have noticed in subgroups that they are not built on groups but on monoid. Why is it better to build definition of subgroup on monoid rather than group. Should I code sublattice definition based on semilattice_sup and semilattice_inf rather than lattice?

[Alex J. Best]

Are you looking at https://github.com/leanprover-community/mathlib/blob/362619ebc74073495414578128b9bcb10879aa57/src/group_theory/subgroup.lean#L91 ? A subgroup is a special case of a submonoid (its one for which inversion fixes the subset). So by extending submonoid you allow yourself to apply any lemmas already proved about submonoids to subgroups as well.

[Matúš Behun]

Alex J. Best said:

Are you looking at https://github.com/leanprover-community/mathlib/blob/362619ebc74073495414578128b9bcb10879aa57/src/group_theory/subgroup.lean#L91 ? A subgroup is a special case of a submonoid (its one for which inversion fixes the subset). So by extending submonoid you allow yourself to apply any lemmas already proved about submonoids to subgroups as well.

Yeah, but group is build on monoid too so I could make subgroup by extending group and just find subset. At the end I would like to contribute to mathlib so if there's no reason not to build sublattice on lattice I can do it that way.

[Alex J. Best]

There is quite a difference in mathlib between groups and subgroups of given groups (they are different types), so I'm not sure you mean by extending group and finding subset. You could define subgroups of G to be groups H together with an injection from H to G but that makes it slightly harder to phrase concepts such as elements of G being in H, different subgroups being equal, or counting the number of subgroups of a given type.

[Matúš Behun]

Alex J. Best said:

There is quite a difference in mathlib between groups and subgroups of given groups (they are different types), so I'm not sure you mean by extending group and finding subset. You could define subgroups of G to be groups H together with an injection from H to G but that makes it slightly harder to phrase concepts such as elements of G being in H, different subgroups being equal, or counting the number of subgroups of a given type.

Oh I see, okay I probably need more time to look at it and then make it wrong way and make it right again. Thanks for pointing out potential problems.