Inf of a pair of topologies

Stream: Is there code for X?

[Christopher Hoskin]

Hello,

I'm looking for a result something like:

universe u

open TopologicalSpace

lemma test1 {α : Type u} [t₁ : TopologicalSpace α] {T₁ : Set (Set α)} {cond₁ : TopologicalSpace.IsTopologicalBasis T₁}
    [t₂ : TopologicalSpace α] {T₂ : Set (Set α)} {cond₂ : TopologicalSpace.IsTopologicalBasis T₂} :
    @IsTopologicalBasis α (t₁ ⊓ t₂) {S | ∃ U₁ ∈ T₁, ∃ U₂ ∈ T₂, S = U₁ ∩ U₂} := sorry

I'm aware of:

theorem isTopologicalBasis_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    {T : ∀ i, Set (Set (X i))} (cond : ∀ i, IsTopologicalBasis (T i)) :
    IsTopologicalBasis { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
      (∀ i, i ∈ F → U i ∈ T i) ∧ S = (F : Set ι).pi U } := sorry

In Topology.Bases and though I should be able to deduce it from that.

I set off naively like this:

lemma test1 {α : Type u} [t₁ : TopologicalSpace α] {T₁ : Set (Set α)} {cond₁ : TopologicalSpace.IsTopologicalBasis T₁}
    [t₂ : TopologicalSpace α] {T₂ : Set (Set α)} {cond₂ : TopologicalSpace.IsTopologicalBasis T₂} :
    @IsTopologicalBasis α (t₁ ⊓ t₂) {S | ∃ U₁ ∈ T₁, ∃ U₂ ∈ T₂, S = U₁ ∩ U₂} := by
  let t : ((i : Fin 2) →  TopologicalSpace α)
  | 1 => t₁
  | 2 => t₂
  let T : (i : Fin 2) → Set (Set α)
  | 1 => T₁
  | 2 => T₂
  let conds : ((i : Fin 2) →  @IsTopologicalBasis _ (t i) (T i))
    | 1 => cond₁
    | 2 => cond₂
  let f : Fin 2 → α → α := fun _ => id
  letI := t₁ ⊓ t₂
  sorry

However after many hours of trying I haven't been able to put it all together correctly.

Is there an easier way of doing this? Is there some kind of "deduce the pairwise result from the pi result" magic that I've missed?

Thanks,

Christopher

[Eric Wieser]

Do we have docs#isTopologicalBasis_prod ?

[Eric Wieser]

docs#TopologicalSpace.IsTopologicalBasis.prod should save you the trouble with Fin 2

[Anatole Dedecker]

In any case it’s the wrong way around to deduce the inf statement from the prod statement, it should be the converse

[Anatole Dedecker]

Your best option would probably be to mimic the proof of the prod statement

[Junyan Xu]

(deleted)

[Christopher Hoskin]

Well, this is true:

-- surely this must exist somewhere???
lemma subset_and_subset {s t u : Set α} (h₁ : s ⊆ u) (h₂ : t ⊆ u) : s ∩ t ⊆ u := by
  convert (Set.inter_subset_inter h₁ h₂)
  exact (inter_self u).symm

protected theorem IsTopologicalBasis.inter {B₁ : Set (Set α)}
    {B₂ : Set (Set α)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) :
    IsTopologicalBasis (image2 (· ∩ ·) B₁ B₂) := by
  refine' isTopologicalBasis_of_isOpen_of_nhds _ _
  · rintro _ ⟨u₁, u₂, hu₁, hu₂, rfl⟩
    exact (h₁.isOpen hu₁).inter (h₂.isOpen hu₂)
  · rintro a u hu uo
    simp only [mem_image2, exists_and_left, exists_exists_and_exists_and_eq_and, mem_inter_iff]
    rcases (h₁.nhds_hasBasis).mem_iff.1 (IsOpen.mem_nhds uo hu) with
      ⟨s, ⟨hs, hbs⟩, hsu⟩
    rcases (h₂.nhds_hasBasis).mem_iff.1 (IsOpen.mem_nhds uo hu) with
      ⟨t, ⟨ht, hbt⟩, htu⟩
    use s
    constructor
    · exact hs
    · use t; exact ⟨ ht, ⟨⟨hbs, hbt⟩, subset_and_subset hsu htu⟩⟩

Although I can't believe that {s t u : Set α} (h₁ : s ⊆ u) (h₂ : t ⊆ u) : s ∩ t ⊆ u is unknown to Lean.

I then try:

lemma test1 {α : Type u} [t₁ : TopologicalSpace α] {T₁ : Set (Set α)} {cond₁ : TopologicalSpace.IsTopologicalBasis T₁}
    [t₂ : TopologicalSpace α] {T₂ : Set (Set α)} {cond₂ : TopologicalSpace.IsTopologicalBasis T₂} :
    @IsTopologicalBasis α (t₁ ⊓ t₂) (image2 (· ∩ ·) T₁ T₂) := by
  letI := t₁ ⊓ t₂
  apply IsTopologicalBasis.inter
  sorry
  sorry

