# Zulip Chat Archive

## Stream: general

### Topic: Closure operators

#### Yaël Dillies (Apr 24 2021 at 18:36):

@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 (Apr 24 2021 at 18:40):

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

#### Yaël Dillies (Apr 24 2021 at 19:29):

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 (Apr 24 2021 at 20:23):

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

#### Yaël Dillies (Apr 24 2021 at 20:58):

Yeah, we do! It's `galois_insertion.closure_operator`

. We might want to rename it to `galois_insertion.to_closure_operator`

.

#### Eric Wieser (Apr 24 2021 at 21:00):

docs#galois_insertion.closure_operator?

#### Yaël Dillies (Apr 24 2021 at 21:01):

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

#### Yaël Dillies (Apr 24 2021 at 21:02):

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 (Apr 24 2021 at 21:03):

In contrast, it works great for `convex_hull`

because `convex`

is unbundled.

#### Yaël Dillies (Apr 29 2021 at 13:33):

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 (Apr 29 2021 at 13:34):

How is this different from a galois insertion?

#### Yaël Dillies (Apr 29 2021 at 13:37):

Oh, is it how Galois insertions work already?

#### Bhavik Mehta (Apr 29 2021 at 13:38):

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

#### Anne Baanen (Apr 29 2021 at 13:41):

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

#### Yaël Dillies (Apr 29 2021 at 13:43):

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 (Apr 29 2021 at 13:44):

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 (Apr 29 2021 at 13:53):

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

?

#### Anne Baanen (Apr 29 2021 at 13:56):

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 (Apr 29 2021 at 13:59):

(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 (Apr 29 2021 at 14:02):

I don't think that's going to work well, because we define `closure`

in terms of the complete lattice structure

#### Eric Wieser (Apr 29 2021 at 14:03):

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 (Apr 29 2021 at 14:05):

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 (Apr 29 2021 at 14:15):

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 (Apr 29 2021 at 14:31):

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 (Apr 29 2021 at 14:32):

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 (Apr 29 2021 at 14:38):

The radical of an ideal is another example :)

#### Yaël Dillies (Apr 29 2021 at 14:39):

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 (Apr 29 2021 at 14:40):

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

#### Yaël Dillies (Apr 29 2021 at 14:41):

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

#### Bhavik Mehta (Apr 29 2021 at 14:43):

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

#### Yaël Dillies (Apr 29 2021 at 14:45):

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

#### Bhavik Mehta (Apr 29 2021 at 14:59):

Yup!

#### Kevin Buzzard (Apr 29 2021 at 16:09):

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

#### Yaël Dillies (Apr 29 2021 at 19:46):

Just spotted `zorn.chain_closure`

and `field_theory.perfect_closure`

in the wild.

#### Adam Topaz (Apr 29 2021 at 20:10):

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 (Apr 29 2021 at 20:15):

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 (Apr 29 2021 at 20:16):

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

#### Adam Topaz (Apr 29 2021 at 20:17):

That's right. you need the exchange axiom

#### Adam Topaz (Apr 29 2021 at 20:18):

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 (Apr 30 2021 at 04:45):

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 (Apr 30 2021 at 07:26):

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 (Apr 30 2021 at 07:29):

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

#### Kevin Buzzard (Apr 30 2021 at 07:39):

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 (May 04 2021 at 11:41):

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 (May 04 2021 at 11:58):

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 (May 04 2021 at 12:03):

We have things like `is_subgroup`

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

#### Scott Morrison (May 04 2021 at 12:07):

@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 (May 04 2021 at 16:49):

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 (May 04 2021 at 21:33):

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 (May 05 2021 at 09:23):

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 (May 05 2021 at 09:38):

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 (May 05 2021 at 09:39):

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 (May 05 2021 at 09:39):

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 (May 05 2021 at 09:40):

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 (May 05 2021 at 09:41):

It is indeed, according to the docstring :)

#### Eric Wieser (May 05 2021 at 10:11):

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 (May 05 2021 at 10:13):

(this would obsolete set_like)

#### Anne Baanen (May 05 2021 at 10:23):

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 (May 05 2021 at 10:24):

(An appropriate version of `set_like`

would basically automate the latter.)

