SpectralClosedRestriction.lean

lemma generizations_eq_iInter_compactOpens [PrespectralSpace X]
    {A : Set X} (hA : IsCompact A) :
    {x : X | ∃ z ∈ A, x ⤳ z} =
      ⋂ U : {U : Set X // IsOpen U ∧ IsCompact U ∧ A ⊆ U}, (U : Set X)

lemma isClosed_constructible_generizations [PrespectralSpace X]
    {A : Set X} (hA : IsCompact A) :
    IsClosed ((WithTopology.ofTopology : WithConstructibleTopology X → X) ⁻¹'
      {x : X | ∃ z ∈ A, x ⤳ z})

lemma exists_specializes_of_mem_closure [SpectralSpace X]
    {A : Set X}
    (hA : IsClosed ((WithTopology.ofTopology : WithConstructibleTopology X → X) ⁻¹' A))
    {x : X} (hx : x ∈ closure A) : ∃ a ∈ A, a ⤳ x

lemma isClosed_of_constructible_closed_specialization [SpectralSpace X]
    {A : Set X}
    (hA : IsClosed ((WithTopology.ofTopology : WithConstructibleTopology X → X) ⁻¹' A))
    (hstable : ∀ ⦃x y : X⦄, x ∈ A → x ⤳ y → y ∈ A) : IsClosed A

theorem exists_clopen_partition_of_connected_closed_intersections [SpectralSpace X]
    {Z A B : Set X} (hA : IsClosed A) (hB : IsClosed B)
    (hAB : A ∪ B = Z) (hdisjoint : Disjoint A B)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X))) :
    ∃ W : Set X, IsClopen W ∧ W ∩ Z = A ∧ Wᶜ ∩ Z = B

theorem clopen_restriction_bijective [SpectralSpace X] {Z : Set X}
    (hZ : IsClosed Z)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X))) :
    Function.Bijective (fun W : Clopens X =>
      (⟨Subtype.val ⁻¹' (W : Set X),
        W.isClopen.preimage continuous_subtype_val⟩ : Clopens Z)) := by
  classical
  constructor
  · intro U V hUV
    apply Clopens.ext
    ext x
    obtain ⟨z, hzZ, hxz⟩ := (hconnected x).nonempty
    have hspec : x ⤳ z := specializes_iff_mem_closure.mpr hxz
    have hzUV : z ∈ U ↔ z ∈ V :=
      Iff.of_eq (congrArg (fun W : Clopens Z => (⟨z, hzZ⟩ : Z) ∈ W) hUV)
    constructor
    · intro hxU
      exact hspec.mem_open V.isOpen (hzUV.mp (hspec.mem_closed U.isClosed hxU))
    · intro hxV
      exact hspec.mem_open U.isOpen (hzUV.mpr (hspec.mem_closed V.isClosed hxV))
  · intro U
    let A : Set X := Subtype.val '' (U : Set Z)
    let B : Set X := Subtype.val '' (U : Set Z)ᶜ
    have hA : IsClosed A := hZ.isClosedMap_subtype_val _ U.isClosed
    have hB : IsClosed B := hZ.isClosedMap_subtype_val _ U.isOpen.isClosed_compl
    have hAB : A ∪ B = Z := by
      ext x
      constructor
      · rintro (⟨z, hz, rfl⟩ | ⟨z, hz, rfl⟩) <;> exact z.2
      · intro hx
        by_cases hxU : (⟨x, hx⟩ : Z) ∈ U
        · exact Or.inl ⟨⟨x, hx⟩, hxU, rfl⟩
        · exact Or.inr ⟨⟨x, hx⟩, hxU, rfl⟩
    have hdis : Disjoint A B := by
      apply Set.disjoint_left.mpr
      rintro x ⟨a, ha, hax⟩ ⟨b, hb, hbx⟩
      have hab : a = b := Subtype.ext (hax.trans hbx.symm)
      exact hb (hab ▸ ha)
    obtain ⟨W, hW, hWA, hWB⟩ :=
      exists_clopen_partition_of_connected_closed_intersections
        hA hB hAB hdis hconnected
    refine ⟨⟨W, hW⟩, Clopens.ext ?_⟩
    ext z
    change z.1 ∈ W ↔ z ∈ U
    constructor
    · intro hzW
      have hzA : z.1 ∈ A := hWA ▸ ⟨hzW, z.2⟩
      obtain ⟨a, ha, haz⟩ := hzA
      exact (Subtype.ext haz : a = z) ▸ ha
    · intro hzU
      have hzA : z.1 ∈ A := ⟨z, hzU, rfl⟩
      exact (show z.1 ∈ W ∩ Z from hWA.symm ▸ hzA).1

theorem locallyConstant_restriction_bijective [SpectralSpace X] {Z : Set X}
    (hZ : IsClosed Z)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X)))
    (S : Type*) :
    Function.Bijective (LocallyConstant.comap
      (⟨Subtype.val, continuous_subtype_val⟩ : C(Z, X)) :
        LocallyConstant X S → LocallyConstant Z S)