subobject predicates

Stream: general

[Oliver Nash]

I'm trying to decide if I should introduce a predicate is_lie_submodule (in the course of formalising some basic facts about normalizers of Lie subalgebras).

Simplifying my situation, I'm looking for opinions on whether I should prefer is_lie_submodule_iff_exists or is_lie_submodule_iff_exists' in the snippet below:

import algebra.lie.submodule

universes u v w

variables {R : Type u} (L : Type v) {M : Type w}
variables [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M]
variables [lie_ring_module L M] [lie_module R L M]
variables (p : submodule R M)

/-- Is it helpful to introduce this? -/
def submodule.is_lie_submodule : Prop := ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p

lemma lie_submodule.coe_submodule_is_lie_submodule (N : lie_submodule R L M) :
  (N : submodule R M).is_lie_submodule L := N.lie_mem

lemma submodule.is_lie_submodule_iff_exists :
  p.is_lie_submodule L ↔ ∃ (N : lie_submodule R L M), ↑N = p :=
begin
  split,
  { intros h, use { lie_mem := h, ..p }, exact lie_submodule.coe_to_submodule_mk p _, },
  { rintros ⟨N, rfl⟩, exact N.coe_submodule_is_lie_submodule L, },
end

/- Alternative version of `is_lie_submodule_iff_exists` that obviates the need for any other
lemmas or defs. Is this preferable, e.g., because we get a simpler API? -/
lemma submodule.is_lie_submodule_iff_exists' :
  (∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p) ↔ ∃ (N : lie_submodule R L M), ↑N = p :=
begin
  split,
  { intros h, use { lie_mem := h, ..p }, exact lie_submodule.coe_to_submodule_mk p _, },
  { rintros ⟨N, rfl⟩, exact N.lie_mem, },
end

[Eric Wieser]

It looks like you probably want submodule.to_lie_submodule (S : submodule R M) (h : sorry) := { map_lie := h, ..S} to promote submodules into lie submodules

[Eric Wieser]

Without actually answering your question directly

[Oliver Nash]

Agreed; in fact I have done this in my actual local work.

[Oliver Nash]

Though I haven't followed the details, I believe that we have had some refactoring associated with issues like whether to prefer bundled subgroups subgroup or the (deprecated?) is_subgroup. I am hoping that anyone involved in that may have experience to share.

[Oliver Nash]

Note however that I am only proposing a def and not a class for is_lie_submodule. I think it definitely would be a mistake to make submodule.is_lie_submodule a class and start down the path of having lemmas that prove results for submodules which happen to carry an instance of submodule.is_lie_submodule etc.

[Eric Wieser]

I think this ties in closely with design questions about linear_map and friends too, but for now it probably makes sense to just continue the existing design.

[Oliver Nash]

I'm all in favour of adhering to existing design but for now I can't see which way that guides me on this point.

[Eric Wieser]

is_lie_submodule seems questionable to me, given it's not phrased in terms of a hypothetical is_submodule

[Oliver Nash]

Oh I see; yeah maybe that's enough to persuade me.

[Eric Wieser]

On the other hand, that's not an argument against also adding is_submodule

[Oliver Nash]

Indeed!

[Oliver Nash]

OK thanks. I'm going to forge ahead and not introduce is_lie_submodule but I'm all ears if anyone else shows up in this thread, especially anyone involved in the is_subgroup vs. group war.

[Eric Wieser]

But then you also need is_submonoid, is_sub_mul_action

[Oliver Nash]

It did occur to me that is_lie_submodule is bascially lie_submodule.lie_mem so we could probably use some magical metaprogramming to auto-generate all this stuff if we wanted it.

[Eric Wieser]

Something I could see being useful is metaprogramming to generate lie_submodule extends submodule from a definition of is_lie_submodule extends is_submodule

[Oliver Nash]

Sure. Presumably we could go either way though? As in: humans define everything in the bundled fashion (lie_submodule, submodule, submonoid, ...) and computers generate the is_ world for us, together with all the links OR vice-versa: humans work in the is_ world and computers generate all the bundled stuff + links.

