discreteLocalConfigSpace

formal source

  97
  98/-- A discrete configuration space where every subset is a neighborhood.
  99    This is the "maximally fine" locality structure. -/
 100def discreteLocalConfigSpace (C : Type*) [Nonempty C] : LocalConfigSpace C where
 101  nonempty := inferInstance
 102  N := fun c => {U : Set C | c ∈ U}
 103  mem_of_mem_N := fun c U hU => hU
 104  N_nonempty := fun c => ⟨Set.univ, mem_univ c⟩
 105  intersection_closed := fun c U V hU hV => ⟨U ∩ V, ⟨hU, hV⟩, Subset.rfl⟩
 106  refinement := fun c U c' hU hc' => ⟨U, hc', Subset.rfl⟩
 107
 108/-! ## Trivial Configuration Space -/
 109
 110/-- A trivial configuration space where only the whole space is a neighborhood.
 111    This is the "maximally coarse" locality structure. -/
 112def trivialLocalConfigSpace (C : Type*) [Nonempty C] : LocalConfigSpace C where
 113  nonempty := inferInstance
 114  N := fun _ => {Set.univ}
 115  mem_of_mem_N := fun c U hU => by
 116    simp only [Set.mem_singleton_iff] at hU
 117    rw [hU]
 118    exact mem_univ c
 119  N_nonempty := fun _ => ⟨Set.univ, rfl⟩
 120  intersection_closed := fun _ U V hU hV => by
 121    simp only [Set.mem_singleton_iff] at hU hV
 122    subst hU hV
 123    exact ⟨Set.univ, rfl, Set.inter_self _ ▸ Subset.rfl⟩
 124  refinement := fun _ U _ hU _ => by
 125    simp only [Set.mem_singleton_iff] at hU
 126    exact ⟨Set.univ, rfl, hU ▸ Subset.rfl⟩
 127
 128/-! ## Module Status -/
 129
 130def locality_status : String :=