Graph-Theoretic Geometry

graph_theoretic_geometry.lean

import Mathlib

class Grph (G : Type) where
  edge : G → G → Prop
open Grph

variable {G H : Type} [Grph G] [Grph H]

structure Hom (G H : Type) [Grph G] [Grph H] where
  obj : G → H
  pres : ∀ {g1 g2 : G}, edge g1 g2 → edge (obj g1) (obj g2)

instance topHom [TopologicalSpace H] : TopologicalSpace (Hom G H) :=
  TopologicalSpace.induced (fun f => f.obj) inferInstance

/--
If X is a hausdorff space, and q is a surjective set map G → H, then
the set of maps G → X that factor through q is a closed subset of
all maps G → X.
-/
lemma factors_closed {X G H : Type} (q : G → H) (hq : Function.Surjective q) [TopologicalSpace X] [T2Space X] :
    IsClosed { g : G → X | ∃ h : H → X, g = h ∘ q } := by
  have : {g : G → X | ∃ h : H → X, g = h ∘ q} =
         {g : G → X | ∀ g₁ g₂, q g₁ = q g₂ → g g₁ = g g₂} := by
    ext g
    constructor
    · rintro ⟨h, hh⟩
      simp only [Set.mem_setOf_eq]
      rw [hh]
      simp only [Function.comp_apply]
      tauto
    · intro hg
      simp only [Set.mem_setOf_eq] at hg
      use (g ∘ Function.surjInv hq); ext; apply hg
      simp [Function.surjInv_eq]
  rw [this]
  have : {g : G → X | ∀ g₁ g₂, q g₁ = q g₂ → g g₁ = g g₂} =
         ⋂ g₁, ⋂ g₂, {g | q g₁ = q g₂ → g g₁ = g g₂} := by
    ext; simp
  rw [this]
  apply isClosed_iInter; intro g₁
  apply isClosed_iInter; intro g₂
  by_cases h : q g₁ = q g₂
  · simp [h]
    refine isClosed_eq (by fun_prop) (by fun_prop)
  · simp [h]

lemma factors_closed2 {X H : Type} [Grph X] (q : G → H)
    (hq : Function.Surjective q) [TopologicalSpace X] [T2Space X] :
    IsClosed { x : Hom G X | ∃ h : H → X, x.obj = h ∘ q } :=
  IsClosed.preimage continuous_induced_dom (factors_closed q hq)

def EdgeSurjective {G H : Type} [Grph G] [Grph H] (q : G → H) : Prop :=
  ∀ h1 h2 : H, edge h1 h2 → ∃ g1 g2 : G, edge g1 g2 ∧ q g1 = h1 ∧ q g2 = h2

lemma edge_surjective_lemma {X : Type} [Grph X] {q : G → H}
    (heq : EdgeSurjective q) [TopologicalSpace X] [T2Space X] :
    { x : Hom G X | ∃ h : Hom H X, x.obj = h.obj ∘ q } =
    { x : Hom G X | ∃ h : H → X, x.obj = h ∘ q } := by
  ext x
  constructor
  · exact fun hx => (let ⟨h,e⟩ := hx; ⟨h.obj, e⟩)
  · intro hx
    simp_all only [Set.mem_setOf_eq]
    obtain ⟨ha, hb⟩ := hx
    let hh : Hom H X := {
      obj := ha,
      pres := by
        intro h1 h2 he
        obtain ⟨g1, g2, he', hq1, hq2⟩ := heq h1 h2 he
        rw [← hq1, ← hq2]
        change edge ((ha ∘ q) g1) ((ha ∘ q) g2)
        rw [← hb]
        exact x.pres he'
    }
    use hh

lemma factors_closed3 {X : Type} [Grph X] (q : G → H)
    (hq : Function.Surjective q) (heq : EdgeSurjective q) [TopologicalSpace X] [T2Space X] :
    IsClosed { x : Hom G X | ∃ h : Hom H X, x.obj = h.obj ∘ q } := by
  rw [edge_surjective_lemma heq]
  exact factors_closed2 q hq