main.lean

import analysis.complex.basic
import geometry.manifold.charted_space
import geometry.manifold.smooth_manifold_with_corners
import topology.category.Top.basic
import topology.constructions
import topology.local_homeomorph
import tactic.linear_combination
import tactic
import tactic.squeeze
import tactic.basic
import data.quot

namespace riemann_surfaces
@[class]
def rsurf (M: Type*) [topological_space M] [charted_space ℂ M] := smooth_manifold_with_corners (model_with_corners_self ℂ ℂ) M
private def pr_sph := ℂ ⊕ ℂ
noncomputable instance pr_sph.topological_space : topological_space pr_sph := sum.topological_space
private def eqv (p q: pr_sph) : Prop :=
(p=q)∨(∃ z w:ℂ, p=sum.inr z∧q=sum.inl w∧z*w=1∨p=sum.inl z∧q=sum.inr w∧z*w=1)
infix `~` := eqv
private theorem eqv.refl : ∀ p : pr_sph, p ~ p :=
begin
intro p,
rw eqv,
left,
split,
end

private theorem eqv.symm :
  ∀ p q : pr_sph, p ~ q → q ~ p :=
begin
intros p q h,
rw eqv,
cases h with h,
left,
exact eq.symm h,
cases h with z h,
cases h with w h,
cases h,
right,
use w,
use z,
right,
simp [h],
cases h with h1 h2,
cases h2 with h2 h3,
ring_nf,
exact h3,
right,
use w,
use z,
left,
finish,
end

private theorem eqv.trans :
  ∀ p q r : pr_sph, p ~ q → q ~ r → p ~ r :=
begin
intros p q r h g,
rw eqv,
cases h with h,
cases g with g,
left,
rw h,
exact g,

cases g with z g,
cases g with w g,
finish,
cases g,
cases h with z h,
cases h with w h,
cases h,
right,
use z,
use w,
finish,
right,
use z,
use w,
finish,
left,
cases_type* or and Exists,
exfalso,
finish,
repeat
begin
rw g_h_h_left at h_h_h_right_left,
injection h_h_h_right_left,
rw h_1 at g_h_h_right_right,
rw mul_comm at h_h_h_right_right,
have t:h_w=g_h_w := inv_unique h_h_h_right_right g_h_h_right_right,
rw h_h_h_left,
rw g_h_h_right_left,
rw t,
end,
exfalso,
finish,
end

private theorem is_equivalence : equivalence eqv :=
mk_equivalence eqv eqv.refl eqv.symm eqv.trans

instance rsph.setoid : setoid pr_sph :=
setoid.mk eqv is_equivalence

definition rsph := quotient rsph.setoid

noncomputable instance decidable_eqv: Π (a b : pr_sph), decidable (eqv a b) :=
begin
intros a b,
exact classical.dec (a~b)
end

attribute [derive decidable_eq] rsph

namespace rsph

definition mk (p:pr_sph) : rsph := ⟦p⟧

noncomputable instance rsph.topological_space : topological_space rsph := @quot.topological_space _ _ pr_sph.topological_space

