Zulip Chat Archive

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}