Closure operators

Stream: general

[Yaël Dillies]

@Bhavik Mehta baked us an API for closure operators (in order/closure.lean). It provides a bundled version of a closure operator. Should we refactor closure, convex_hull and other, or should we instead prove an unbundled version as an instance for each of them?

[Eric Wieser]

Would this work for a bundled version of say docs#submonoid.closure? What would that look like if so?

[Yaël Dillies]

Actually, you already have a Galois insertion on submonoids, which is better than a closure operator. So I don't think it's applicable there, apart from exempting from proving some lemmas by hand.

[Eric Wieser]

Do we have a way to downgrade a galois insertion to a closure operator then?

[Yaël Dillies]

Yeah, we do! It's galois_insertion.closure_operator. We might want to rename it to galois_insertion.to_closure_operator.

[Eric Wieser]

docs#galois_insertion.closure_operator?

[Yaël Dillies]

Ah oops, it's rather docs#galois_connection.closure_operator

[Yaël Dillies]

Actually, it's not much that the Galois insertion (or connection?) is more powerful than the closure operator but rather that submonoid is bundled. I can easily define the closure operator to output the carrier of submonoid.closure, but not with the information that it's a submonoid built in.

[Yaël Dillies]

In contrast, it works great for convex_hull because convex is unbundled.

[Yaël Dillies]

Actually, I'm thinking there's something to be done there. The pattern "closure operator that's actually not quite one because it outputs the closure bundled with more info" is ultra common: subgroups, submonoids, subspaces... and I'm sure you can think of more than I do. What we could do would be to define bundled_closure_operator as a closure operator bundled with the information that its output is a submonoid/subgroup/subspace...
What's your opinion?

[Bhavik Mehta]

How is this different from a galois insertion?

[Yaël Dillies]

Oh, is it how Galois insertions work already?

[Bhavik Mehta]

It seems to me that you're describing exactly a galois insertion, which is already there for submonoids, subgroups etc

[Anne Baanen]

In particular, you turn docs#subgroup.gi into a closure operator by forgetting the bundled info after applying docs#subgroup.closure.

[Yaël Dillies]

Bhavik Mehta said:

It seems to me that you're describing exactly a galois insertion, which is already there for submonoids, subgroups etc

No, that's not how it works. Take for example submonoid.closure. It's defined as \la s, Inf {S : submonoid M | s ⊆ ↑S}. What I'm offering is to define it as

bundled_closure_operator
(to_fun := \la s, Inf {S : submonoid M | s ⊆ ↑S})
(to_coe := \la s, Inf {t | s ⊆ t \and \ex S : submonoid M, t = ↑S})
(<more infos to make to_coe a closure operator>)

or something of sort

[Yaël Dillies]

My point is that we could change the way the info is bundled so that we can actually use the theorems associated with closure operators.

[Eric Wieser]

Are you asking for a shorter name for subgroup.gc.closure_operator?

[Anne Baanen]

Is this the kind of thing you're looking for?

import group_theory.subgroup

/-- The `has_closure A B` typeclass represents types with
a canonical injection `coe : A → set B`, which has a left adjoint `closure : set B → A`.
-/
class has_closure (A : Type*) (B : out_param $ Type*) extends set_like A B :=
(closure : set B → A)
(gi : galois_insertion closure coe)

namespace has_closure

variables {A B : Type*}

instance [has_closure A B] : complete_lattice A :=
has_closure.gi.lift_complete_lattice

end has_closure

instance subgroup.has_closure (G : Type*) [group G] :
  has_closure (subgroup G) G :=
{ closure := subgroup.closure,
  gi := subgroup.gi G,
  .. subgroup.set_like }

[Anne Baanen]

