subobjects as monomorphisms

Stream: mathlib4

[Julien Michel]

I was reading through some files about inner product spaces. There seem to be some conflicting design philosophies here and there. For example Basis and OrthogonalFamily are defined in terms of morphisms rather than specific elements. But many algebraic Sub-things are defined with a carrier set in the traditional way. Shouldn't they be defined in terms of injective morphisms ? Or is it a bad idea ?
For example, I'm thinking that one could define a Subgroup in this way: (Maybe it's not the best design)

structure Subgroup' (G : Type*) [Group G] (K : Type*) [Group K] where  -- (maybe as a class?)
  hom : K →* G
  injective : Function.Injective hom

Would there be issues with defining all Sub things in a similar way? Would that help making things more elegant?

[Johan Commelin]

With that approach, Subgroup G would no longer be a lattice.

[Johan Commelin]

One is almost never interested in the structure of all bases of a vector space, but a single specific basis should be as flexible as possible.

[Johan Commelin]

Otoh, the structure of all subgroups is quite interesting.

[Johan Commelin]

This informs these different design approaches.

[Julien Michel]

What about this ?

structure Subgroup'' (G : Type*) [Group G] where
  K : Type*
  is_group : Group K
  hom : K →* G
  injective : Function.Injective hom

[Johan Commelin]

Still not a lattice

[Adam Topaz]

import Mathlib

open CategoryTheory

variable (X : GroupCat)

#synth (Lattice (Subobject X)) -- fails

:halo:

[Adam Topaz]

oh that's not right.

[Julien Michel]

Are you sure it wouldn't be possible to make that into a lattice by embedding the subgroups into the target group, to give back meaning to intersection and union generated subgroups? (but I guess you're gonna say then just define a subgroup inside its carrier group )
Do you know results in mathlib that uses the lattice of subgroups ? I'm not familiar with their usage, and how frequently they are used

[Adam Topaz]

At least

import Mathlib

open CategoryTheory

variable (X : GroupCat)
#synth (PartialOrder (Subobject X))

works.

[Adam Topaz]

it is possible to give a lattice structure. But the main issue is that these wouln't be very convenient to work with.

[Julien Michel]

I guess. That's why I'm wondering if that's a frequent use case

[Adam Topaz]

note that with your definition, you will not get a lattice as Johan said. You need to mod out by isomorphisms at some point to get a lattice.

[Julien Michel]

Ok then I suppose it adds even more inconvenience

[Adam Topaz]

if you want to experiment a bit, I would focus on the case of subsets first.

[Johan Commelin]

@Julien Michel Intersections of subgroups are everywhere. A particularly nice statement involving the order structure on subgroups comes from Galois theory. But there are many more examples (although they don't have catchy names).

[Julien Michel]

Right, so more basically being able to conveniently intersect things is important.

[Adam Topaz]

Not really related to this, but the reason that #synth (Lattice (Subobject X)) fails when X : GroupCat is because of the following, which should be fixed at some point:

import Mathlib

open CategoryTheory Limits

#synth HasPullbacks GroupCat.{0} -- ok
#synth HasBinaryCoproducts GroupCat.{0} -- fails
#synth HasImages GroupCat.{0} -- fails

[Matthew Ballard]

Aren’t these marked subgroups or something?

[Matthew Ballard]

Or maybe framed?

[Adam Topaz]

I think “framed” would be more like specifying generators of the subgroup. I don’t think I’ve seen such a concept in nature.

[Matthew Ballard]

I think about the distinction between GW invariants vs actual curve counts (not directly applicable I know)

[Patrick Massot]

Julien, the sup operation is also crucial. The whole story of generated subgroups in framed in this lattice mindset.

[Patrick Massot]

Did you read the discussion at https://leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html#subgroups?