Getting rid of the sorrys is defeating me.

[Patrick Massot]

Anatole didn't write that your statement is wrong, he wrote that the optimal proof strategy goes in the other direction.

[Jireh Loreaux]

(deleted)

[Junyan Xu]

One of h1 and h2 is unnecessary:

lemma subset_and_subset {s t u : Set α} (h₁ : s ⊆ u) : s ∩ t ⊆ u :=
  fun _ h ↦ h₁ h.1
  -- or (s.inter_subset_left t).trans h₁

[Junyan Xu]

I think it's pretty easy to specialize docs#isTopologicalBasis_iInf to isTopologicalBasis_inf and that kind of statement is arguably what we should have in mathlib (rather than putting three different topologies on the same space; usually you'd use type synonyms for that).
It's usually easier to use Bool for this purpose than Fin 2, since Bool.rec is convenient and has good defeq properties. Some examples are here.

[Richard Copley]

Christopher Hoskin said:

Although I can't believe that {s t u : Set α} (h₁ : s ⊆ u) (h₂ : t ⊆ u) : s ∩ t ⊆ u is unknown to Lean.

The aim is not to make a library containing every obvious fact in mathematics, as entertaining as that might be (cf. The Poetry Cloud by Cixin Liu). It's a success if what is there makes your lemma easy to prove in a couple of steps!

[Junyan Xu]

Scratch that, I now think using docs#TopologicalSpace.IsTopologicalBasis.prod and mimicking the proof that deduces isTopologicalBasis_iInf from isTopologicalBasis_pi would be the easiest. No need to deal with universe ULift issues ...

[Junyan Xu]

Here's a complete proof:

import Mathlib.Topology.Bases

open TopologicalSpace

variable {X Y Z} [tY : TopologicalSpace Y] [tZ : TopologicalSpace Z] (fY : X → Y) (fZ : X → Z)

theorem induced_to_prod (f : X → Y × Z) :
    induced f inferInstance = induced (fun x ↦ (f x).1) tY ⊓ induced (fun x ↦ (f x).2) tZ := by
  erw [induced_inf]
  simp_rw [induced_compose]
  rfl

theorem inducing_inf_to_prod :
    @Inducing X (Y × Z) (induced fY tY ⊓ induced fZ tZ) _ fun x ↦ (fY x, fZ x) :=
  letI := induced fY tY ⊓ induced fZ tZ; ⟨(induced_to_prod fun x ↦ (fY x, fZ x)).symm⟩

theorem TopologicalSpace.IsTopologicalBasis.inf
    {BY : Set (Set Y)} {BZ : Set (Set Z)} (bY : IsTopologicalBasis BY) (bZ : IsTopologicalBasis BZ) :
    @IsTopologicalBasis X (induced fY tY ⊓ induced fZ tZ) (BY.image2 (fY ⁻¹' · ∩ fZ ⁻¹' ·) BZ) := by
  letI := induced fY tY ⊓ induced fZ tZ
  convert (bY.prod bZ).inducing (inducing_inf_to_prod fY fZ)
  rw [Set.image_image2]; rfl

example {t₁ t₂ B₁ B₂} (h₁ : @IsTopologicalBasis X t₁ B₁) (h₂ : @IsTopologicalBasis X t₂ B₂) :
    @IsTopologicalBasis X (t₁ ⊓ t₂) (Set.image2 (· ∩ ·) B₁ B₂) := by
  convert @IsTopologicalBasis.inf X X X t₁ t₂ id id B₁ B₂ h₁ h₂ <;> rw [@induced_id _ (_)]
-- need to specify all implicit arguments because multiple instances on the same type
-- would be easier if `TopologicalSpace` arguments in `TopologicalSpace.IsTopologicalBasis.inf`
-- are regular implicit rather than instance implicit

[Christopher Hoskin]

@Junyan Xu Thanks very much for your proof. I'm afraid the way Mathlib handles topologies is just a bit beyond the grasp of my intellect. I'm trying to apply your result to the Lawson Topology:

import Mathlib.Topology.Order.LowerUpperTopology
import Mathlib.Topology.Order.ScottTopology

open Set Topology TopologicalSpace

variable {X Y Z} [tY : TopologicalSpace Y] [tZ : TopologicalSpace Z] (fY : X → Y) (fZ : X → Z)

theorem induced_to_prod (f : X → Y × Z) :
    induced f inferInstance = induced (fun x ↦ (f x).1) tY ⊓ induced (fun x ↦ (f x).2) tZ := by
  erw [induced_inf]
  simp_rw [induced_compose]
  rfl

