preimage_of_image_univ missing in Mathlib?

Stream: mathlib4

[Kent Van Vels]

I was surprised that I needed to prove the following claim. It just says that the preimage of the image of a universal set is the same universal set. The "hard inclusion" is docs#Set.subset_preimage_image and the other inclusion is trivial, Anyways, I have it written here, if anyone thinks it should be included in mathlib.

import Mathlib.Tactic
open Function Set
variable {α β:Type*}

theorem preimage_image_univ {f : α → β} : f ⁻¹' (f '' univ) = univ :=
  subset_antisymm (fun _ _ ↦ True.intro) (subset_preimage_image f univ)

I can try to set up a pull request, but I haven't done that before. So for something this small, I would like to avoid doing it.

Thanks.

[Junyan Xu]

simp is your friend. simp? says

simp only [image_univ, preimage_range]

[Kent Van Vels]

Yeah, I know I am not doing amazing mathematics here. :) Thanks for the tip. I never remember to do simp?. Is the advantage of "simp only" that it runs faster?

[Junyan Xu]

It does run faster, but my purpose is just to show you the lemmas used. by simp would be a perfectly fine proof for this goal.

[Patrick Massot]

If you want to add a lemma then it would be nicer to put the more natural statement and deduce yours.

variable {α β : Type*}

lemma GaloisConnection.l_u_top [PartialOrder α] [OrderTop α] [Preorder β] [OrderTop β]
    {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤ :=
  gc.u_eq_top.mpr le_rfl

theorem preimage_image_univ {f : α → β} : f ⁻¹' (f '' univ) = univ :=
  Set.image_preimage.l_u_top

[Kent Van Vels]

I have only the slightest introduction to GaloisConnections. I think in the "Mathematics in Lean" book.

[Kent Van Vels]

So I will just mark this as resolved.

[Notification Bot]

Kent Van Vels has marked this topic as resolved.

[Kevin Buzzard]

Kent Van Vels said:

I have only the slightest introduction to GaloisConnections. I think in the "Mathematics in Lean" book.

Well f ⁻¹' and f '' are the perfect place to start learning about them! Here's one way of thinking about them. If f : α → β and we have subsets $X \subseteq\alpha$ and $Y\subseteq\beta$, when does $f$ induce a function from $X$ to $Y$? Well one way of asserting that this happens is that f '' X ⊆ Y. Another way of asserting this is that X ⊆ f ⁻¹' Y. In particular, these statements about X and Y, one involving f '' and the other involving f ⁻¹', are logically equivalent. This is exactly the Galois connection axiom for order-preserving maps (by which I mean ⊆-preserving here, i.e. X₁ ⊆ X₂ → f '' X₁ ⊆ f '' X₂ and similar for f ⁻¹'). Turns out that from this axiom alone you can deduce a bunch of other random stuff such as f ⁻¹' (f '' ⊤) = ⊤ where ⊤ is the biggest element of your source partial order. The Galois connection API just proves a bunch of these things, meaning that you don't have to independently prove them for e.g. images and preimages of sets under functions, pushforward and pullback of topologies, pushforward and pullback of filters, the Galois correspondence between intermediate fields and subgroups etc etc etc.

[Edward van de Meent]

Another example is the correspondence between (monoid/group/ring/algebra/module) "closures" and "forgetting" the structure, i.e. s <= H.carrier <-> s.closure <= H . (The mathlib name for the "closure" in question varies)

[Notification Bot]

Kent Van Vels has marked this topic as unresolved.

[Kent Van Vels]

I might dig into this over the weekend. @Kevin Buzzard, do you have a work sheet on Galois Connections?

[Kevin Buzzard]

I can't find one :-( I once lectured undergraduate algebraic geometry and realised that lectures 1 and 2, which started "let k be an algebraically closed field" and then proceeded to set up a Galois connection between subsets of k^n and ideals in k[X_1,X_2,..,X_n], was just a stupid special case of the whole Galois connection thing, and so I changed it to "let k be an arbitrary commutative ring" and then just set up the general theory of Galois connections and then applied it to get results about Zariski closed sets. But the Nullstellensatz has some actual content, and there you need that k is an alg closed field.

[Patrick Massot]

@Kent Van Vels there are some explanations at the beginning of https://vimeo.com/834887419. You can also look at the corresponding exercises in GlimpseOfLean

[Kent Van Vels]

@Patrick Massot , thanks for the links I will look into them. I really like reading/doing as many "Introduction to Lean" things.

I plan on adding to this to the library. I have an idea about Galois Connections now so I feel comfortable adding that lemma there. My name on github is kvanvels.

[Patrick Massot]

You should have a GitHub invitation!

[Kent Van Vels]

@Patrick Massot, I am finally getting around to this now that I have a little more time since Christmas is over. I have a few questions for you. I normally don't need this much "hand-holding" but since this is the first time I am contributing, I hope it is ok.

I added the "l_u_top" function in Mathlib/Order/GaloisConnection.lean So far, so good. I then added the function preimage_image_univ in Mathlib/Data/Set/Image.lean, but it complained that Set.image_preimage was unknown, so after some digging I added import Mathlib.Data.Set.Lattice to the imports. Using emacs, this resulted in it complaining that many (maybe all) of the theorems were previously defined. I looked at the problem in VS code, and it complained about detecting a build cycle". Here is an excerpt of what it said:

Running Mathlib.Data.Set.Image
error: build cycle detected:

  +Mathlib.Data.Set.Lattice:olean
  +Mathlib.Data.Bool.Set:olean
  +Mathlib.Order.CompleteLattice:olean
  +Mathlib.Order.CompleteBooleanAlgebra:olean
  +Mathlib.Data.Set.Lattice:olean

So it looks like I am inducing an "include cycle". How should I proceed? Can I solve this by doing a "clean build" or something similar? Perhaps there is a better place to define the Galois Connection of set preimage_image?

I have the changes committed to my local branch it is called kvanvels_branchand I just pushed it. Thanks!

[Eric Wieser]

This tells you that you have a loop of files that import each other cyclically; and therefore the import you added was a mistake.

[Eric Wieser]

Probably you put the new lemma in the wrong file; can you put it in Data/Set/Lattice instead?

[Kent Van Vels]

I have no objection to putting it there, I chose the file location because there is a very closely related theorem in there: subset_preimage_image.

[Ruben Van de Velde]

Right- so either you need to prove your lemma without relying on the lattice structure, or you need to move it somewhere where the lattice structure is available

[Kent Van Vels]

@Patrick Massot I have written a patch and have submitted a pull request.

Can you please double check that you are happy with the name in the GaloisConnection file? I followed your suggestion here. However, I would think it should be called u_l_top not l_u_top. @Eric Wieser Is unsure of the naming, too.

Should I be asking that kind of a question here, or in github?

Thanks

[Patrick Massot]

What is the statement of this u_l_top?

[Eric Wieser]

(@Kent Van Vels, if you write # followed by the PR number, it will link here)

[Kent Van Vels]

@Patrick Massot The PR is #20346. The statement is

lemma GaloisConnection.l_u_top [PartialOrder α] [OrderTop α] [Preorder β] [OrderTop β]
    {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤ := sorry

We are applying the composition

$$u \circ l.$$

[Patrick Massot]

Oh yes, this is definitely u_l_top. If I wrote it the other way around then it was a typo.