(This doesn't work great because you can't infer which closure you're taking from the arguments, so you need to keep writing x ∈ (closure s : subgroup G).)

[Eric Wieser]

I don't think that's going to work well, because we define closure in terms of the complete lattice structure

[Eric Wieser]

I have a refactor in progress that replaces subgroup with subtype is_subgroup, that might make it easier to generalize this type of thing

[Anne Baanen]

Yeah, as it is set up currently it wouldn't work in some places where closure is defined in terms of Inf. However, instances like docs#intermediate_field.complete_lattice already use this technique and would definitely see advantages in terms of deduplication.

[Anne Baanen]

For example, here are the first few closure lemmas in subgroup.lean, which are really just galois_insertion _ coe lemmas:

lemma subset_closure : s ⊆ (closure s : A) :=
has_closure.gi.gc.le_u (le_refl _)

lemma closure_le : closure s ≤ S ↔ s ⊆ S :=
has_closure.gi.gc _ _

lemma mem_closure {x : B} : x ∈ (closure s : A) ↔ ∀ S : A, s ⊆ S → x ∈ S :=
by { simp_rw [← set_like.mem_coe, ← set.singleton_subset_iff, ← closure_le],
     exact ⟨λ h S, le_trans h, λ h, h _ (le_refl _)⟩ }

lemma closure_eq_of_le (h₁ : s ⊆ S) (h₂ : S ≤ closure s) : closure s = S :=
le_antisymm (closure_le.2 h₁) h₂

[Yaël Dillies]

Yes, you very much got my point. Sorry for being unclear. I'm mostly worried about the duplication I'm seeing all over the place (have a look at convex_hull, for example).

[Yaël Dillies]

I'm now planning on bundling closure operators whose output is unbundled. I already spotted convex hull, topological closure, transitive closure, reflexive closure.
What do you think?

[Bhavik Mehta]

The radical of an ideal is another example :)

[Yaël Dillies]

Ooh, right! The radical of a natural too, but I'm not sure that already exists/there's a nice way to formulate it without using ideals.

[Bhavik Mehta]

I think radical of a natural should be an interior operator rather than a closure operator?

[Yaël Dillies]

rad n is literally the natural number corresponding to the radical of nZ.

[Bhavik Mehta]

Sure, but the radical of a natural can be smaller (in divisibility or the usual ordering) than the natural itself

[Yaël Dillies]

Ah right. Am I correct thinking that an interior operator is literally a closure operator with respect to the dual order?

[Bhavik Mehta]

Yup!

[Kevin Buzzard]

The inequality on ideals is dual to the divisibility operator on naturals :-)

[Yaël Dillies]

Just spotted zorn.chain_closure and field_theory.perfect_closure in the wild.

[Adam Topaz]

I think another closure operator that we should add ASAP is the relative algebraic closure of a set in a field extension. The general stuff about closure operators would then let us define transcendence degree, transcendence bases, etc.

[Yaël Dillies]

Do you already have a definition and only need a refactor, or do you need to set up the theory as well?

[David Wärn]

I thought there's content to the assertion that transcendence degree is well-defined? It's some matroid property?

[Adam Topaz]

That's right. you need the exchange axiom

[Adam Topaz]

Yaël Dillies said:

Do you already have a definition and only need a refactor, or do you need to set up the theory as well?

No, as far as I'm aware the definition of relative algebraic closure is not in mathlib

[Johan Commelin]

What is the "relative algebraic closure"? Is this just the "algebraic closure of $K$ in $L$"? Because that's the same as the integral closure, which mathlib knows about.

[Yaël Dillies]

How do we want to deal with interior operators? Do we want to make a specific API, or just define the ones we have as closure operators on the dual order?

[Yaël Dillies]

in particular, is there any general interaction between interior and closure operators?

[Kevin Buzzard]

The problem with this question is that there are people who feel that the principled approach is to do everything twice, and there are people who feel that duplicating code can't be the right idea, so you might not get a coherent answer about how to make an interior API. The only way I've seen interior and closure interact is via frontier, which is closure minus interior and has its own little API.

[Yaël Dillies]

