Abstracting the substructure lattice construction

Stream: mathlib4

[Artie Khovanov]

There's a lot of API duplicated (inconsistently) in this area of the algebra library. I've tried factoring the proof closure is a Galois insertion into a typeclass: #20621
Any thoughts?

[Johan Commelin]

I think this is an interesting idea to pursue. It should (in a follow-up PR, I guess) also be used to deduplicate Submodule.span and LieModule.lieSpan.

[Johan Commelin]

But let's make sure that we get the definition right, and not run into troubles with definitional equalities.

[Johan Commelin]

You currently have

class SetLikeCompleteLattice (L α : Type*) extends CompleteLattice L, SetLike L α where
  le_def' : le =
    @LE.le L (@Preorder.toLE L (@PartialOrder.toPreorder L SetLike.instPartialOrder))
  lt_def' : lt =
    @LT.lt L (@Preorder.toLT L (@PartialOrder.toPreorder L SetLike.instPartialOrder))
  coe_sInf' (s : Set L) : sInf s = InfSet.sInf (SetLike.coe '' s)

and this is needed because docs#SetLike.instPartialOrder is creating data.

But I think we are asking for trouble if we push along like this.
Instead, SetLike should extend PreOrder, I think.

[Thomas Browning]

I've wondered about this as well. Would one option be to extend SetLike to have an additional Prop-valued axiom stating that every Set-theoretic intersection is in the image of the coercion?

[Johan Commelin]

What do you mean exactly?

[Johan Commelin]

Ooh, I see. You want to say $\forall a b, \exists c, \text{coe}\, c = \text{coe}\, a \cap \text{coe}\, b$

[Johan Commelin]

And maybe also for infinite intersections

[Thomas Browning]

Yes, exactly. Something like this:

class SubobjectLike (A B : Type*) extends SetLike A B where
  foo : ∀ S : Set A, ∃ a₀ : A, coe a₀ = ⋂ a ∈ S, coe a

noncomputable def closure (A : Type*) {B : Type*} [h : SubobjectLike A B] (b : Set B) : A :=
  (h.foo {a : A | SetLike.coe a ≤ b}).choose

One annoying this is that A needs to be explicit, so you would still need separate declarations for all the various closures (unless you want to be writing things like closure (IntermediateField K L) S), but you could at least use this to streamline things.

[Johan Commelin]

A doesn't have to be explicit, right? It can be inferred from the expected type.
And when that is not available, we can use (A := _) syntax to supply it.

[Johan Commelin]

But still, I don't like the idea of creating more and more data out of the original SetLike class.

[Johan Commelin]

The mathlib pattern is to avoid creating data, and extending it instead.

[Thomas Browning]

What do you mean by creating data here?

[Johan Commelin]

And we can provide a constructor with minimal axioms, so that the data can still be created when needed.

[Johan Commelin]

In this case closure. Because now it will not be defeq to the current defn of Submodule.span R s etc...

[Johan Commelin]

docs#SetLike.instPartialOrder is a mathlib-antipattern.

[Thomas Browning]

Ah, so would it be better to have a predicate IsClosureOperatorwith instances for span, adjoin, etc..., with all the relevant API?

[Thomas Browning]

Or I suppose you could include closure in the data of SubobjectLike, but have a constructor just assuming the axiom foo. Is that closer to what you're thinking?

[Johan Commelin]

Exactly

[Johan Commelin]

Additionally, SetLike should extend PartialOrder, with a separate constructor that only assumes the current fields

[Thomas Browning]

Right. Also, what's the pros and cons of extends vs typeclass assumption:

class SubobjectLike₁ (A B : Type*) extends SetLike A B where
  closure : Set B → A
  closure_le_iff : ∀ {a : A} {b : Set B}, closure b ≤ a ↔ b ⊆ SetLike.coe a

vs

class SubobjectLike₂ (A B : Type*) [SetLike A B] where
  closure : Set B → A
  closure_le_iff : ∀ {a : A} {b : Set B}, closure b ≤ a ↔ b ⊆ SetLike.coe a

[Thomas Browning]