[Eric Wieser]

The bundled version has a lot of boilerplate about coercions

[Oliver Nash]

Theoretically a lot of that could be auto-generated too though, right? I mean maybe all that boilerplate is a smell that we humans should be making definitions in the clean is_ world and computers should be populating the bundled world based on that (including all the boilerplate)? Anyway, I'm waffling and I need to help unpack the shopping now.

[Kevin Buzzard]

Let me try and recall what happened with groups. There were two things which got deprecated: the class is_group_hom, a predicate on functions between groups, and the class is_subgroup, a predicate on subsets of a group. My memory is that the problem with is_group_hom was that type class inference would spot that f circ g was a group hom but it wouldn't spot that lam x, f (g x) was. There were similar problems with persuading type class inference to play well with is_subgroup. So the classes were abandoned. I don't think there's any use for is_group_hom any more? However my understanding is that is_subgroup turns out to be useful predicate, and the reason it sits in deprecated is simply that it should be turned into a def. @Mario Carneiro how close am I to the truth here? What is the plan with the deprecated stuff?

[Mario Carneiro]

I think the use of is_subgroup should be minimized but not necessarily eliminated, and is_group_hom too. The main place these come up is when you have a set appear independently of a subgroup structure and want to say it is a subgroup; you can do this with \ex s : subgroup, s = X but this still amounts to having an is_subgroup definition kicking around.

The issue with type class inference is that using set, resp. function syntax for sets causes problems if you have any bound variables, because typeclass inference does not handle higher order goals. Also \circ makes everything worse because it's reducible so if this appears in your goal then you already have bound variables in the goal. As long as you don't use bound variables and only ever build things "structurally", typeclass inference works, and bundled subgroups/homs have the necessary discipline to ensure that you only ever build structured things.

[Oliver Nash]

Thank you both for these helpful remarks. The comments about typeclass inference not handling higher order goals and so having problems with bound variables, though not directly related to my issue, are interesting.

[Oliver Nash]

Mario Carneiro said:

The main place these come up is when you have a set appear independently of a subgroup structure and want to say it is a subgroup; you can do this with \ex s : subgroup, s = X but this still amounts to having an is_subgroup definition kicking around.

This is basically exactly my situation. I want to state the Lie algebra equivalent of subgroup.normal_in_normalizer (which I've only just thought to look up!).

[Oliver Nash]

Looking at this now though I see that subgroup.normal_in_normalizer defines an instance of the Prop-valued subgroup.normal which looks like an error to me since subgroup.normal is a structure and not a class.

[Oliver Nash]

I'll be taking this up properly tomorrow. I'll attempt not to introduce is_lie_submodule but I'll take Mario's "minimized but not necessarily eliminated" remark as permission to propose it if I think it makes sense.

[Johan Commelin]

Oliver Nash said:

Looking at this now though I see that subgroup.normal_in_normalizer defines an instance of the Prop-valued subgroup.normal which looks like an error to me since subgroup.normal is a structure and not a class.

normal is a class, afaik. But it is debatable whether it should be.

[Oliver Nash]

Oh you're quite right, I missed this on the very next line below the definition of subgroup.normal:

attribute [class] normal

[Kevin Buzzard]

Yeah, don't you love the way they do that -- it's to catch people out :-) The correct way to check is not to look at the definition in mathlib but to do #print normal and look at the attributes at the top. They do it with topological spaces too.

[Oliver Nash]

Ah sure I'm used to being caught out and I'll remember this in future!

[Kevin Buzzard]

Actually I think it's not to catch people out -- I asked Johannes a very long time ago why topological_space was defined as a structure and then given the class attribute, but I did not understand his reply (I would probably have more of a chance now -- I think it was to do with structure projections or fields or the right kind of brackets or wanting to prove that topological spaces are a lattice...)

[Mario Carneiro]

I think these aren't ok anymore in lean 4

[Oliver Nash]

Given that it's more work to apply the attribute later, Chesterton's fence would suggest they had a good resaon.

[Mario Carneiro]

The effect of applying them later is that the fields of the structure get () binders instead of []