Two carriers for submodule

Stream: new members

[Martin C. Martin]

submodule extends add_submonoid, from which it inherits a field called carrier (via add_subsemigroup), and also sub_mul_action, from which it inherits another field, also called carrier. How do we ensure that these two carriers are the same?

Or is there only one? Here we refer to submodule.carrier, which suggests that maybe there's only a single inherited field? If so, how does that work?

[Yaël Dillies]

There is indeed only one. The answer so as to why it works the way you intend it to depends whether you use flat or nested structures. submodule is a flat structure so I'm going to explain this one.

[Eric Wieser]

Section 2 of arxiv#2306.00617 has some examples demonstrating how multiple inheritance works, both with flat inheritance (mathlib3) and nested inheritance (mathlib4, but presented in lean 3 in that paper)

[Yaël Dillies]

submodule extending add_submonoid and sub_mul_action means that Lean takes their fields and makes them fields of submodule, merging fields with the same name, eg carrier. Then it creates the obvious functions submodule.to_add_submonoid : submodule R M → add_submonoid M and submodule.to_sub_mul_action : submodule R M → sub_mul_action R M where the field add_submonoid.x/sub_mul_action.x gets filled in with submodule.x.

[Kyle Miller]

"Flat structures" is switched on with set_option old_structure_cmd true (the structure ends up having the union of all the fields of everything it extends, rather than using any of the parent structures themselves as fields). Yaël's explaining this, but I just wanted to point out that this option is important.

[Martin C. Martin]

I was afraid it might be named based. So this means, if person A maintains a structure somewhere and decides to change the name of a field, and unknown to them, the new name happens to be the same as person B chose for their unrelated structure, then person C, who extends both of them, now has only one field, not two. However, I suppose the name is part of the external interface of the structure. There's nothing like hidden fields in OO. There are no implementation details. :)

[Kyle Miller]

I didn't realize it's name-based in Lean 4 too. This is fine:

structure A where
  x : Nat

structure B where
  x : Nat

structure C extends A, B

If the types don't match it'll throw an error though.

[Kyle Miller]

If you want to protect against this, then just like in OO I think you'd embed rather than extend.

structure C where
  toA : A
  toB : B

[Martin C. Martin]

Where can I read more about inheritance in Lean 3?

[Eric Wieser]

Did you already read section 2 of arxiv#2306.00617 above? I'm not sure there's much else to know: inheritance is just syntactic sugar for either copying across all the fields, or inserting a parent field

[Martin C. Martin]

Ok thanks, I'll read that.

[Eric Wieser]

If your question is actually "where can I read more about mathematical uses of structure", https://leanprover-community.github.io/mathematics_in_lean/C07_Hierarchies.html#sub-objects is probably a good resource

[Eric Wieser]

(but that's for Lean 4)