Oh, I found a funny one. span_points and affine_span are the unbundled and bundled variant of the same closure operator. Here it seems that my approach is well worth some thought.
My idea is that, given a partial order on α and a structure S α on α (think of (≤) and subgroup), we could define a "bundled closure operator" on α as an object that could be coerced to a function α → S α, knowing that the output of this function could itself be coerced to α. That way, we could get the best off both worlds.

[Yaël Dillies]

What I don't know is whether it's possible to feed in such a structure (subgroup, submonoid, affine_subspace...) to a constructor. Is it?

[Kevin Buzzard]

We have things like is_subgroup (a predicate on subsets) which can sometimes be useful in situations like this.

[Scott Morrison]

@Yaël Dillies, you might look at the design of concrete_category, and for example how we set up Mon, Group, Module, and so on, to see one approach to be polymorphic in typeclasses.

[Yaël Dillies]

Eric Wieser said:

Would this work for a bundled version of say docs#submonoid.closure? What would that look like if so?

Turns out it works! The trick is to simply change closure_operator extends α →ₘ α to closure_operator extends α →ₘ β and ask for the instance [has_coe_t β α] (if anyone knows how to ask this coercion to be monotone, please tell me!).

import order.closure
import group_theory.submonoid.basic

open set submonoid

variables {M : Type*} [mul_one_class M]

def submonoid.neo_closure : closure_operator (set M) (submonoid M) :=
{ to_fun := λ s, Inf {S : submonoid M | s ⊆ ↑S},
  le_closure' := λ s x hx, mem_Inf.2 $ λ S hS, hS hx,
  idempotent' := sorry,
  monotone' := sorry }

I left idempotent' and monotone' sorried because the easy way to prove them is to use my new constructors, which I haven't yet bothered to translate in this new two types closure operators paradigm.

[Yaël Dillies]

Anne Baanen said:

(This doesn't work great because you can't infer which closure you're taking from the arguments, so you need to keep writing x ∈ (closure s : subgroup G).)

In my conception of things, we would rather define group.closure and then write x ∈ G.closure s. The example I posted just above should clear up my intentions.

[Anne Baanen]

Ah good idea! I didn't like the idea of defining subgroup.closure and submonoid.closure and submodule.span and ... because you would have to copy over all (simp) lemmas, but instantiating it as a bundled type fixes that.

[Anne Baanen]

Is this the place you need your has_coe_t to be either id or the map sending subobjects to the carrier set? I think you're looking for the docs#set_like typeclass in that case.

[Oliver Nash]

I haven't been following this thread properly but if we're going to define some fancy new submodule.span then we might want to do the same for docs#lie_submodule.lie_span

[Anne Baanen]

Sorry, just realized this is being discussed further here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/monotone.20coercion

[Anne Baanen]

Oliver Nash said:

I haven't been following this thread properly but if we're going to define some fancy new submodule.span then we might want to do the same for docs#lie_submodule.lie_span

Definitely! If the lie_span of s is the smallest lie_submodule whose carrier set contains s, then it should be defined as a closure operator.

[Anne Baanen]

It is indeed, according to the docstring :)

[Eric Wieser]

A refactor I've been considering is redefining submodule as subtype is_submodule, which means we can have a general closure operator which just means closure (s : set A) (p : set A \to Prop) : subtype p := Inf { x : subtype p | s \sub \u x}

[Eric Wieser]

(this would obsolete set_like)

[Anne Baanen]

Interesting idea, I don't know if it would completely obsolete set_like though: wouldn't you have to choose between writing subtype (is_subobject X) everywhere, or writing subobject X and copying over all subtype lemmas?

[Anne Baanen]

(An appropriate version of set_like would basically automate the latter.)

[Scott Morrison]

... or define submodule M as subobject (Module.of R M)... :-) I really haven't thought whether it is at all plausible. There is a complete lattice structure on subobject X with reasonable assumption, however, and various functoriality / pullback / pushforward operations.

[Yaël Dillies]

