Cubes & Vectors

cube.lean

import analysis.real data.finsupp linear_algebra
import .vec


noncomputable theory

local attribute [instance] classical.prop_decidable

universes u v w x
variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}

section constructions
local notation `cont` := @continuous _ _
open topological_space lattice

variable {f : α → β}

lemma continuous_Sup_rng {t₁ : topological_space α} {t₂ : set (topological_space β)}
  (h : ∀t∈t₂, cont t₁ t f) : cont t₁ (Sup t₂) f :=
continuous_iff_le_coinduced.2 $ Sup_le $ assume t ht, continuous_iff_le_coinduced.1 $ h _ ht

lemma continuous_Sup_dom {t₁ : set (topological_space α)} {t₂ : topological_space β}
  {t : topological_space α} (h₁ : t ∈ t₁) (hf : cont t t₂ f) : cont (Sup t₁) t₂ f :=
continuous_iff_induced_le.2 $ le_Sup_of_le h₁ $ continuous_iff_induced_le.1 hf

lemma continuous_supr_rng {t₁ : topological_space α} {t₂ : ι → topological_space β}
  (h : ∀i, cont t₁ (t₂ i) f) : cont t₁ (supr t₂) f :=
continuous_Sup_rng $ assume t ⟨i, hi⟩, hi.symm ▸ h i

lemma continuous_supr_dom {t₁ : ι → topological_space α} {t₂ : topological_space β}
  (i : ι) (h : cont (t₁ i) t₂ f) : cont (supr t₁) t₂ f :=
continuous_Sup_dom ⟨i, rfl⟩ h

end constructions

@[simp] lemma vector.nth_zero {n : ℕ} {a : α} {v : vector α n} : (a :: v).nth 0 = a :=
by cases v; refl

@[simp] lemma vector.nth_succ {n : ℕ} {a : α} {i : fin n} {v : vector α n} : (a :: v).nth i.succ = v.nth i :=
by cases v with v hv; cases i with i hi; refl

namespace vector

instance (n : ℕ) [t : topological_space α] : topological_space (vector α n) :=
⨆(i:fin n), t.induced (λv, v.nth i)

lemma continuous_vector_rng [topological_space α] [topological_space β] {n : ℕ} {f : β → vector α n}
  (h : ∀i (hi : i < n), continuous (λb, (f b).nth ⟨i, hi⟩)) : continuous f :=
continuous_supr_rng $ assume ⟨i, hi⟩, continuous_induced_rng $ h i hi

lemma continuous_vector_apply [topological_space α] {n : ℕ} {i : fin n} : continuous (λx:vector α n, x.nth i) :=
by apply continuous_supr_dom i _; apply continuous_induced_dom

lemma continuous_cons [topological_space α] [topological_space β] {n : ℕ}
  {f : α → β} {g : α → vector β n} (hf : continuous f) (hg : continuous g) :
  continuous (λa, f a :: g a) :=
continuous_vector_rng $ assume i hi,
match i, hi with
| 0,     h := show continuous (λa, (f a :: g a).nth 0), by simp [hf]
| (i+1), h :=
  have i < n, from nat.lt_of_succ_lt_succ h,
  show continuous (λa, (f a :: g a).nth (⟨i, this⟩ : fin n).succ),
    by simp; exact hg.comp continuous_vector_apply
end

end vector


namespace singular_homology