theorem inducing_inf_to_prod :
    @Inducing X (Y × Z) (induced fY tY ⊓ induced fZ tZ) _ fun x ↦ (fY x, fZ x) :=
  letI := induced fY tY ⊓ induced fZ tZ; ⟨(induced_to_prod fun x ↦ (fY x, fZ x)).symm⟩

theorem TopologicalSpace.IsTopologicalBasis.inf
    {BY : Set (Set Y)} {BZ : Set (Set Z)} (bY : IsTopologicalBasis BY) (bZ : IsTopologicalBasis BZ) :
    @IsTopologicalBasis X (induced fY tY ⊓ induced fZ tZ) (BY.image2 (fY ⁻¹' · ∩ fZ ⁻¹' ·) BZ) := by
  letI := induced fY tY ⊓ induced fZ tZ
  convert (bY.prod bZ).inducing (inducing_inf_to_prod fY fZ)
  rw [Set.image_image2]; rfl

example {t₁ t₂ B₁ B₂} (h₁ : @IsTopologicalBasis X t₁ B₁) (h₂ : @IsTopologicalBasis X t₂ B₂) :
    @IsTopologicalBasis X (t₁ ⊓ t₂) (Set.image2 (· ∩ ·) B₁ B₂) := by
  convert @IsTopologicalBasis.inf X X X t₁ t₂ id id B₁ B₂ h₁ h₂ <;> rw [@induced_id _ (_)]
-- need to specify all implicit arguments because multiple instances on the same type
-- would be easier if `TopologicalSpace` arguments in `TopologicalSpace.IsTopologicalBasis.inf`
-- are regular implicit rather than instance implicit

namespace Topology

variable {α : Type*}

variable [Preorder α]

/--
The Lawson topology is defined as the meet of the `LowerTopology` and the `ScottTopology`.
-/
def lawson : TopologicalSpace α := lower α ⊓ scott

variable (α) [TopologicalSpace α]

/-
The Lawson topology is defined as the meet of the `LowerTopology` and the `ScottTopology`.
-/
class IsLawson : Prop where
  topology_eq_lawson : ‹TopologicalSpace α› = lawson

/--
The sets of the form U\↑F where U is Scott open and F is finite form a basis for the Lawson
topology
-/
def lawsonBasis := (image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1)
    (IsLower.lowerBasis (WithLower α)) {U | @IsOpen (WithScott α) _ U})

namespace IsLawson

variable [TopologicalSpace α] [IsLawson α]

lemma topology_eq : ‹_› = lawson := topology_eq_lawson

protected theorem isTopologicalBasis : TopologicalSpace.IsTopologicalBasis (lawsonBasis α) := by
  rw [lawsonBasis]
  convert IsTopologicalBasis.inf WithLower.toLower WithScott.toScott IsLower.isTopologicalBasis (TopologicalSpace.isTopologicalBasis_opens (α := WithScott α))
  erw [topology_eq α]
  rw [lawson]
  apply (congrArg₂ Inf.inf _) _
  sorry
  sorry

end IsLawson

end Topology

Is this the right idea? I reduce it to the goals

scott = induced (⇑WithScott.toScott) WithScott.instTopologicalSpaceWithScott

and

lower α = induced (⇑WithLower.toLower) WithLower.instTopologicalSpaceWithLower

but then I'm not sure what to do next (or if this is just nonsense)?

Thanks,

Christopher

[Ruben Van de Velde]

I think you rather want to create Lawson as a type alias for \a and define an instance : TopologicalSpace (Lawson \a)

[Jireh Loreaux]

@Christopher Hoskin Ruben may be right, but your goals are easily provable.

example {α : Type*} [Preorder α] :
    lower α = induced WithLower.toLower WithLower.instTopologicalSpaceWithLower := by
  letI _ := lower α; exact @IsLower.WithLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩ |>.inducing.induced

[Yaël Dillies]

Ruben Van de Velde said:

I think you rather want to create Lawson as a type alias for α and define an instance : TopologicalSpace (Lawson α)

This is not really the pattern in this part of the library (or rather the pattern is to have both the type synonym and the topology on the original space)

[Christopher Hoskin]

I left out the type synonym and some of the other boilerplate for a MWE, but I have it in the file I'm working on.

[Christopher Hoskin]

@Yaël Dillies we have:

def lower (α : Type*) [Preorder α] : TopologicalSpace α

but

variable {α β : Type*}
variable [Preorder α]
...
def scottHausdorff : TopologicalSpace α where
...
def scott : TopologicalSpace α := upperSet α ⊔ scottHausdorff

Presumably it should be:

def scottHausdorff (α : Type*) [Preorder α]  : TopologicalSpace α where
...
def scott (α : Type*) [Preorder α]  : TopologicalSpace α := upperSet α ⊔ scottHausdorff α

