Quotient additive commutative topological group

quotient_top_grop.lean

import analysis.topology.topological_structures
import group_theory.quotient_group

open function set

variables {α : Type*} [topological_space α] {β : Type*} [topological_space β]
variables {γ : Type*} [topological_space γ] {δ : Type*} [topological_space δ]

def is_open_map (f : α → β) := ∀ U : set α, is_open U → is_open (f '' U)

namespace is_open_map
protected lemma prod {f : α → β} {g : γ → δ} (hf : is_open_map f) (hg : is_open_map g) :
  is_open_map (λ p : α × γ, (f p.1, g p.2)) :=
begin
  intros s s_op,
  rw is_open_prod_iff,
  rintros b d ⟨⟨a, c⟩, ac_in, ac_bd⟩,
  change (f a, g c) = (b, d) at ac_bd,
  cases prod.mk.inj_iff.1 ac_bd with f_a g_c,
  rcases is_open_prod_iff.1 s_op a c ac_in with ⟨u, v, u_op, v_op, a_in, c_in, uv_s⟩,
  existsi [f '' u, g '' v, hf u u_op, hg v v_op],
  split,
  { rw ←f_a,
    exact mem_image_of_mem f a_in },
  { split,
    { rw ← g_c,
      exact mem_image_of_mem g c_in },
    { rw prod_image_image_eq,
      exact image_subset _ uv_s }}
end

lemma of_inverse {f : α → β} {g : β → α} (h : continuous g) (l_inv : left_inverse f g) (r_inv : right_inverse f g) :
  is_open_map f :=
begin
  intros s s_op,
  have : f '' s = g ⁻¹' s,
  { ext x,
    simp [mem_image_iff_of_inverse r_inv l_inv] },
  rw this,
  exact h s s_op
end

local attribute [extensionality] topological_space_eq

lemma quotient_map_of_open_of_surj_of_cont {f : α → β} (cont : continuous f) (op : is_open_map f) (surj : surjective f): quotient_map f :=
⟨surj, begin
  ext s,
  split; intro h,
  { exact cont s h },
  have := op (f ⁻¹' s) h,
  rwa image_preimage_eq surj at this,
end⟩
end is_open_map

variables [add_comm_group α] [topological_add_group α] (N : set α) [is_add_subgroup N]

instance [topological_add_group α] (N : set α) [is_add_subgroup N]: topological_space (quotient_add_group.quotient N) :=
by dunfold quotient_add_group.quotient ; apply_instance

open quotient_add_group

lemma quotient_group_saturate (s : set α) :
  (coe : α → quotient N) ⁻¹' ((coe : α → quotient N) '' s) = (⋃ x : N, (λ y, x.1 + y) '' s) :=
begin
  ext x,
  rw mem_preimage_eq,
  rw mem_Union,
  split ; intro h,
  { rcases h with ⟨a, a_in, h⟩,
    rw quotient_add_group.eq at h,
    existsi (⟨-a+x, h⟩ : N),
    rw mem_image,
    existsi [a, a_in],
    simp },
  { rcases h with ⟨⟨n, n_in⟩, x_in⟩,
    rw mem_image at x_in,
    rcases x_in with ⟨a, a_in, ha⟩,
    rw mem_image,
    existsi [a, a_in],
    rw quotient_add_group.eq,
    rwa show -a + x = n, by rw ←ha ; simp }
end

lemma is_open_translate (a : α) : is_open_map (λ x, a + x) :=
begin
  have : continuous (λ x, -a + x) := continuous_add continuous_const continuous_id,
  apply is_open_map.of_inverse this,
  simp[function.left_inverse], intro x, rw [add_comm, add_assoc], simp,
  simp[function.left_inverse], intro x, finish
end

lemma quotient_group.open_coe : is_open_map (coe : α →  quotient N) :=
begin
  intros s s_op,
  change is_open ((coe : α →  quotient N) ⁻¹' (coe '' s)),
  rw quotient_group_saturate N s,
  apply is_open_Union,
  rintro ⟨n, _⟩,
  exact is_open_translate n s s_op
end

instance topological_add_group_quotient : topological_add_group (quotient N) :=
{ continuous_add := begin
    have cont : continuous ((coe : α → quotient N) ∘ (λ (p : α × α), p.fst + p.snd)) :=
    continuous.comp continuous_add' continuous_quot_mk,

    have quot : quotient_map (λ p : α × α, ((p.1:quotient N), (p.2:quotient N))),
    { apply is_open_map.quotient_map_of_open_of_surj_of_cont,
      { apply continuous.prod_mk,
        { exact continuous.comp continuous_fst continuous_quot_mk },
        { exact continuous.comp continuous_snd continuous_quot_mk } },
      { exact is_open_map.prod (quotient_group.open_coe N) (quotient_group.open_coe N) },
      { rintro ⟨⟨x⟩, ⟨y⟩⟩,
        existsi (x, y),
        refl }},
    exact (quotient_map.continuous_iff quot).2 cont,
  end,
  continuous_neg := begin
    apply continuous_quotient_lift,
    change continuous ((coe : α → quotient N) ∘ (λ (a : α), -a)),
    exact continuous.comp continuous_neg' continuous_quot_mk
  end }