Zulip Chat Archive

Stream: general

Topic: subobjects


view this post on Zulip Kevin Buzzard (Jul 20 2019 at 14:38):

This is the Lean proof that the open subsets of a topological space form a complete lattice.

instance : complete_lattice (opens α) :=
complete_lattice.copy
(@order_dual.lattice.complete_lattice _
  (@galois_insertion.lift_complete_lattice
    (order_dual (set α)) (order_dual (opens α)) _ interior (subtype.val : opens α  set α) _ gi))
/- le  -/ (λ U V, U.1  V.1) rfl
/- top -/ set.univ, _root_.is_open_univ (subtype.ext.mpr interior_univ.symm)
/- bot -/ , is_open_empty rfl
/- sup -/ (λ U V, U.1  V.1, _root_.is_open_union U.2 V.2) rfl
/- inf -/ (λ U V, U.1  V.1, _root_.is_open_inter U.2 V.2)
begin
  funext,
  apply subtype.ext.mpr,
  symmetry,
  apply interior_eq_of_open,
  exact (_root_.is_open_inter U.2 V.2),
end
/- Sup -/ (λ Us, ⋃₀ (subtype.val '' Us), _root_.is_open_sUnion $ λ U hU,
by { rcases hU with ⟨⟨V, hV, h, h', dsimp at h', subst h', exact hV})
begin
  funext,
  apply subtype.ext.mpr,
  simp [Sup_range],
  refl,
end

I was expecting the proof to look more like the following: "we all know that set alpha is a complete lattice, and open subsets are just a sublattice of this, so things like finite intersections and infinite unions will remain the same once it has been fed into the system that finite intersections and infinite unions of opens are open, which is the axioms for a topology, so we're done". It will be some sort of sub-infi-bot-hemi-sup-subcomplete-lattice or whatever. Are these kinds of sublattices already in mathlib? Then you get of the form a sub-infi-hemi-sublattice of a complete lattice is complete. Is this a thing? Can this be an instance? What is going on with this code? It looks on the face of it as bad as some of the code I write, and the authors of the file are Johannes and Mario. @Mario Carneiro why did things turn out like that with all the _copy nonsense?

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 14:43):

Hey -- are sublattices in Lean bundled or unbundled?

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 14:45):

@Johannes Hölzl I am learning to love lattices! What do you think about bundled sublattices?

view this post on Zulip Chris Hughes (Jul 20 2019 at 15:00):

I'm AFK. What do the two begin... end blocks prove?

view this post on Zulip Chris Hughes (Jul 20 2019 at 15:00):

I guess the hard part is infinite sup and inf.

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 15:08):

structure subthing (K : Type) [thing K] :=
(carrier : set K)
(proof : is_subthing carrier)

Is carrier idiomatic Lean?

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 15:08):

The first begin end block proves this:

1 goal
α : Type u_1,
_inst_1 : topological_space α
⊢ (λ (U V : opens α), ⟨U.val ∩ V.val, _⟩) = complete_lattice.inf

and the second proves this:

1 goal
α : Type u_1,
_inst_1 : topological_space α
⊢ (λ (Us : set (opens α)), ⟨⋃₀(subtype.val '' Us), _⟩) = complete_lattice.Sup

view this post on Zulip Chris Hughes (Jul 20 2019 at 15:11):

My guess is it's because the definition given by the galois insertion would be interior (a \cap b) , but that's not the definition we want in this case.

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 15:21):

That's an interesting observation.

Is there no notation for has_Sup or has_Inf like we have and for sup and inf? And this supr notation -- is that notation which doesn't have a typeclass associated to it? Is that something which could change in Lean 4?

view this post on Zulip Chris Hughes (Jul 20 2019 at 15:30):

It doesn't have a typeclass because of universe issues.

view this post on Zulip Chris Hughes (Jul 20 2019 at 15:31):

The indexing type could be in any universe.

view this post on Zulip Chris Hughes (Jul 20 2019 at 15:32):

It leads to a somewhat unnatural definition for cInf on Prop and set

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 16:05):

Is this a bug in open?

import data.set.lattice

open lattice

structure lattice.sublattice (α : Type) [lattice α] :=
(carrier : set α)
(sup_preserved :  a b  carrier, a  b  carrier)
(inf_preserved :  a b  carrier, a  b  carrier)

-- note that lattice is open.
-- uncomment the next line to fix line 17:
-- open lattice

instance (α : Type) [lattice α] : has_coe_to_sort (sublattice α) := ⟨_, sublattice.carrier

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 16:38):

class thing (α : Type) : Type. -- insert data here

variables {α : Type} [thing α]

class is_subthing (s : set α) : Prop := true -- insert proofs here

structure subthing (α : Type) [thing α] :=
(carrier : set α)
(proof : is_subthing carrier)

instance : has_coe_to_sort (subthing α) := ⟨_, subthing.carrier

instance : has_coe (subthing α) (set α) := subthing.carrier

instance : has_coe_to_fun (subthing α) :=
{ F := λ _, α  Prop,
  coe := λ β, β.carrier}

Which coercion should I be using?

view this post on Zulip Chris Hughes (Jul 20 2019 at 16:49):

Probably the first two.

view this post on Zulip Johan Commelin (Jul 20 2019 at 17:27):

I'm AFK.

@Chris Hughes AFK? Did you mean AFL?

view this post on Zulip Chris Hughes (Jul 20 2019 at 20:10):

What's AFL?

view this post on Zulip Wojciech Nawrocki (Jul 20 2019 at 20:11):

Maybe Chris is trying out a pure type theory without axiom K.

view this post on Zulip Chris Hughes (Jul 20 2019 at 20:12):

I mean away from laptop. But my phone screen doesn't count as a keyboard.

view this post on Zulip Jesse Michael Han (Jul 20 2019 at 20:18):

AFL = away from lean

i wonder if anyone's tried running lean on their phone

view this post on Zulip Chris Hughes (Jul 20 2019 at 20:20):

I tried because there is an emacs app. I gave up without much effort. I think @Kevin Buzzard does it.

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 20:44):

Yes I've had Lean running on rooted Android phone

view this post on Zulip Mario Carneiro (Jul 20 2019 at 21:03):

browser-lean?

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 23:05):

It was a chrooted debian with emacs


Last updated: May 16 2021 at 21:11 UTC