Doubts on definition of topologies

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I'm trying to understand and use the several ways of constructing topologies that are already included in mathlib, but I don't really know how to acces its open sets.

For example, if I'm not mistaken, this three instances shold result in the same topology:

instance TopologicalSpace.instInitial {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace X where
    IsOpen U := ∀ x ∈ U, ∃ (G : Finset {U | ∃ (i : ι) (V : Set (Y i)), IsOpen V ∧ U = (F i) ⁻¹' V}), (∀ g ∈ G, x ∈ g.1) ∧ {y | ∀ g ∈ G, y ∈ g.1} ⊆ U
    isOpen_univ := by
      dsimp
      intro x xinuniv
      use ∅
      simp
    isOpen_inter := by
      dsimp
      intro U V U_open V_open x xinUV
      rcases U_open x xinUV.1 with ⟨GU, GUeq⟩
      rcases V_open x xinUV.2 with ⟨GV, GVeq⟩
      use GU ∪ GV
      constructor
      · intro g ginUV
        rw [Finset.mem_union] at ginUV
        rcases ginUV with ginU | ginV
        · exact GUeq.1 g ginU
        · exact GVeq.1 g ginV
      · intro y yin
        have interinU := GUeq.2
        have interinV := GVeq.2
        dsimp at yin
        constructor
        · apply interinU
          dsimp
          intro g' g'inGU
          exact yin g' (Finset.mem_union_left GV g'inGU)
        · apply interinV
          dsimp
          intro g' g'inGV
          exact yin g' (Finset.mem_union_right GU g'inGV)
    isOpen_sUnion := by
      dsimp
      intro s h x xinUs
      rcases xinUs with ⟨t, tins, xint⟩
      rcases h t tins x xint with ⟨G, eq⟩
      use G
      constructor
      · exact eq.1
      · apply le_trans eq.2
        intro z zint
        use t

instance TopologicalSpace.instInitial' {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace X := TopologicalSpace.generateFrom {U | ∃ (i : ι) (V : Set (Y i)), IsOpen V ∧ U = (F i) ⁻¹' V}

