Sets vs Structures

Stream: new members

[Luna]

Why are sets defined as a function instead of the following?

structure Set (α : Type _) (P : α → Prop) where
    val : α
    prop : P val

Defining sub-algebraic structures (e.g. subgroups, etc) seem to be easier using this definition, since the set itself is a type instead of a term.

[Kyle Miller]

The general idea is that Set is a type that lets you do set operations (like unions, intersections etc) and then there is a coercion to docs#Subtype (your type) when you want to treat the set as a type, which doesn't have a good way to have these operations.

This is used heavily by algebraic subobjects. The carrier set is coerced to a type when the subobject is treated like an object.

[Luna]

Ok that makes sense. So why does Mathlib opt to create "sub-" versions of algebraic structures instead of interpreting Group (Subtype P) as a subgroup? Is it just preference or is there a technical benefit to create individual "sub-" classes for each algebraic structure?

[Luna]

Also just out of curiosity, is there a way to abuse the notational system in lean to accept (a : (Set P₁) ∩ (Set P₂)) where intersection is given by

def Set.inter := Set (fun a => (P₁ a) ∧ (P₂ a))

[Jireh Loreaux]

One of the important reasons to have e.g., Subgroup, is that there is a natural lattice structure on this type. Likewise for other subobject classes. Moreover, morphisms in the relevant categories will act on these subobjects too. In short: we don't care only that subgroups are groups, but about many more things besides.

[Kyle Miller]

Luna said:

instead of interpreting Group (Subtype P) as a subgroup?

This is basically what mathlib does in the end to give subgroups a group structure. The way it works is that is that given S : Subgroup G, then there's a Group (Subtype S.carrier) structure.

[Luna]

Ah! That makes sense. I was just expecting the definition of a Subgroup to be the following:

class Subgroup {G : Type _} (S : Set G) extends Group (Subtype S)