For SetLike and PartialOrder it should be extends, since there are cases where you want to get the PartialOrder from the minimal SetLike constructor. But does it matter here?

[Johan Commelin]

Not much difference, except in the amount of typing when setting up your variable lines

[Thomas Browning]

Oh, I guess SubobjectLikeshould also extend CompleteLattice since that has data.

[Edward van de Meent]

Johan Commelin said:

I think this is an interesting idea to pursue. It should (in a follow-up PR, I guess) also be used to deduplicate Submodule.span and LieModule.lieSpan.

as well as (Add)Submonoid.closure and (Add)Subgroup.closure?

[Yaël Dillies]

I've been meaning to kill SetLike.instPartialOrder and introduce a new class OrderedSetLike instead. It's really annoying that currently the semantics confuse "I have an injective coercion to sets" with "I have an injective coercion to sets that orders me". Eg this is wrong for upper sets (wrong way around) and partitions (completely nonsense).

[Johan Commelin]

I'm working on a refactor right now.

[Johan Commelin]

@Yaël Dillies What would you like to happen with upper sets?

[Johan Commelin]

Atm, I'm not giving them any instance. Otherwise we need some ContravariantlyOrderedSetLike. That is out of scope for my refactor.

[Eric Wieser]

Johan Commelin said:

But still, I don't like the idea of creating more and more data out of the original SetLike class.

I actually think that this is acceptable as long as we do this for all the data, but indeed as Yaël Dillies points out, the data constructed isn't right for some situations.

[Johan Commelin]

#20638 -- I've tried to make this PR minimally invasive, but it still touches a lot of files.

[Edward van de Meent]

i've just realised, since "ordered sets" exist in math, maybe OrderedSetLike is a bad name?

[Edward van de Meent]

because the ordering is not on the elements of the sets, like for posets (partially ordered sets), but on the collection of sets under consideration?

[Johan Commelin]

We have ConcreteCategory, so maybe ConcretePartialOrder?

[Edward van de Meent]

maybe we just don't want this as a class, and instead want a SetLike.toPartialOrder definition which occasionally gets used for an instance?

[Edward van de Meent]

(that seems like maybe a smaller PR)

[Johan Commelin]

Well, the followup goal was to unify all the span and closure operators... so we need a class for those. And that would be a superclass of this one.

[Artie Khovanov]

How do we maintain the defeq of the bottom element of our lattice of substructures?

[Artie Khovanov]

Everything apart from bot and sup is determined by the "nice" embedding into our powerset, so we can just define those fields explicitly within our default instance, and sup isn't ususally given an explicit definition in favour of an induction principle, but bot isn't determined, yet is usually given an explicit definition.

[Artie Khovanov]

eg
bot : Subsemigroup S = emptyset
bot : Subgroup G = {1}
bot : Subring R = {0,1,2,...}
bot : Subalgebra R A = range (embedding R -> A)

[Artie Khovanov]

We might have to maintain that coe_sInf' axiom rather than doing it via an instance heirarchy

[Artie Khovanov]

Right now we have

@[to_additive "The `AddSubsemigroup`s of an `AddMonoid` form a complete lattice."]
instance : CompleteLattice (Subsemigroup M) :=
  { completeLatticeOfInf (Subsemigroup M) fun _ =>
      IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
    le := (· ≤ ·)
    lt := (· < ·)
    bot := ⊥
    bot_le := fun _ _ hx => (not_mem_bot hx).elim
    top := ⊤
    le_top := fun _ x _ => mem_top x
    inf := (· ⊓ ·)
    sInf := InfSet.sInf
    le_inf := fun _ _ _ ha hb _ hx => ⟨ha hx, hb hx⟩
    inf_le_left := fun _ _ _ => And.left
    inf_le_right := fun _ _ _ => And.right }

and yeah, given a proof of ∀ S : Set A, ∃ a₀ : A, coe a₀ = ⋂ a ∈ S, coe a, all those data fields can be generated in a way that's defeq to rn.. except bot

[Thomas Browning]

You can always have a constructor that takes in any data you want to preserve (e.g., bot and closure) and autogenerates the rest.