private lemma mk_preimg (x: set pr_sph): mk⁻¹' (mk '' x) = x∪ sum.inr '' (field.inv '' ((sum.inl⁻¹' x)\{0}))∪ sum.inl '' (field.inv '' ((sum.inr⁻¹' x)\{0})) :=
begin
  change quotient.mk ⁻¹' (quotient.mk '' x) = x ∪ sum.inr '' (field.inv '' ((sum.inl ⁻¹' x) \ {0})) ∪ sum.inl '' (field.inv '' ((sum.inr ⁻¹' x) \ {0})),
  simp only [set.image, set.preimage, set.mem_set_of_eq],
  ext,
  simp only [quotient.eq, set.mem_set_of_eq, forall_exists_index, and_imp],
  simp only [set.mem_diff, set.mem_set_of_eq, set.mem_singleton_iff, set.mem_union_eq],
  split,
  intro h,
  cases h with a h,
  cases h with h1 h2,
  change eqv a x_1 at h2,
  rw eqv at h2,
  cases h2 with h21 h22,
  left,
  finish,
  cases h22 with z h22,
  cases h22 with w h22,
  cases_type* and or,
  right,
  use w,
  split,
  use z,
  have t: z≠0,
  intro h,
  revert h22_right_right,
  rw h,
  finish,
  split,
  finish,
  change z⁻¹=w,
  apply_fun (λ x,z⁻¹*x) at h22_right_right,
  field_simp at h22_right_right,
  field_simp,
  rw <- h22_right_right,
  exact mul_comm z w,
  exact eq.symm h22_right_left,
  left,
  right,
  use w,
  split,
  use z,
  have t: z≠0,
  intro h,
  revert h22_right_right,
  rw h,
  finish,
  split,
  finish,
  change z⁻¹=w,
  apply_fun (λ x,z⁻¹*x) at h22_right_right,
  field_simp at h22_right_right,
  field_simp,
  rw <- h22_right_right,
  exact mul_comm z w,
  exact eq.symm h22_right_left,
  intro h,
  cases h,
  cases h,
  use x_1,
  finish,
  cases h with a h,
  cases h with h1 h2,
  cases h1 with w h1,
  cases h1 with h11 h12,
  change ∃ (a : pr_sph), a ∈ x ∧ eqv a x_1,
  use sum.inl w,
  rw eqv,
  cases h11 with h111 h112,
  split,
  exact h111,
  right,
  use w,
  use a,
  simp only [true_and, false_or, eq_self_iff_true, false_and],
  split,
  exact eq.symm h2,
  change w⁻¹=a at h12,
  rw <- h12,
  field_simp,
  change ∃ (a : pr_sph), a ∈ x ∧ eqv a x_1,
  cases h with a h,
  cases h with h1 h2,
  cases h1 with a_1 h1,
  cases h1 with h11 h12,
  use sum.inr a_1,
  split,
  cases h11 with h111 h112,
  exact h111,
  rw eqv,
  right,
  use a_1,
  use a,
  left,
  split,
  refl,
  split,
  exact eq.symm h2,
  cases h11 with h111 h112,
  change a_1⁻¹=a at h12,
  rw <- h12,
  field_simp,
end

lemma is_open_mk : is_open_map mk :=
begin
  rw is_open_map,
  intro x,
  intro h,
  rw is_open_coinduced,
  change is_open (mk ⁻¹' (mk '' x)),
  rw mk_preimg,
  apply is_open.union,
  apply is_open.union,
  exact h,
  apply open_embedding.is_open_map open_embedding_inr,
  rw is_open_iff_nhds,
  intros a g,
  have t:a≠0,
    simp at g,
    cases g with x_1 g,
    cases g with g1 g2,
    cases g1 with g11 g12,
    rw <- g2,
    apply_fun field.inv,
    change x_1⁻¹⁻¹≠0⁻¹,
    field_simp,
    exact g12,
  simp only [filter.le_principal_iff],
  have tt:=continuous_at_inv₀,
  specialize tt t,
  change continuous_at field.inv a at tt,
  swap,
  exact normed_division_ring.to_has_continuous_inv₀,
  rw continuous_at_def at tt,
  have ttt: ∀ x:set ℂ, field.inv⁻¹' x=field.inv '' x,
  intro x,
  rw set.image,
  rw set.preimage,
  ext,
  simp,
  split,
  intro h,
  use field.inv x_1,
  split,
  exact h,
  change x_1⁻¹⁻¹=x_1,
  field_simp,
  intro h,
  cases h with a h,
  cases h with h1 h2,
  apply_fun field.inv at h2,
  change a⁻¹⁻¹=x_1⁻¹ at h2,
  rw inv_inv at h2,
  change x_1⁻¹∈ x,
  rw <- h2,
  exact h1,
  rw <- ttt,
  apply tt,
  rw mem_nhds_iff,
  use sum.inl ⁻¹' x \ {0},
  split,
  exact rfl.subset,
  split,
  refine is_open.sdiff _ _,
  apply continuous_inl.is_open_preimage x,
  exact h,
  exact t1_space.t1 0,
  rw <- set.mem_preimage,
  rw ttt,
  exact g,
  
  apply open_embedding.is_open_map open_embedding_inl,
  rw is_open_iff_nhds,
  intros a g,
  have t:a≠0,
    simp at g,
    cases g with x_1 g,
    cases g with g1 g2,
    cases g1 with g11 g12,
    rw <- g2,
    apply_fun field.inv,
    change x_1⁻¹⁻¹≠0⁻¹,
    field_simp,
    exact g12,
  simp only [filter.le_principal_iff],
  have tt:=continuous_at_inv₀,
  specialize tt t,
  change continuous_at field.inv a at tt,
  swap,
  exact normed_division_ring.to_has_continuous_inv₀,
  rw continuous_at_def at tt,
  have ttt: ∀ x:set ℂ, field.inv⁻¹' x=field.inv '' x,
  intro x,
  rw set.image,
  rw set.preimage,
  ext,
  simp,
  split,
  intro h,
  use field.inv x_1,
  split,
  exact h,
  change x_1⁻¹⁻¹=x_1,
  field_simp,
  intro h,
  cases h with a h,
  cases h with h1 h2,
  apply_fun field.inv at h2,
  change a⁻¹⁻¹=x_1⁻¹ at h2,
  rw inv_inv at h2,
  change x_1⁻¹∈ x,
  rw <- h2,
  exact h1,
  rw <- ttt,
  apply tt,
  rw mem_nhds_iff,
  use sum.inr ⁻¹' x \ {0},
  split,
  exact rfl.subset,
  split,
  refine is_open.sdiff _ _,
  apply continuous_inr.is_open_preimage x,
  exact h,
  exact t1_space.t1 0,
  rw <- set.mem_preimage,
  rw ttt,
  exact g,
end

namespace charts

def pr_c_chart_l: set pr_sph := set.range sum.inl
def c_chart_l := set.image mk pr_c_chart_l
lemma pr_c_chart_l_is_open: pr_sph.topological_space.is_open pr_c_chart_l:= open_embedding_inl.open_range
lemma c_chart_l_is_open: is_open c_chart_l := is_open_mk pr_c_chart_l pr_c_chart_l_is_open
def pr_inv:pr_sph→ pr_sph:=@sum.rec ℂ ℂ (λ_, pr_sph) sum.inr sum.inl


@[continuity]
private lemma pr_inv.is_continuous: continuous pr_inv :=
begin
apply continuous_sum_rec,
continuity,
end

private lemma pr_inv_desc : (∀ z w:pr_sph,eqv z w→eqv (pr_inv z) (pr_inv w)) :=
begin
intros z w h,
rw eqv at *,
cases h,
rw h,
finish,
rw pr_inv,
right,
cases_type* and or Exists,
rw h_h_h_left,
rw h_h_h_right_left,
simp only [false_and, false_or, exists_and_distrib_left],
use h_w,
split,
refl,
use h_h_w,
finish,
rw h_h_h_left,
rw h_h_h_right_left,
simp only [false_and, or_false, exists_and_distrib_left],
use h_w,
use h_h_w,
finish,
end

def inv: rsph→ rsph := quot.lift (mk∘ pr_inv) begin
change ∀ (a b : pr_sph), setoid.r a b → ⟦pr_inv a⟧ = ⟦pr_inv b⟧,
simp only [quotient.eq],
exact pr_inv_desc,
end

@[continuity]
lemma inv.is_continuous: continuous inv := begin
rw inv,
continuity,
change continuous quotient.mk,
exact continuous_quotient_mk
end

@[continuity]
private noncomputable def inv.homeomorph := Top.homeo_of_iso ({
hom:= {to_fun:=inv},
inv:= {to_fun:=inv},
} : category_theory.iso (Top.of rsph) (Top.of rsph))

def c_chart_r := set.image inv c_chart_l

def chart_map_l := mk ∘ sum.inl
def chart_map_r := inv∘mk ∘ sum.inl

def chart_map_l_open_embedding: open_embedding chart_map_l := ⟨⟨begin
rw chart_map_l,
change inducing (quotient.mk∘sum.inl),
fconstructor,
ext,
split,
intro h,
change is_open x at h,
rw is_open_induced_iff',
use set.image (quotient.mk∘sum.inl) x,
split,
rw set.image_comp,
apply is_open_mk,
apply open_embedding_inl.is_open_map x,
exact h,
rw set.preimage_image_eq,
rw function.injective,
intros a b g,
simp only [quotient.eq] at g,
change eqv (sum.inl a) (sum.inl b) at g,
rw eqv at g,
cases g,
injection g,
cases g with z g,
cases g with w g,
cases g,
finish,
finish,
intro h,
change is_open x,
rw is_open_induced_iff' at h,
cases h with t h,
cases h with h1 h2,
rw <-h2,
rw set.preimage_comp,
apply continuous_inl.is_open_preimage (quotient.mk ⁻¹' t),
exact is_open_coinduced.mp h1,
end,

begin
rw chart_map_l,
rw function.injective,
intros z w,
simp only [function.comp_app],
change quotient.mk (sum.inl z) = quotient.mk (sum.inl w) → z = w,
rw quotient.eq,
change eqv (sum.inl z) (sum.inl w) → z = w,
rw eqv,
finish
end⟩,begin
rw chart_map_l,
rw set.range_comp,
apply is_open_mk,
exact is_open_range_inl,
end⟩

def chart_map_r_open_embedding: open_embedding chart_map_r := begin
rw chart_map_r,
apply open_embedding.comp,
exact homeomorph.open_embedding inv.homeomorph,
exact chart_map_l_open_embedding,
end

def range_l:= set.range (mk∘(sum.inl:ℂ→ pr_sph))
def range_r:= set.range (mk∘(sum.inr:ℂ→ pr_sph))

def range_l.open: is_open range_l :=
begin
rw range_l,
apply is_open_map.is_open_range,
apply is_open_map.comp,
exact is_open_mk,
exact open_embedding_inl.is_open_map,
end

def range_r.open: is_open range_r :=
begin
rw range_r,
apply is_open_map.is_open_range,
apply is_open_map.comp,
exact is_open_mk,
exact open_embedding_inr.is_open_map,
end

noncomputable def local_homeo_l :=local_homeomorph.restr (charts.chart_map_l_open_embedding.to_local_homeomorph charts.chart_map_l).symm range_l

noncomputable def local_homeo_r :=local_homeomorph.restr (charts.chart_map_r_open_embedding.to_local_homeomorph charts.chart_map_r).symm range_r
end charts

noncomputable instance rsph_compl_manif: charted_space ℂ rsph := { atlas:= {charts.local_homeo_l, charts.local_homeo_r},
chart_at:=λ z, if z=mk (sum.inr 0) then charts.local_homeo_r else charts.local_homeo_l,
mem_chart_source:=begin
intro x,
split_ifs,
rw charts.local_homeo_r,
simp only [local_homeomorph.symm_to_local_equiv, local_equiv.symm_source, open_embedding.to_local_homeomorph_target,
  set.mem_range, ne.def, local_homeomorph.restr_to_local_equiv, local_equiv.restr_source, set.mem_inter_eq],
use 0,
finish,
rw h,
rw interior_eq_iff_open.mpr charts.range_r.open,
simp only [charts.range_r, set.mem_range, exists_apply_eq_apply],
rw charts.local_homeo_l,
have hx:x ∈ interior charts.range_l,
{rw interior_eq_iff_open.mpr charts.range_l.open,
  simp [charts.range_l,mk],
  have t:= quot.exists_rep x,
  cases t with a t,
  cases a,
  use a,
  rw <- t,
  finish,
  use a⁻¹,
  rw <- t,
  change _ = mk _,
  simp only [mk, quotient.eq],
  change eqv _ _,
  rw eqv,
  right,
  use a⁻¹,
  use a,
  simp only [false_and, eq_self_iff_true, true_and, false_or],
  have tt:a≠0,
  {
  intro k,
  revert h,
  rw <-t,
  rw k,
  finish,
  },
  field_simp,
},
simp only [local_homeomorph.symm_to_local_equiv, local_equiv.symm_source, open_embedding.to_local_homeomorph_target,
  set.mem_range, local_homeomorph.restr_to_local_equiv, local_equiv.restr_source, set.mem_inter_eq],
have g:=quotient.exists_rep x,
cases g with a g,
cases a,
use a,
finish,
exact hx,
use a⁻¹,
simp [charts.chart_map_l,mk],
rw <- g,
rw quotient.eq,
change eqv (sum.inl a⁻¹) (sum.inr a),
rw eqv,
right,
use a⁻¹,
use a,
right,
split,
refl,
split,
refl,
have t:a≠ 0,
finish,
finish,
exact hx,
end,

chart_mem_atlas:=begin
finish,
end,
}

instance rsph_rsurf: rsurf rsph :=
begin
have M: cont_diff_on ℂ ⊤ (λ z:ℂ,z⁻¹) {z:ℂ|z≠ 0},
{
  exact cont_diff_on_inv ℂ,
},
rw rsurf,
apply smooth_manifold_with_corners_of_cont_diff_on,
assume a b ha hb,
simp only [atlas, set.mem_insert_iff, set.mem_singleton_iff] at ha hb,
rcases ha with rfl | rfl; rcases hb with rfl | rfl,
{
  exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_cont_diff_groupoid _ _ _)).1
},
{
  apply M.congr_mono _ _,
  rintro _ ⟨⟨h1,⟨y,h2⟩⟩,g⟩,
  apply eq.symm,
  simp only [charts.local_homeo_r] with mfld_simps,
  rw local_homeomorph.eq_symm_apply,
  all_goals{simp only [charts.local_homeo_r, charts.local_homeo_l, charts.chart_map_l, charts.chart_map_r, mk, charts.inv, ne.def, set.mem_range] with mfld_simps at *},
  change (mk ∘ charts.pr_inv) _ = _,
  simp only [charts.pr_inv, mk, function.comp_app, quotient.eq],
  change eqv _ _,
  rw eqv,
  right,
  use x⁻¹,
  use x,
  left,
  split,
  refl,
  split,
  refl,
  rw interior_eq_iff_open.mpr charts.range_r.open at h2,
  simp only [charts.range_r, mk, set.mem_range, function.comp_app, quotient.eq] at h2,
  change ∃ y, eqv _ _ at h2,
  simp only [eqv, false_and, or_false, exists_and_distrib_left, false_or] at h2,
  have t:x≠0,
  intro t,
  rcases h2 with ⟨y,⟨z,h21,⟨w,h221,h222⟩⟩⟩,
  injection h221,
  revert h222,
  rw <- h_1,
  rw t,
  simp only [mul_zero, zero_ne_one, forall_false_left],
  field_simp,
  exact y,
  simp only [charts.range_r],
  rw set.subset_def,
  intro x,
  simp [mk],
  rw interior_eq_iff_open.mpr charts.range_l.open,
  intros h y g,
  change mk _ = _ at g,
  simp [mk,charts.pr_inv] at g,
  intros _ hx,
  change eqv _ _ at g,
  revert g,
  rw hx,
  simp only [eqv, false_and, or_false, exists_and_distrib_left, false_or, forall_exists_index, and_imp],
  intros x1 hx1 x2 hx2,
  injection hx2 with hx2,
  rw <- hx2,
  field_simp,
},
{
  apply M.congr_mono _ _,
  rintro _ ⟨⟨h1,⟨h21,h22⟩⟩,g⟩,
  apply eq.symm,
  simp only [charts.local_homeo_l] with mfld_simps,
  rw local_homeomorph.eq_symm_apply,
  all_goals{simp only [charts.local_homeo_r, charts.local_homeo_l, charts.chart_map_l, charts.chart_map_r, mk, charts.inv, ne.def, set.mem_range] with mfld_simps at *},

  have t:x≠0, {
  intro t,
  rcases h21 with ⟨y,h21⟩,
  change _ = mk _ at h21,
  simp only [charts.pr_inv, mk, quotient.eq] at h21,
  revert h21,
  change eqv _ _→ false,
  rw t,
  simp only [eqv, false_and, false_or, exists_and_distrib_left, forall_exists_index, and_imp],
  intros z1 g1 z2 g2,
  injection g2,
  rw <- h_1,
  field_simp,
  },
  change _ = mk _,
  simp only [charts.pr_inv, mk, function.comp_app, quotient.eq],
  change eqv _ _,
  rw eqv,
  right,
  use x⁻¹,
  use x,
  right,
  split,
  refl,
  split,
  refl,
  field_simp,
  exact h21,

  simp only [charts.range_r],
  rw set.subset_def,
  intro x,
  simp [mk],
  rw interior_eq_iff_open.mpr charts.range_l.open,
  intros h y g,
  change _ = mk _ at g,
  simp [mk,charts.pr_inv] at g,
  intros _ hx,
  change eqv _ _ at g,
  revert g,
  rw hx,
  simp only [eqv, false_and, or_false, exists_and_distrib_left, false_or, forall_exists_index, and_imp],
  intros x1 hx1 x2 hx2,
  injection hx2 with hx2,
  rw <- hx2,
  field_simp,
},
{
  exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_cont_diff_groupoid _ _ _)).1
},
end
end rsph

end riemann_surfaces