Eric Wieser said:

A refactor I've been considering is redefining submodule as subtype is_submodule, which means we can have a general closure operator which just means closure (s : set A) (p : set A \to Prop) [complete_lattice (subtype p)] : subtype p := Inf {x : subtype p | s ⊆ ↑x}

How does that interact with my refactor proposition? Would you do that instead of mine, or layer both?

[Yaël Dillies]

Ah actually wouldn't there be the problem that closure operators don't need complete lattices to work? Partial order is enough, but I don't know whether any of the closure operators we deal with in practice are partial orders but not complete lattices.

[Aaron Anderson]

This isn’t a redefinition of closure_operator, it’s a specific function that could be made into a closure_operator

[Yaël Dillies]

Okay so we have Galois connections and closure operators. Which way do we want go? Should we build Galois connections from closure operators, or closure operators from Galois connections?

If we start from Galois connections, then we're kind of burying the actual closure and maybe it will be harder to work with in practice (is there any way to systematically simplify it?). Further, I don't think we ever use Galois connections in expression. They rather tend to be passed as instances. The current way things are set up is that we first define the closure operator, and then prove the galois_connection/galois_insertion instance.

If we start from closure operators, I don't think we have the problem that closure operators do not uniquely determine Galois connections because we're bundling them with the functions. But we might want to change the definition we currently have to get rid of the galois_connection field:

structure fully_bundled (α β : Type*) [preorder α] [preorder β] :=
(l : α → β)
(u : β → α)
(gc : galois_connection l u)

structure partially_bundled {α β : Type*} [preorder α] [preorder β] (u : β → α) :=
(l : α → β)
(gc : galois_connection l u)

Actually, given that closure_operator and galois_connection take in the same infos and that galois_connection isn't really used apart from instances, wouldn't there be a way to unify them under a single structure that would both have a coe_to_fun and be useful as an instance on its own?

[Patrick Massot]

Galois connections are used in lots of places in mathlib.

[Yaël Dillies]

But are they used in a way that's incompatible with giving them dot notation?

[Anne Baanen]

My concrete proposal (from the other thread) would be to use partially_bundled galois insertions (connections), because I foresee a major use case will be for subobjects, where the u is instantiated to be coe : subfoo α → set α.

[Anne Baanen]

Let me write out a bit of code...

[Anne Baanen]

This is how I would rewrite lines 540-563 of group_theory/subgroup.lean:

import group_theory.subgroup

structure lower_adjoint {α β : Type*} [preorder α] [preorder β] (u : β → α) :=
(to_fun : α → β)
(gi' : galois_insertion to_fun u)

namespace lower_adjoint

variables {α β : Type*} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u)

instance : has_coe_to_fun (lower_adjoint u) :=
{ F := λ _, α → β, coe := to_fun }

initialize_simps_projections lower_adjoint (to_fun → apply)

def gi : galois_insertion l u := l.gi'

end lower_adjoint