instance TopologicalSpace.instInitial'' {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace X := ⨅ (i : ι), TopologicalSpace.induced (F i) (h i)

So, one should be able to prove

lemma eq1 {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace.instInitial X Y h F = TopologicalSpace.instInitial' X Y h F := by
    sorry

lemma eq2 {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace.instInitial X Y h F = TopologicalSpace.instInitial'' X Y h F := by
    sorry

However, how can this be done?

I don't know how to simplify the open sets of the last two instances (the one using the infimum and the one using the generator set), so when in the proof it appears that some set is open with respect to one of those topologies, I don't know how to simplify the expression to obtain information about it.

On the other hand, I know that those two topologies are defined as infimums, so maybe the way to prove it is by stating that the first instance is the corresponding infimum in both cases? If so, how can this be done?

If possible, I'd like to know how to prove it both ways to learn as much as I can.

On the other hand, by using any of this instances I want to also define an instance for the weak topology with respect to a bilinear form (and a subset of the second space involved in the bilinear form, but that's not important here) . I know is already defined, but I also want to prove that my approach is the same as the implemented one.

For that, I've defined an structure for bilineal forms (that I also know now that it can be simplified to E →ₗ[𝕂] F →ₗ[𝕂] 𝕂)

/- Definition of bilinear forms and the "symmetrical" bilineal form associated to a given one -/

structure BilinearForm (E F 𝕂 : Type) [RCLike 𝕂] [AddCommGroup E] [Module 𝕂 E] [AddCommGroup F] [Module 𝕂 F] where
  toFun : E → F → 𝕂
  right_linear : ∀ (f : F), IsLinearMap 𝕂 (fun (e : E) ↦ toFun e f)
  left_linear : ∀ (e : E), IsLinearMap 𝕂 (fun (f : F) ↦ toFun e f)

instance [RCLike 𝕂] [AddCommGroup E] [Module 𝕂 E] [AddCommGroup F] [Module 𝕂 F] :
  CoeFun (BilinearForm E F 𝕂) (fun _ ↦ E → F → 𝕂) where
    coe := BilinearForm.toFun

attribute [coe] BilinearForm.toFun

instance BilinearForm' {E F 𝕂 : Type} [RCLike 𝕂] [AddCommGroup E] [Module 𝕂 E] [AddCommGroup F] [Module 𝕂 F]  (B : BilinearForm E F 𝕂) : BilinearForm F E 𝕂 where
  toFun := fun f e ↦ B e f
  right_linear := B.left_linear
  left_linear := B.right_linear

/- Associated map to a bilineal form -/

def AsocMap {E F 𝕂 : Type} [RCLike 𝕂] [AddCommGroup E] [Module 𝕂 E] [AddCommGroup F] [Module 𝕂 F]
            (B : BilinearForm E F 𝕂) : E → Dual 𝕂 F := fun e ↦
            {
              toFun := fun f ↦ B e f
              map_add' := by
                intro f f'
                dsimp
                exact (B.left_linear e).1 f f'
              map_smul' := by
                intro k f
                dsimp
                exact (B.left_linear e).2 k f
            }

theorem isLinearAsocMap {E F 𝕂 : Type} [RCLike 𝕂] [AddCommGroup E] [Module 𝕂 E] [AddCommGroup F] [Module 𝕂 F]
            (B : BilinearForm E F 𝕂) : IsLinearMap 𝕂 (AsocMap B) := by
              constructor
              · intro e e'
                ext f
                dsimp [AsocMap]
                exact (B.right_linear f).1 e e'
              · intro k e
                ext f
                dsimp [AsocMap]
                exact (B.right_linear f).2 k e

Then, the instance for the weak topology (I also know it can be defined in a simpler way as it is implemented in mathlib, but I want to make it work with this equivalent definition) should be something like

instance WeakTopology (E : Type) {F 𝕂 : Type} [RCLike 𝕂] [AddCommGroup E] [Module 𝕂 E] [AddCommGroup F] [Module 𝕂 F]
                      (B: BilinearForm E F 𝕂) (H : Set F) : TopologicalSpace E :=
                        TopologicalSpace.instInitial E (fun (h : H) ↦ 𝕂)
                        (by intro i; dsimp; sorry)
                        (fun (h : H) ↦ (AsocMap (BilinearForm' B) h))

However, I have two problems.

The first one is that it appeart the following error :

´cannot find synthesization order for instance WeakTopology with type
(E : Type) →
{F 𝕂 : Type} →
[inst : RCLike 𝕂] →
[inst_1 : AddCommGroup E] →
[inst_2 : Module 𝕂 E] →
[inst_3 : AddCommGroup F] → [inst_4 : Module 𝕂 F] → BilinearForm E F 𝕂 → Set F → TopologicalSpace E
all remaining arguments have metavariables:
AddCommGroup ?F
@Module 𝕂 ?F DivisionSemiring.toSemiring AddCommGroup.toAddCommMonoid´

And, the second one, that I don't know how to substitute the "sorry" by a correct proof that 𝕂 is a topological space. I cannot find any instance for it.

Thanks in advance.

[Esteban Martínez Vañó]

Esteban Martínez Vañó ha dicho:

And, the second one, that I don't know how to substitute the "sorry" by a correct proof that 𝕂 is a topological space. I cannot find any instance for it.

I think I've solved this problem:

instance RCLike.instTopologicalSpace {𝕂 : Type} [RCLike 𝕂] : TopologicalSpace 𝕂 := RCLike.toDenselyNormedField.toNormedField.toMetricSpace.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace

Is there an easier way of expressing it?

[Johan Commelin]

cc @Yury G. Kudryashov

[Yury G. Kudryashov]

Esteban Martínez Vañó said:

Esteban Martínez Vañó ha dicho:

And, the second one, that I don't know how to substitute the "sorry" by a correct proof that 𝕂 is a topological space. I cannot find any instance for it.

I think I've solved this problem:

instance RCLike.instTopologicalSpace {𝕂 : Type} [RCLike 𝕂] : TopologicalSpace 𝕂 := RCLike.toDenselyNormedField.toNormedField.toMetricSpace.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace

Is there an easier way of expressing it?

inferInstance

[Yury G. Kudryashov]

If I don't reply with more details in 24h, then please ping me again.

[Esteban Martínez Vañó]

cc @Yury G. Kudryashov

[Yury G. Kudryashov]

About 1st error: this can't be an instance, only a def, because Lean can't find K, F, and B based on E.

[Yury G. Kudryashov]

About equality of topologies: for existing constructions (2nd and 3rd definitions), you can use docs#Set.setOf_exists docs#generateFrom_iUnion_isOpen docs#isOpen_induced_iff

[Yury G. Kudryashov]

For equality to your custom definition, you can use docs#TopologicalSpace.IsTopologicalBasis.isOpen_iff together with constructors for IsTopologicalBasis.

[Esteban Martínez Vañó]

Okay, I've made some progress. But, how can you go from Finset to Finite?

Because after obtaining a basis for the second construction, the sets they use are Finite, but I've defined my topology with the Finset class.

[Esteban Martínez Vañó]

I mean, in general, how can one prove that a set is Finite? Because I find it quite difficult

[Edward van de Meent]

show that Set.card is positive, or Set.encard is not top.

[Edward van de Meent]

i understand that that might not be a very helpful answer, but i'm not exactly sure what the context of the question is.

[Edward van de Meent]

do you have a #mwe ?

[Esteban Martínez Vañó]

This is what I've done.

import Mathlib.Topology.Bases

set_option linter.unusedVariables false

open Set Filter Topology Classical Function

instance TopologicalSpace.instInitial {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace X where
    IsOpen U := ∀ x ∈ U, ∃ (G : Finset {U | ∃ (i : ι) (V : Set (Y i)), IsOpen V ∧ U = (F i) ⁻¹' V}), (∀ g ∈ G, x ∈ g.1) ∧ {y | ∀ g ∈ G, y ∈ g.1} ⊆ U
    isOpen_univ := by
      dsimp
      intro x xinuniv
      use ∅
      simp
    isOpen_inter := by
      dsimp
      intro U V U_open V_open x xinUV
      rcases U_open x xinUV.1 with ⟨GU, GUeq⟩
      rcases V_open x xinUV.2 with ⟨GV, GVeq⟩
      use GU ∪ GV
      constructor
      · intro g ginUV
        rw [Finset.mem_union] at ginUV
        rcases ginUV with ginU | ginV
        · exact GUeq.1 g ginU
        · exact GVeq.1 g ginV
      · intro y yin
        have interinU := GUeq.2
        have interinV := GVeq.2
        dsimp at yin
        constructor
        · apply interinU
          dsimp
          intro g' g'inGU
          exact yin g' (Finset.mem_union_left GV g'inGU)
        · apply interinV
          dsimp
          intro g' g'inGV
          exact yin g' (Finset.mem_union_right GU g'inGV)
    isOpen_sUnion := by
      dsimp
      intro s h x xinUs
      rcases xinUs with ⟨t, tins, xint⟩
      rcases h t tins x xint with ⟨G, eq⟩
      use G
      constructor
      · exact eq.1
      · apply le_trans eq.2
        intro z zint
        use t

lemma TopologicalSpace.instInitial.isOpen {ι: Type} {X : Type} {Y : ι → Type u} {h : ∀ (i : ι), TopologicalSpace (Y i)}
  {F: (i : ι) → (X → (Y i))} (U: Set X) : @IsOpen X (TopologicalSpace.instInitial X Y h F) U ↔ ∀ x ∈ U, ∃ (G : Finset {U | ∃ (i : ι) (V : Set (Y i)), IsOpen V ∧ U = (F i) ⁻¹' V}), (∀ g ∈ G, x ∈ g.1) ∧ {y | ∀ g ∈ G, y ∈ g.1} ⊆ U := by
    rfl

instance TopologicalSpace.instInitial' {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace X := TopologicalSpace.generateFrom {U | ∃ (i : ι) (V : Set (Y i)), IsOpen V ∧ U = (F i) ⁻¹' V}

lemma eq1 {ι: Type} (X : Type) (Y : ι → Type u) (h : ∀ (i : ι), TopologicalSpace (Y i))
  (F: (i : ι) → (X → (Y i))) : TopologicalSpace.instInitial X Y h F = TopologicalSpace.instInitial' X Y h F := by
    have : @TopologicalSpace.IsTopologicalBasis X (TopologicalSpace.instInitial' X Y h F)
      ((fun (f : Set (Set X)) => ⋂₀ f) '' {f : Set (Set X) | f.Finite ∧ f ⊆ {U | ∃ i V, IsOpen V ∧ U = F i ⁻¹' V}}) := by
        apply @TopologicalSpace.isTopologicalBasis_of_subbasis X (TopologicalSpace.instInitial' X Y h F) {U | ∃ (i : ι) (V : Set (Y i)), IsOpen V ∧ U = (F i) ⁻¹' V} _
        rfl
    ext U
    constructor
    · intro Uopen
      rw [@TopologicalSpace.IsTopologicalBasis.isOpen_iff X (TopologicalSpace.instInitial' X Y h F) U (((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {U | ∃ i V, IsOpen V ∧ U = F i ⁻¹' V}})) this]
      rw [TopologicalSpace.instInitial.isOpen] at Uopen
      intro a ainU
      rcases Uopen a ainU with ⟨G, aininter, interinU⟩
      use {y | ∀ g ∈ G, y ∈ g.1}
      constructor
      · rw [mem_image]
        let H := {x : Set X | ∃ g ∈ G, x = g.1}
        use H
        constructor
        · dsimp
          constructor
          · sorry
          · intro U UinH
            dsimp
            dsimp [H] at UinH
            rcases UinH with ⟨g, ginG, Ueqg⟩
            have := g.2
            rw [← Ueqg] at this
            assumption
        · ext x
          constructor
          · intro xininter
            rw [mem_sInter] at xininter
            dsimp
            intro g ginG
            have : g.1 ∈ H := by
              dsimp [H]
              use g
            exact xininter g.1 this
          · intro xin
            dsimp at xin
            rw [mem_sInter]
            intro t tinH
            dsimp [H] at tinH
            rcases tinH with ⟨g, ginG, teqg⟩
            rw [teqg]
            exact xin g ginG
      · constructor
        · dsimp
          assumption
        · assumption
    · sorry

The problem is with the first sorry (I haven't tried yet to prove the other one)

I've defined the set H := {x : Set X | ∃ g ∈ G, x = g.1} because it helps to prove everything else relatively easy, but I don't know how to prove it is finite (although it must be as G is a Finset)

[Edward van de Meent]

i'd say easiest way would be first define H' to be the (Finset-typed) image of G under the injective embedding given by fun g -> g.val , then use the coersion to Set of that.

[Edward van de Meent]

let me see if i can find the lemma for this...

[Yury G. Kudryashov]

There is docs#Finset.finite_toSet for one direction

[Edward van de Meent]

the issue is not just that, the types of the sets are different

[Yury G. Kudryashov]

And docs#Set.Finite.exists_finset for the other.

[Edward van de Meent]

you need to insert a casting from a subtype to supertype.

[Yury G. Kudryashov]

Could you please extract the goal you want to prove?

[Yury G. Kudryashov]

You can use lift s to Set t using hs to go from s : Set α with hs : s ⊆ t to Set t, similarly for s : Finset s

[Edward van de Meent]

Edward van de Meent said:

let me see if i can find the lemma for this...

i was thinking of docs#Finset.image

[Edward van de Meent]

showing that that is finite should be easy

[Yury G. Kudryashov]

It's (s.image Subtype.val).finite_toSet

[Esteban Martínez Vañó]

Thanks to both! I've managed to prove the first equivalence following all of your coments.
I'll try the second one when I have some time, but I suppose that with all this information I should be able to do it.

[Patrick Massot]

The most relevant answer to the original question is probably: why do you want to do with a description of those open sets that you couldn’t do much more easily with the formula ⨅ (i : ι), TopologicalSpace.induced (F i) (h i)?

[Esteban Martínez Vañó]

I just wanted to show that all three where the same as an exercise, because by doing it I knew I will learn how to work with the different ways of defining topologies in Lean

[Esteban Martínez Vañó]

And it has worked by the way. I've learned a lot :)

[Patrick Massot]

Learning is great, but I’m still a bit worried that you learned stuff that will help you fight Mathlib instead of using it happily.

[Esteban Martínez Vañó]

In practice I'll always use mathlib's definitions and theorems, but I also like to implement them myself to see how it can be done and compare it with how it is already done. I don't think I'm fighting agains Mathlib (or I don't intend to do it). Anyways, I'll take your concern into account for the future