to be consistent?

[Yaël Dillies]

Hmm yeah, α should be explicit in scottHausdorff

[Yaël Dillies]

Sorry I didn't catch that in review

[Christopher Hoskin]

Similarly we have:

#check IsLower.WithLowerHomeomorph

but

#check WithScott.withScottHomeomorph

which is right?

[Yaël Dillies]

The latter

[Christopher Hoskin]

I'll do a PR to make it consistent then.

[Christopher Hoskin]

https://github.com/leanprover-community/mathlib4/pull/10346

[Christopher Hoskin]

This works:

example {α : Type*} [Preorder α] :
    lower α = induced WithLower.toLower WithLower.instTopologicalSpaceWithLower := by
  letI _ := lower α; exact @WithLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩ |>.inducing.induced

But this fails with (deterministic) timeout at 'isDefEq', maximum number of heartbeats (1000000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

set_option maxHeartbeats 1000000 in
example {α : Type*} [Preorder α] :
    scott α = induced WithScott.toScott WithScott.instTopologicalSpaceWithScott := by
  letI _ := scott α; exact @WithScott.withScottHomeomorph α ‹_› (scott α) ⟨rfl⟩ |>.inducing.induced

[Jireh Loreaux]

I think you want the symm of that homeomorphism, but I'm not at Lean to check. You might also try providing the arguments to IsScott.mk explicitly instead of hiding them behind the anonymous constructor with rfl.

[Anatole Dedecker]

Coming back to the original question, I still think it's cleaner to do (all code below is with the environment of docs#IsTopologicalBasis.prod)

protected theorem IsTopologicalBasis.inf {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)}
    (h₁ : IsTopologicalBasis (t := t₁) B₁) (h₂ : IsTopologicalBasis (t := t₂) B₂) :
    IsTopologicalBasis (t := t₁ ⊓ t₂) (image2 (· ∩ ·) B₁ B₂) := by
  let  _: TopologicalSpace β := t₁ ⊓ t₂
  refine isTopologicalBasis_of_isOpen_of_nhds (t := _) ?_ ?_
  · rintro _ ⟨u₁, hu₁, u₂, hu₂, rfl⟩
    exact ((h₁.isOpen (t := t₁) hu₁).mono inf_le_left).inter
      ((h₂.isOpen (t := t₂) hu₂).mono inf_le_right)
  · rintro x u hu uo
    rcases (nhds_inf (a := x)).symm ▸ (h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))
      |>.mem_iff.1 (uo.mem_nhds hu) with ⟨⟨s, t⟩, ⟨⟨hs, ha⟩, ht, hb⟩, hu⟩
    exact ⟨s ∩ t, mem_image2_of_mem hs ht, ⟨ha, hb⟩, hu⟩

and then change the prod theorem to

protected theorem IsTopologicalBasis.induced [s : TopologicalSpace β] (f : α → β)
    {T : Set (Set β)} (h : IsTopologicalBasis T) :
    IsTopologicalBasis (t := induced f s) ((preimage f) '' T) :=
  h.inducing (t := induced f s) (inducing_induced f)

protected theorem IsTopologicalBasis.prod {β} [TopologicalSpace β] {B₁ : Set (Set α)}
    {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) :
    IsTopologicalBasis (image2 (· ×ˢ ·) B₁ B₂) := by
  have := (h₁.induced Prod.fst).inf (h₂.induced Prod.snd)
  rwa [image2_image_left, image2_image_right] at this

[Anatole Dedecker]

Did anyone make a PR out of Junyan's version already? If not I'll open a PR with this and other cleanups in this file.

[Christopher Hoskin]

Anatole Dedecker said:

Did anyone make a PR out of Junyan's version already? If not I'll open a PR with this and other cleanups in this file.

@Anatole Dedecker I've been experimenting with it locally, but have done nothing towards preparing a PR, so I'd be very happy for you to go ahead.

[Anatole Dedecker]

#10732

[Christopher Hoskin]

This seems to work:

def lawson_basis := (image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1)
  (IsLower.lowerBasis (WithLower α)) {U | @IsOpen (WithScott α) _ U})

protected theorem isTopologicalBasis : TopologicalSpace.IsTopologicalBasis (lawson_basis α) := by
  rw [lawson_basis]
  convert IsTopologicalBasis.inf_induced (γ := α) IsLower.isTopologicalBasis
    (TopologicalSpace.isTopologicalBasis_opens (α := WithScott α)) WithLower.toLower WithScott.toScott
  erw [topology_eq α]
  rw [lawson]
  apply (congrArg₂ Inf.inf _) _
  letI _ := lower α; exact @IsLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩ |>.inducing.induced
  letI _ := scott α; exact @IsScott.withScottHomeomorph α _ (scott α) ⟨rfl⟩ |>.inducing.induced