[Artie Khovanov]

Oh you're so right
Wait that's literally how this complete lattice instance is working!

[Artie Khovanov]

Johan Commelin said:

#20638 -- I've tried to make this PR minimally invasive, but it still touches a lot of files.

/-- A class to indicate that there is a canonical order preserving injection
between `A` and `Set B`. -/
class OrderedSetLike (A : Type*) (B : outParam Type*) extends PartialOrder A where
  /-- The coercion from a term of a `SetLike` to its corresponding `Set`. -/
  protected coe : A → Set B
  /-- The coercion from a `SetLike` type preserves the ordering. -/
  protected coe_subset_coe' {S T : A} : coe S ⊆ coe T ↔ S ≤ T

Doesn't this class also kill the defeq of "≤" as "coe · ⊆ coe ·", just like my proposal? I spelled mine in that way with the technical instances just so I wouldn't have to think about the proofs I was copying. I could spell it your way, but it wouldn't get around this issue of the definitional equality being erased in the abstract.

[Edward van de Meent]

that's up to instances to decide; see for example here in Johan's PR

[Artie Khovanov]

Oh yeah for sure, every concrete instance will have the right definitional equalities
But they won't be accessible just from the class assumption i.e. when we are proving stuff about the Galois insertion

[Artie Khovanov]

Maybe this isn't an issue but I thought that was undesirable?
Then the \bot thing isn't an issue either

[Edward van de Meent]

if it's used when proving stuff, since it is propeq, it shouldn't be an issue, no?

[Artie Khovanov]

well, the proofs have to be changed
from the current ones
but yes it's not a huge deal

[Artie Khovanov]

Johan Commelin said:

#20638 -- I've tried to make this PR minimally invasive, but it still touches a lot of files.

Why doesn't OrderedSetLike extend SetLike?

[Artie Khovanov]

(deleted)

[Artie Khovanov]

OK, my new definition is

class LatticeSetLike (L : Type*) (α : outParam Type*)
    extends CompleteLattice L, OrderedSetLike L α where
  coe_sInf' (s : Set L) : coe (sInf s) = InfSet.sInf (coe '' s)

[Artie Khovanov]

But when I try to use it in practice it doesn't work nicely, and I'm not sure how to fix it:

@[to_additive]
instance : LatticeSetLike (Subsemigroup M) M where
  __ := (inferInstance : CompleteLattice (Subsemigroup M))
  __ := (inferInstance : OrderedSetLike (Subsemigroup M) M)
  coe_sInf' := by
    rw [show OrderedSetLike.coe = SetLike.coe by rfl]
    simp

(this is on top of the changes in #20638)

[Artie Khovanov]

How can I make it so the instance is just the following?

@[to_additive]
instance : LatticeSetLike (Subsemigroup M) M where
  coe_sInf' := by simp

[Artie Khovanov]

never mind, fixed it all!
attempt 2: #20621 (building on @Johan Commelin's PR)

[Artie Khovanov]

Thomas Browning said:

Or I suppose you could include closure in the data of SubobjectLike, but have a constructor just assuming the axiom foo. Is that closer to what you're thinking?

I've implemented this (except I didn't include closure as data, instead I included all the lattice data)

[Artie Khovanov]

(Renamed the thread to clarify the scope -- most of the duplicated lemmas are about closures but the construction of the CompleteLattice instance is also duplicated.)

[Johan Commelin]

Linking to the parallel thread #mathlib4 > proposal: lattice operations on `SetLike`s? with a very similar proposal by David Loeffler

[Johan Commelin]

I think one downside of LatticeSetLike is that it will require duplicating the order hierarchy.
For that reason, it might be better to have a mixin, on top of SetLike and LE.

[Johan Commelin]

Here is a rough sketch/proposal

• LE X -- ordering
• SetLike X Y -- coercion (injective)
• IsConcrete X Y -- coercion is order preserving, mixin depending on LE X and SetLike X
• CompleteLattice X etc -- order hierarchy, extending LE X
• HasSpan Y X -- a notation typeclass for a function span : Set Y -> X
• IsConcreteWithSpan X Y -- the span is a closure operator, and gives a Galois connection together with the coe, extending IsConcrete X Y and HasSpan X Y. (Probably needs a better name.)