def unit_interval : Type := {r : ℝ // 0 ≤ r ∧ r ≤ 1}
namespace unit_interval

instance : topological_space unit_interval :=
by unfold unit_interval; apply_instance

instance : has_zero unit_interval := ⟨⟨0, le_refl 0, zero_le_one⟩⟩
instance : has_one unit_interval := ⟨⟨1, zero_le_one, le_refl 1⟩⟩

end unit_interval

def unit_cube : ℕ → Type := vector unit_interval

namespace unit_cube

instance (n : ℕ) : topological_space (unit_cube n) :=
⨆(i:fin n), unit_interval.topological_space.induced (λv:unit_cube n, v.nth i)

lemma continuous_unit_cube_rng [topological_space β] {n : ℕ} {f : β → unit_cube n}
  (h : ∀i (hi : i < n), continuous (λb, (f b).nth ⟨i, hi⟩)) : continuous f :=
continuous_supr_rng $ assume ⟨i, hi⟩, continuous_induced_rng $ h i hi

lemma continuous_unit_cube_apply {n : ℕ} {i : fin n} : continuous (λx:unit_cube n, x.nth i) :=
by apply continuous_supr_dom i _; apply continuous_induced_dom


lemma continuous_insert {α : Type*} [topological_space α] {n : ℕ} {i : fin (n + 1)}
  {f : α → unit_interval} {g : α → unit_cube n} :
  continuous (λa, (g a).insert_at (f a) i) :=
_

end unit_cube

def degenerate {n : ℕ} (f : unit_cube n → α) : Prop :=
∃i:fin n, ∀x y : unit_cube n, (∀j, j ≠ i → x j = y j) → f x = f y

def cube (α : Type u) [topological_space α] (n : ℕ) : Type u :=
{ f : unit_cube n → α // continuous f }

namespace cube
variables [topological_space α] [topological_space β] {n : ℕ}

def proj (i : fin n) (v : unit_interval) (c : cube α (n + 1)) : cube α n :=
⟨c.1 ∘ unit_cube.insert i v, continuous.comp unit_cube.continuous_insert c.2⟩

def map {f : α → β} (hf : continuous f) (c : cube α n) : cube β n :=
⟨f ∘ c.1, continuous.comp c.2 hf⟩

end cube

def cube_group (α : Type u) [topological_space α] (n : ℕ) : Type u :=
{c : cube α n // ¬ degenerate c.1} →₀ ℤ

namespace cube_group
variables [topological_space α] [topological_space β] {n : ℕ}
instance : add_comm_group (cube_group α n) := finsupp.add_comm_group
instance : module ℤ (cube_group α n) := finsupp.to_module

def sum [add_comm_group γ] (c : cube_group α n) (f : cube α n → γ) : γ :=
c.sum $ λx i, gsmul (f x) i

example [module ℤ γ] {f : cube α n → γ} : is_linear_map (λg:cube_group α n, g.sum f) :=
⟨assume g₁ g₂, finsupp.sum_add_index (assume a, gsmul_zero _) (assume a i₁ i₂, gsmul_add _ _ _),
  assume j g,
  calc _ = (finsupp.sum g $ λx i, gsmul (gsmul (f x) i) j) :
    by simp [sum, finsupp.sum_smul_index, gsmul_zero, (gsmul_mul _ _ _).symm, mul_comm]
    ... = _ : _⟩

instance : has_coe (cube α n) (cube_group α n) :=
⟨λc, if h : degenerate c.1 then 0 else finsupp.single ⟨c, h⟩ 1⟩

def boundary (g : cube_group α (n + 1)) : cube_group α n :=
g.sum $ λc, finset.univ.sum $ λi, c.proj i 0 - c.proj i 1

def map (f : α → β) (c : cube_group α n) : cube_group β n :=
if hf : continuous f then c.sum $ λc, c.map hf else 0

end cube_group

end singular_homology

vec.lean

import data.vector data.list

namespace list
variables {α : Type*} {a : α}

def insert_at (a : α) : ℕ → list α → list α
| 0     as       := a :: as
| (n+1) []       := [a]
| (n+1) (a'::as) := a' :: insert_at n as

def remove_at : ℕ → list α → list α
| _     []      := []
| 0     (a::as) := as
| (n+1) (a::as) := a :: remove_at n as

lemma length_insert_at : ∀n as, length (insert_at a n as) = length as + 1
| 0     as       := rfl
| (n+1) []       := rfl
| (n+1) (a'::as) := congr_arg nat.succ $ length_insert_at n as

lemma length_remove_at_add_one : ∀n (as : list α), n < length as →
  length (remove_at n as) + 1 = length as
| 0     (a::as) h := rfl
| (n+1) (a::as) h := congr_arg nat.succ $ length_remove_at_add_one n as $ nat.lt_of_succ_lt_succ h

lemma remove_at_insert_at : ∀n as, n ≤ length as →
  remove_at n (insert_at a n as) = as
| 0     []      h := rfl
| 0     (a::as) h := rfl
| (n+1) (a::as) h := congr_arg (cons a) $ remove_at_insert_at n as $ nat.le_of_succ_le_succ h

lemma insert_at_remove_at_of_gt : ∀n m as, n < length as → m > n →
  insert_at a m (remove_at n as) = remove_at n (insert_at a (m + 1) as)
| 0     (m+1) (a::as) has hmn := rfl
| (n+1) (m+1) (a::as) has hmn :=
  congr_arg (cons a) $
    insert_at_remove_at_of_gt n m as (nat.lt_of_succ_lt_succ has) (nat.lt_of_succ_lt_succ hmn)

lemma insert_at_remove_at_of_le : ∀n m as, n < length as → m ≤ n →
  insert_at a m (remove_at n as) = remove_at (n + 1) (insert_at a m as)
| n       0       (a :: as) has hmn := rfl
| (n + 1) (m + 1) (a :: as) has hmn :=
  congr_arg (cons a) $
    insert_at_remove_at_of_le n m as (nat.lt_of_succ_lt_succ has) (nat.le_of_succ_le_succ hmn)

end list

namespace vector
open list
variables {α : Type*} {a : α} {n : ℕ}

def insert_at (a : α) (i : fin (n+1)) (v : vector α n) : vector α (n+1) :=
⟨v.1.insert_at a i.1, eq.trans (length_insert_at i.1 v.1) $ congr_arg nat.succ v.2⟩

def remove_at (i : fin (n+1)) (v : vector α (n+1)) : vector α n :=
⟨v.1.remove_at i.1, nat.succ.inj $ eq.trans (length_remove_at_add_one _ _ $ v.2.symm ▸ i.2) v.2⟩

lemma remove_at_insert_at {v : vector α n} {i : fin (n+1)} : remove_at i (insert_at a i v) = v :=
subtype.eq $ remove_at_insert_at i.1 v.1 $ v.2.symm ▸ nat.le_of_succ_le_succ i.2

/-
lemma nth_insert_at_gt {v : vector α n} {i j : fin (n+1)} {a : α} :
  ∀(h : j < i), (v.insert_at a i).nth j = v.nth ⟨j.1, nat.lt_of_succ_lt_succ $ lt_of_le_of_lt h i.2⟩ :=
_
-/

end vector