#### Scott Morrison (May 05 2021 at 11:36):

... 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 (May 05 2021 at 20:45):

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 (May 06 2021 at 08:50):

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 (May 06 2021 at 19:32):

This isn’t a redefinition of `closure_operator`

, it’s a specific function that could be made into a `closure_operator`

#### Yaël Dillies (May 10 2021 at 16:48):

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 (May 10 2021 at 16:52):

Galois connections are used in lots of places in mathlib.

#### Yaël Dillies (May 10 2021 at 16:55):

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

#### Anne Baanen (May 10 2021 at 20:25):

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 (May 10 2021 at 20:25):

Let me write out a bit of code...

#### Anne Baanen (May 10 2021 at 20:39):

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 (May 10 2021 at 20:40):

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

#### Eric Wieser (May 10 2021 at 21:07):

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 (May 10 2021 at 21:41):

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

#### Anne Baanen (May 10 2021 at 21:45):

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 (May 10 2021 at 21:50):

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 (May 12 2021 at 07:19):

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 (May 12 2021 at 07:19):

Note that a closure operator only requires a `galois_connection`

.

#### Anne Baanen (May 12 2021 at 08:36):

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 (May 12 2021 at 08:37):

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 (May 12 2021 at 08:40):

Do you think there's any chance we'll need `upper_adjoint`

? If I'm correct this is an interior operator.

#### Yaël Dillies (May 12 2021 at 08:42):

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 (May 12 2021 at 08:45):

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 (May 12 2021 at 08:48):

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 (May 12 2021 at 08:49):

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 (May 12 2021 at 08:50):

That is, I would rather write `ideal.span s`

(or `submodule.span R s`

) than `(@semiring.to_module R).span s`

#### Yaël Dillies (May 12 2021 at 08:51):

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

#### Yaël Dillies (May 12 2021 at 08:53):

So what's there to be done?

#### Yaël Dillies (May 12 2021 at 08:54):

I think we can just go through `order/closure.lean`

and see what needs changing.

#### Yaël Dillies (May 12 2021 at 08:55):

Ah yeah, I wanted to try out the case `α = β`

as I suspect the `id`

will turn out weird.

#### Yaël Dillies (May 12 2021 at 08:59):

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 (May 12 2021 at 09:00):

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 (May 12 2021 at 09:02):

Is that `id`

a problem?

#### Yaël Dillies (May 12 2021 at 09:03):

I don't know, you tell me. But I wouldn't want `id`

s to clutter all expressions involving convex hulls and stuff.

#### Yaël Dillies (May 12 2021 at 09:09):

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 (May 12 2021 at 10:29):

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 (May 12 2021 at 10:32):

`x.gi'`

is about `x.to_fun`

, `x.gi`

is about `⇑x`

#### Eric Wieser (May 12 2021 at 10:32):

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

#### Yaël Dillies (May 12 2021 at 10:35):

Aaah, I see :)

#### Bhavik Mehta (May 12 2021 at 11:04):

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 (May 12 2021 at 11:06):

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

, right?

#### Bhavik Mehta (May 12 2021 at 11:07):

Yup

#### Yaël Dillies (May 12 2021 at 11:15):

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 (May 12 2021 at 11:17):

`lower_adjoint id`

seems to rather correspond to an interior operator, but `lower_adjoint`

does give closure operators. I'm confused.

#### Yaël Dillies (May 12 2021 at 11:23):

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

#### Yaël Dillies (May 12 2021 at 12:03):

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

#### Yaël Dillies (May 12 2021 at 14:10):

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 (May 12 2021 at 18:09):

So Bhavik and I have been thinking about creating a constructor from a `complete_lattice`

structure 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 (May 12 2021 at 18:25):

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 (May 12 2021 at 18:37):

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 (May 12 2021 at 19:49):

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

#### Yaël Dillies (May 12 2021 at 21:37):

Would it make sense to define `upper_adjoint`

in a similar fashion?

#### Yaël Dillies (May 12 2021 at 21:38):

Also, `order.semiconj_Sup`

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

#### Yaël Dillies (May 15 2021 at 21:35):

Last updated: Aug 03 2023 at 10:10 UTC