@[simps?] def subgroup.closure' (G : Type*) [group G] :
  lower_adjoint (coe : subgroup G → set G) :=
{ to_fun := subgroup.closure,
  gi' := subgroup.gi G }

-- Lemmas for `lower_adjoint (coe : α → set β)`, where `set_like α β`
section coe_to_set

namespace lower_adjoint

variables {α β : Type*} [set_like α β]
variables (closure : lower_adjoint (coe : α → set β))
variables {s : set β} {S : α}

lemma subset : s ⊆ (closure s : α) :=
closure.gi.gc.le_u (le_refl _)

lemma le_iff : closure s ≤ S ↔ s ⊆ S :=
closure.gi.gc _ _

lemma mem_iff {x : β} : x ∈ (closure s : α) ↔ ∀ S : α, s ⊆ S → x ∈ S :=
by { simp_rw [← set_like.mem_coe, ← set.singleton_subset_iff, ← closure.le_iff],
     exact ⟨λ h S, le_trans h, λ h, h _ (le_refl _)⟩ }

lemma closure_eq_of_le (h₁ : s ⊆ S) (h₂ : S ≤ closure s) : closure s = S :=
le_antisymm (closure.le_iff.2 h₁) h₂

end lower_adjoint

end coe_to_set

[Anne Baanen]

(Definitely not going to stick to these names, but the overall structure seems viable to me.)

[Eric Wieser]

Are those the only four lemma that can be generalized in this way, or are there more and you just picked them as examples?

[Anne Baanen]

There are definitely more, these were just the first ones I did before I got bored.

[Anne Baanen]

E.g. from submodule.span we'd also get (untested, just copied and renamed)

lemma mono (h : s ⊆ t) : closure s ≤ closure t :=
closure.le_iff.2 $ subset.trans h closure.subset

@[simp] lemma apply_self : closure (S : set β) = S :=
closure.eq_of_le closure.subset (le_refl _)

[Anne Baanen]

And then there's the other complete lattice operators:

@[simp] lemma map_empty : closure (∅ : set β) = ⊥ :=
closure.gi.gc.l_bot

@[simp] lemma map_univ : closure (univ : set M) = ⊤ :=
eq_top_iff.2 $ set_like.le_def.2 $ closure.subset

lemma map_union (s t : set β) : closure (s ∪ t) = closure s ⊔ closure t :=
closure.gi.gc.l_sup

lemma map_Union {ι} (s : ι → set β) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
closure.gc.l_supr

lemma eq_supr_closure_singleton : closure s = ⨆ x ∈ s, closure {x} :=
by simp only [←map_Union, set.bUnion_of_singleton s]

etc.

[Yaël Dillies]

So lower_adjoint would act like the closure operator? And you want to feed in a galois_insertion inside it, then take it out?
Let's see if I can do something with that.

[Yaël Dillies]

Note that a closure operator only requires a galois_connection.

[Anne Baanen]

Ah sorry, yes. It should probably be galois_connection, I just took the previous code where the closure map was defined in a typeclass and adjusted it, overlooking that difference.

[Yaël Dillies]

I tried making dot notation work but it turns out weird because group is unbundled.

@[simps] def group.closure {G : Type*} (hG : group G) :
  lower_adjoint (coe : subgroup G → set G) :=
{ to_fun := λ k, Inf {K | k ⊆ K},
  gc' := λ k K,
    ⟨set.subset.trans $ λ x hx, subgroup.mem_Inf.2 $ λ K hK, hK hx, λ h, Inf_le h⟩ }

lemma subset_closure (G : Type*) [h : group G] (s : set G) :
  s ⊆ h.closure s :=
h.closure.gc.le_u (le_refl _)

[Yaël Dillies]

Do you think there's any chance we'll need upper_adjoint? If I'm correct this is an interior operator.

[Yaël Dillies]

I kind of find it weird to name a closure operator lower_adjoint but I guess it's more accurate as the actual closure operator is the composition of both adjoints.

[Anne Baanen]

The name lower_adjoin is definitely something of a placeholder, which I used because I'm more at home with (basic) category theory than order theory.

[Eric Wieser]

Note that we already have docs#monoid.closure but it has quite a different type; so I think group.closure is a bad name.

[Anne Baanen]

I would follow the existing mathlib convention and call it subgroup.closure. Dot notation seems unlikely to work well, especially since there are things like the smallest ideal of R containing s that would become module.span with your convention, and there's no easy way to name the module R R instance.

[Anne Baanen]

That is, I would rather write ideal.span s (or submodule.span R s) than (@semiring.to_module R).span s

[Yaël Dillies]

Yeah, I think so too. But I think there are also cases where dot notation turns out fine.

[Yaël Dillies]

So what's there to be done?

[Yaël Dillies]

I think we can just go through order/closure.lean and see what needs changing.

[Yaël Dillies]

Ah yeah, I wanted to try out the case α = β as I suspect the id will turn out weird.

[Yaël Dillies]

Ugh, yeah it does: (λ (s : set E), ⋂ (t : set E) (hst : s ⊆ t) (ht : convex t), t) s ≤ t ↔ s ≤ id t

[Yaël Dillies]

Then maybe we can restrict closure_operator to same-set closure operators and lower_adjoint (or however we end up calling it) to the other cases?

[Eric Wieser]

Is that id a problem?

[Yaël Dillies]

I don't know, you tell me. But I wouldn't want ids to clutter all expressions involving convex hulls and stuff.

[Yaël Dillies]

Yaël Dillies said:

Then maybe we can restrict closure_operator to same-set closure operators and lower_adjoint (or however we end up calling it) to the other cases?

@Bhavik Mehta is that how you saw things (with galois_insertion instead of lower_adjoint) when introducing order/closure.lean?

[Yaël Dillies]

Anne Baanen said:

This is how I would rewrite lines 540-563 of group_theory/subgroup.lean:

import group_theory.subgroup

structure lower_adjoint {α β : Type*} [preorder α] [preorder β] (u : β → α) :=
(to_fun : α → β)
(gi' : galois_insertion to_fun u)

namespace lower_adjoint

variables {α β : Type*} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u)

instance : has_coe_to_fun (lower_adjoint u) :=
{ F := λ _, α → β, coe := to_fun }

initialize_simps_projections lower_adjoint (to_fun → apply)

def gi : galois_insertion l u := l.gi'

end lower_adjoint

@[simps?] def subgroup.closure' (G : Type*) [group G] :
  lower_adjoint (coe : subgroup G → set G) :=
{ to_fun := subgroup.closure,
  gi' := subgroup.gi G }

-- Lemmas for `lower_adjoint (coe : α → set β)`, where `set_like α β`
section coe_to_set

namespace lower_adjoint

variables {α β : Type*} [set_like α β]
variables (closure : lower_adjoint (coe : α → set β))
variables {s : set β} {S : α}

lemma subset : s ⊆ (closure s : α) :=
closure.gi.gc.le_u (le_refl _)

lemma le_iff : closure s ≤ S ↔ s ⊆ S :=
closure.gi.gc _ _

lemma mem_iff {x : β} : x ∈ (closure s : α) ↔ ∀ S : α, s ⊆ S → x ∈ S :=
by { simp_rw [← set_like.mem_coe, ← set.singleton_subset_iff, ← closure.le_iff],
     exact ⟨λ h S, le_trans h, λ h, h _ (le_refl _)⟩ }

lemma eq_of_le (h₁ : s ⊆ S) (h₂ : S ≤ closure s) : closure s = S :=
le_antisymm (closure.le_iff.2 h₁) h₂

end lower_adjoint

end coe_to_set

What's the point of introducing gi' first versus just putting gi as a field?

[Eric Wieser]

x.gi' is about x.to_fun, x.gi is about ⇑x

[Eric Wieser]

It's like docs#add_monoid_hom.map_add vs docs#add_monoid_hom.map_add'

[Yaël Dillies]

Aaah, I see :)

[Bhavik Mehta]

The original reason I wanted closure operators wasn't to make algebraic structures easier, but to be able to talk about results for general closure operators. So as long as there's a type for closure operators on a type, I'm happy

[Yaël Dillies]

And when you talk about general closure operators, you mean α → α, right?

[Bhavik Mehta]

Yup

[Yaël Dillies]

Uh, I'm confused. This is wrong

def closure_operator.lower_adjoint (c : closure_operator α) : lower_adjoint (id : α → α) :=
{ to_fun := c.to_fun,
  gc' := _ }

[Yaël Dillies]

lower_adjoint id seems to rather correspond to an interior operator, but lower_adjoint does give closure operators. I'm confused.

[Yaël Dillies]

Maybe for that we need an antitone Galois connection? That's weird.

[Yaël Dillies]

I think I just tangled myself up and it actually works.

[Yaël Dillies]

So here's how it looks

G: Type u_1
h: group G
s: set G
⊢ s ⊆ ↑(⇑subgroup.closure' s)

Is it too coercion-frightening?

[Yaël Dillies]

So Bhavik and I have been thinking about creating a constructor from a complete_latticestructure on `` and here's how it goes

/-- Constructor from a `complete_lattice`. It is a commonplace construction with
`u := (coe : β → α)` -/
@[simps] def complete_lattice.closure (hu : monotone u) (hu₂ : ∀ s : set β, u (Inf ...) = lub (u ...) :
  lower_adjoint u :=
{ to_fun := λ k, Inf {K | k ≤ u K},
  gc' := λ k K,
  ⟨begin
    intro h,
    sorry
  end, λ h, Inf_le h⟩
}

[Yaël Dillies]

It seems that it's hard to get back galois_connection from complete_lattice. And I say "get back" because most of the complete_lattice instances we're concerned about use at one point or another the galois_connection in disguise.

[Yaël Dillies]

So I think the way to do would be basic stuff -> lower_adjoint (sorry, Anne Baanen this is slowly settling as the name :stuck_out_tongue:) -> lemmas about the closure -> complete_lattice -> more stuff

[Yaël Dillies]

Here's where stuff happens: https://github.com/leanprover-community/mathlib/tree/yael/lower_adjoint

[Yaël Dillies]

Would it make sense to define upper_adjoint in a similar fashion?

[Yaël Dillies]

Also, order.semiconj_Sup now ought to disappear, as what's in there just got heavily generalised.

[Yaël Dillies]

#7608

[Aaron Anderson]

I'd like to prove some things about the lattice of closed sets of a ClosureOperator/LowerAdjoint.

[Aaron Anderson]

Unfortunately, closed is defined differently for both of them - at least, in theory - the definition for LowerAdjoint satisfies l.closureOperator.closed = l.closed definitionally.

[Aaron Anderson]

To avoid duplicating all this API, should I perhaps just prove this API for ClosureOperator, and then tweak the LowerAdjoint API to define closed entirely in terms of the corresponding ClosureOperator?

[Yaël Dillies]

Wait wait, I have a refactor that solves this.

[Aaron Anderson]

Oh, fantastic!

[Aaron Anderson]

I'm behind the times on lots of things - is there a thread or branch I can see progress on?

[Aaron Anderson]

(I hadn't really started work on this, so I'm glad I posted!)

[Yaël Dillies]

No, the refactor is in my head. I'm writing up a PR as we speak.

[Aaron Anderson]

Then I'll just look forward to it.

[Yaël Dillies]

#9153

[Yaël Dillies]

This is the result of a veeeery long reflexion. Hope you like it :smile:

[Aaron Anderson]

That does look like an improvement!

[Aaron Anderson]

You do make a note on the PR though that you are “still not sure we want LowerAdjoint to even exist” - do we actually have a better solution for substructures generated by some set?

[Yaël Dillies]

What kind of substructures do you have in mind?

[Aaron Anderson]

docs#FirstOrder.Language.Substructure.closure is implemented as a LowerAdjoint, and I see no reason why docs#Subgroup.closure and such aren't

[Aaron Anderson]

I see, perhaps all the necessary weight is carried by the unbundled Galois insertion, such as docs#Subgroup.gi

[Aaron Anderson]

In that case, I might want my API at the level of Galois connections or insertions.

[Yaël Dillies]

Yes exactly. I figured out that the situation closure operators are useful in is exactly when we don't care about the preorder of closed elements (or at least not as a first class citizen). This happens with convex sets, upper, lower sets, sup-closed, inf-closed sets, normal fields... but not subgroups. That's why the former are ClosureOperators (or could be) while the latter carry a Galois connection instead.

[Yaël Dillies]

According to that logic, LowerAdjoint has no use case, since it is across two types and we already have GaloisConnection.