Post #1905730

@pamorim That's one way to define it but that requires defining the Cartesian lifts from the start. You can also directly define a displayed category of subgroups as having an object S over a group G being a subgroup and then a displayed morphism over a homomorphism phi : G -> H from S over G to T over H to be a proof that for all s in S. phi(s) in T. Then Cartesian lifts have a universal property in this displayed category. More generally you can define e.g. a displayed category of monomorphisms over any category. I like the perspective of the displayed category first because there's something slightly non-trivial in defining the Cartesian lift: you have to prove that the inverse image phi^*(T) is actually a subgroup not just a subset. And for the general monomorphism case you can define the displayed category of monos even if the category doesn't have the pullbacks you need to define the inverse image