[Johan Commelin]

In particular, the OrderedSetLike from my PR would be replaced by the IsConcrete mixin.

[Anne Baanen]

I agree that mixins would be a nice way to save us from having to duplicate the order hierarchy (at the expense of some amount of discoverability).

[Anne Baanen]

How would we deal with CompleteLattice + IsConcrete together implying IsConcreteWithSpan? (Since we could also define the span of a set s in a setlike S as the infimum of {x : S | s \subset coe x}.)

[Johan Commelin]

That would be a separate constructor, right?

[Anne Baanen]

I suppose we would need a separate constructor anyway, since not every definition of spans would go through taking infima.

[Edward van de Meent]

/poll if/when we merge the "closure" functions, what should it be called:
closure (even though docs#closure already exists)
span
adjoint

[Edward van de Meent]

docs#closure

[Edward van de Meent]

i'd really like for this to be called closure if it's possible to avoid a clash with the preexisting topological closure. And adjoint is very undescript, imo.

[Johan Commelin]

Can we have

-- U+29FC ⧼ LEFT-POINTING CURVED ANGLE BRACKET and U+29FD ⧽

as notation?

[Johan Commelin]

I know docs#ClosureOperator is a thing, but all over algebra these constructions are called span. Hence my vote.
It is also shorter.

[Eric Wieser]

Is notation going to help? How do we plan to distinguish Submodule.span SomeLongRing {v} and Algebra.adjoin SomeLongRing {x}?

[Eric Wieser]

(⧼v⧽ : Submodule SomeLongRing _) I guess? But we'd end up with the annotation pretty much all the time.

[Johan Commelin]

I'm hoping the expected type will solve this very often.

[Johan Commelin]

And otherwise we can have ⧼v⧽_[Submodule SomeLongRing _]

[Edward van de Meent]

Johan Commelin said:

Can we have

-- U+29FC ⧼ LEFT-POINTING CURVED ANGLE BRACKET and U+29FD ⧽

as notation?

which of these do you mean?

variable (R : Type*) [Ring R] (s : Set R) (P : R -> Prop)
-- version A
#check (⧼s⧽ : Subring R) -- Subring R
-- version B
#check (⧼x : R | P x⧽ : Subring R) -- Subring R

[Eric Wieser]

This raises the fact that we could perhaps just use a coercion?

[Eric Wieser]

⧼x : R | P x⧽ seems too magic to me, but ⧼{x : R | P x}⧽ is a bit noisy

[Edward van de Meent]

perhaps we can have a default instance depending on opened scope?

[Johan Commelin]

I meant both notations! And @Eric Wieser I don't agree it is too magic. It's notation that is very common on the literature.

[Eric Wieser]

Would it support the entire family of set literal notations?

[Edward van de Meent]

we likely can't have both ⧼s⧽ (referring to the closure of a set) and ⧼x⧽ (referring to the closure of a single element)

[Johan Commelin]

@Eric Wieser Yes. Although there might be some edge cases that I fail to think of right now.

[Artie Khovanov]

Johan Commelin said:

I'm hoping the expected type will solve this very often.

Very often you want to prove things relating closures to each other, though. In particular, because explicit use of sums is discouraged, you often want to prove theorems of the form

(SubObject1.closure s : Set G) = (SubObject2.closure (f s) : Set G).

[Edward van de Meent]

we will have the type ascription issue anyway, since HasSpan.span s will also complain.

[Artie Khovanov]

@Johan Commelin re your proposal:
Part of what I am trying to abstract out is the construction of a lattice instance on Subobject. Specifically, the result is that, if the coercion reflects arbitrary infima, then Subobject gets a CompleteLattice instance and a closure operator for free.

I'm trying to think how this fits into your proposal. Just as we define a constructor for IsConcrete from SetLike, we can define constructors for CompleteLattice, HasSpan and IsConcreteWithSpan from IsConcrete under the additional assumption that SetLike.coe reflects (arbitrary) infima. Is this the intended pattern?

[Artie Khovanov]

Johan Commelin said:

I think one downside of LatticeSetLike is that it will require duplicating the order hierarchy.
For that reason, it might be better to have a mixin, on top of SetLike and LE.

Sorry, I'm not sure what this means. What is going to be duplicated? If you have closure s defined as sInf {l : L | s ≤ l}, then you have arbitrary infima, and so a complete lattice.

[Artie Khovanov]

Edward van de Meent said:

we will have the type ascription issue anyway, since HasSpan.span s will also complain.

True. In my proposal, I have the lattice type L as an explicit argument to closure. Then I introduce abbreviations

abbrev Subsemigroup.closure = LatticeSetLike.closure (Subsemigroup S)

[Edward van de Meent]

Artie Khovanov said:

Johan Commelin said:

I think one downside of LatticeSetLike is that it will require duplicating the order hierarchy.
For that reason, it might be better to have a mixin, on top of SetLike and LE.

Sorry, I'm not sure what this means. What is going to be duplicated? If you have closure s defined as sInf {l : L | s ≤ l}, then you have arbitrary infima, and so a complete lattice.

it means that not only will the approach use LatticeSetLike, but also SemiLatticeSupSetLike, SemiLatticeInfSetLike, and similar for a whole bunch of superclasses of Lattice

[Artie Khovanov]

I'm not sure I understand. Those subclasses appear unnecessary to me because eg a SemiLatticeSup and SemiLatticeInf are CompleteLattices, with the rest of the operations determined uniquely. If you have a well-behaved sInf operation in a poset, you have a complete lattice.

[Johan Commelin]

Edward van de Meent said:

we will have the type ascription issue anyway, since HasSpan.span s will also complain.

span (as := Subgroup G) s :smiley:

[Artie Khovanov]

you would have to write that every time -- it can't infer the type in practice!

[Eric Wieser]

(span s : Subgroup G) is shorter

[Eric Wieser]

Note that we actually already have notation for this in mathlib, for docs#IntermediateField.adjoin (F⟮α⟯)

[Artie Khovanov]

I think that, if we are explicitly annotating the type every time, then the information allowing us to determine the type should just be an explicit argument

[Johan Commelin]

@Artie Khovanov I agree that everything will be a complete lattice, but what if I want to have a complete Boolean algebra, say? Or some other wacky combo.

[Johan Commelin]

Johan Commelin said:

And otherwise we can have ⧼v⧽_[Submodule SomeLongRing _]

We can have notation that includes the type.

[Artie Khovanov]

Ah right, I see. I didn't think about extending upwards. I guess this way allows us to unify other closure operations as well, such as topological closure?

[Eric Wieser]

I'm not really a fan of notation that just reinvents type ascription

[Eric Wieser]

⧼v⧽_[Submodule SomeLongRing _] is only one character shorter than (⧼v⧽ : Submodule SomeLongRing _)

[Artie Khovanov]

I think it's important to force users to specify the type, otherwise it's a massive footgun for people unfamiliar with this part of the library (as well as being confusing from a mathematical perspective).
You can always add namespaced abbrevs

[Edward van de Meent]

Eric Wieser said:

⧼v⧽_[Submodule SomeLongRing _] is only one character shorter than (⧼v⧽ : Submodule SomeLongRing _)

removing the underscore inbetween, 2 characters :upside_down:

[Eric Wieser]

I don't think forcing it is really a notation question, users can still not specify it by writing ⧼v⧽_[_]

[Artie Khovanov]

Johan Commelin said:

• IsConcrete X Y -- coercion is order preserving, mixin depending on LE X and SetLike X

We could call this IsConcreteLE?
Sorry this is getting a bit bikeshed, I'll go ahead and write this proposal up tonight probably so we have something concrete to look at.

[Artie Khovanov]

@Johan Commelin not sure how to prove IsConcrete for the default SetLike order nicely. Right now I have:

/-- A class to indicate that the canonical injection between `A` and `Set B` is order-preserving. -/
class IsConcreteLE (A B : Type*) [SetLike A B] [LE A] where
  /-- The coercion from a `SetLike` type preserves the ordering. -/
  protected coe_subset_coe' {S T : A} : SetLike.coe S ⊆ SetLike.coe T ↔ S ≤ T

variable {A : Type*} {B : Type*} [i : SetLike A B]

def toLE : LE A where
  le := fun H K => ∀ ⦃x⦄, x ∈ H → x ∈ K

def toPartialOrder : PartialOrder A where
  __ := toLE
  __ := PartialOrder.lift (SetLike.coe : A → Set B) coe_injective

instance : @IsConcreteLE A B _ toLE :=
  let _ := toLE (i := i)
  exact ⟨Iff.rfl⟩

[Anne Baanen]

Is the problem that you have to specify toLE explicitly here? You can use attribute [local instance] to add it to the available instances in the current scope, for example:

import Mathlib.Data.SetLike.Basic

/-- A class to indicate that the canonical injection between `A` and `Set B` is order-preserving. -/
class IsConcreteLE (A B : Type*) [SetLike A B] [LE A] where
  /-- The coercion from a `SetLike` type preserves the ordering. -/
  protected coe_subset_coe' {S T : A} : SetLike.coe S ⊆ SetLike.coe T ↔ S ≤ T

namespace SetLike

variable {A : Type*} {B : Type*} [i : SetLike A B]

/--

This is an `abbrev` so that it can reduce when it is a local instance.
See note [reducible non-instances].
-/
abbrev toLE : LE A where
  le := fun H K => ∀ ⦃x⦄, x ∈ H → x ∈ K

abbrev toPartialOrder : PartialOrder A where
  __ := toLE
  __ := PartialOrder.lift (SetLike.coe : A → Set B) coe_injective

attribute [local instance] toLE toPartialOrder

instance : IsConcreteLE A B :=
  ⟨Iff.rfl⟩

end SetLike

[Anne Baanen]

(It's also a good idea to make defs that will act like instances into abbrevs, because declaring instances makes them more reducible than default.)

[Artie Khovanov]

@Anne Baanen by the way, my editor cannot ever find the note [reducible non-instances]. How do I get it to appear?
Also, what is the difference between abbrev and @[reducible] def?

[Anne Baanen]

The note lives in Mathlib/Algebra/HierarchyDesign.lean. Maybe it's not found because it's not imported?

[Anne Baanen]

abbrev does slightly more than @[reducible], I think it at least adds @[inline] as well. But I don't recall the details. Mostly I use it because it's somewhat nicer to read than @[reducible] def.

[Artie Khovanov]

OK, the design has now been implemented (for one example) in #20836, feel free to check it out and give feedback

[Artie Khovanov]

didn't implement the notation because I don't know how to do that

[Artie Khovanov]

hm
terminological question: I would naively interpret HasClosure as referring to a closure operator cl:A -> A
of course, such operators are precisely the ones arising from a Galois insertion (eg from (cl '' A) to A), but maybe we should have a different name for what is just the property of SetLike.coe having an adjoint
I still think the adjoint map should be called "closure", of course

[Bhavik Mehta]

cc @Yaël Dillies, I think you and I came to basically this exact conclusion a few years ago!

[Yaël Dillies]

Yes, I have been silently following this discussion and I didn't really want to intervene, because what I have to say is that I think the solutions that were offered here are overengineered and will each fail to capture some subtleties of various subobjects and their associated closure operator. Eg

• Does the closure operator return Set α or Subobject α?
• How is the closure operator usually called?
• How to name lemmas describing the interaction of several closure operators?

[Johan Commelin]

• We are trying to to abstract all the different span : Set \a -> Subobject \a. So that should be the type of the abstraction.
• I don't care too much. We had a vote upstairs.
• Depends on :up: but I'm sure we can solve this, just like with lemmas describing the interaction of several Adds or Muls.

[Artie Khovanov]

I don't see why we can't use the existing naming conventions for interaction of different closure operators
like subgroup_closure etc