## Stream: general

### Topic: subobjects

#### 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?

#### Kevin Buzzard (Jul 20 2019 at 14:43):

Hey -- are sublattices in Lean bundled or unbundled?

#### Kevin Buzzard (Jul 20 2019 at 14:45):

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

#### Chris Hughes (Jul 20 2019 at 15:00):

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

#### Chris Hughes (Jul 20 2019 at 15:00):

I guess the hard part is infinite sup and inf.

#### 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?

#### 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


#### 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.

#### 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?

#### Chris Hughes (Jul 20 2019 at 15:30):

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

#### Chris Hughes (Jul 20 2019 at 15:31):

The indexing type could be in any universe.

#### Chris Hughes (Jul 20 2019 at 15:32):

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

#### 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⟩


#### 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?

#### Chris Hughes (Jul 20 2019 at 16:49):

Probably the first two.

#### Johan Commelin (Jul 20 2019 at 17:27):

I'm AFK.

@Chris Hughes AFK? Did you mean AFL?

What's AFL?

#### Wojciech Nawrocki (Jul 20 2019 at 20:11):

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

#### Chris Hughes (Jul 20 2019 at 20:12):

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

#### Jesse Michael Han (Jul 20 2019 at 20:18):

AFL = away from lean

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

#### 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.

#### Kevin Buzzard (Jul 20 2019 at 20:44):

Yes I've had Lean running on rooted Android phone

browser-lean?

#### Kevin Buzzard (Jul 20 2019 at 23:05):

It was a chrooted debian with emacs

Last updated: May 16 2021 at 21:11 UTC