ring_stuff.lean

import algebra.ring group_theory.submonoid ring_theory.ideals linear_algebra.basic
import tactic.ring

namespace localization_alt

universes u v w
variables {A : Type u} {B : Type v} {C : Type w} 
variables [comm_ring A] [comm_ring B] [comm_ring C]
variables (S : set A) [is_submonoid S] (f : A → B) [is_ring_hom f]

/- This is essentially the same logic as units.ext, but in more 
   convenient form.
-/
lemma comm_monoid.inv_unique {M : Type*} [comm_monoid M] 
 {a ai₁ ai₂ : M} (e₁ : a * ai₁ = 1) (e₂ : a * ai₂ = 1) : ai₁ = ai₂ := 
calc 
  ai₁ = ai₁ * 1 : (mul_one ai₁).symm
  ... = (ai₁ * a) * ai₂ : by rw[← e₂,mul_assoc]
  ... = ai₂ : by rw[mul_comm ai₁ a,e₁,one_mul]


def ker : ideal A := 
{
  carrier := λ a, f a = 0,
  zero := is_ring_hom.map_zero f,
  add := begin
   intros a1 a2 fa1z fa2z, 
   change f a1 = 0 at fa1z,
   change f a2 = 0 at fa2z,
   show f (a1 + a2) = 0,
   simp[is_ring_hom.map_add f,fa1z,fa2z]
  end,
  smul := begin
   intros a1 a2 fa2z,
   change f a2 = 0 at fa2z,
   show f (a1 * a2) = 0,
   simp[is_ring_hom.map_mul f,fa2z],
  end
}

def inverts_data (S : set A) (f : A → B) : Type* := 
 ∀ s : S, {si : B // (f s) * si = 1}

def inverts (S : set A) (f : A → B) : Prop := 
 ∀ s : S, ∃ si : B, (f s) * si = 1

lemma inverts_subsingleton (S : set A) (f : A → B) :
 subsingleton (inverts_data S f) := 
begin
 constructor,
 intros fi1 fi2,
 funext s,
 rcases (fi1 s) with ⟨si1,e1⟩,
 rcases (fi2 s) with ⟨si2,e2⟩,
 apply subtype.eq,
 exact comm_monoid.inv_unique e1 e2,
end

def inverts_of_data (h : inverts_data S f) : inverts S f := 
 λ s, ⟨(h s).1,(h s).2⟩

noncomputable def inverts_some (h : inverts S f) : inverts_data S f := 
 λ s, ⟨classical.some (h s),classical.some_spec (h s)⟩

def has_denom_data (S : set A) (f : A → B) := 
 ∀ b : B, {sa : S × A // (f sa.1) * b = f sa.2 }

def has_denom (S : set A) (f : A → B) : Prop := 
 ∀ b : B, ∃ (sa : S × A), (f sa.1) * b = (f sa.2)

def has_denom_of_data (h : has_denom_data S f) : has_denom S f :=
 λ b, ⟨(h b).1,(h b).2⟩

noncomputable def has_denom_some (h : has_denom S f) : has_denom_data S f := 
 λ b, ⟨classical.some (h b),classical.some_spec (h b)⟩

def ann_aux (S : set A) [is_submonoid S] : Type* := 
 { as : A × S // as.1 * as.2 = 0 }

namespace ann_aux

def zero : ann_aux S := ⟨⟨0,1⟩,by simp⟩ 

def add (as bt : ann_aux S) : ann_aux S := begin
 rcases as with ⟨⟨a,s⟩,asz0⟩,
 rcases bt with ⟨⟨b,t⟩,btz0⟩,
 have h : (a + b) * (s * t) = 0 := calc
  (a + b) * (s * t) = (a * s) * t + (b * t) * s : by ring
  ... = 0 : by rw[asz0,btz0,zero_mul,zero_mul,zero_add],
 exact ⟨⟨a + b,s * t⟩,h⟩,
end

def smul (a : A) (bt : ann_aux S) : ann_aux S := begin
 rcases bt with ⟨⟨b,t⟩,eb0⟩,
 have eab : (a * b) * t = 0 := 
  ((mul_assoc a b t).trans (congr_arg (λ x, a * x) eb0)).trans (mul_zero a),
 exact ⟨⟨a * b,t⟩,eab⟩,
end

end ann_aux

def submonoid_ann (S : set A) [is_submonoid S] : ideal A := 
{ carrier := λ a, ∃ as : ann_aux S, as.1.1 = a,
  zero := ⟨ann_aux.zero S,rfl⟩,
  add := λ _ _ ⟨⟨⟨a,s⟩,ea0⟩,rfl⟩ ⟨⟨⟨b,t⟩,eb0⟩,rfl⟩, ⟨ann_aux.add S ⟨⟨a,s⟩,ea0⟩ ⟨⟨b,t⟩,eb0⟩,rfl⟩,
  smul := λ a _ ⟨⟨⟨b,t⟩,eb0⟩,rfl⟩, ⟨ann_aux.smul S a ⟨⟨b,t⟩,eb0⟩,begin rw ann_aux.smul,refl,end⟩
}

lemma inverts_ker (hf : inverts S f) : submonoid_ann S ≤ ker f := 
begin
 apply submodule.le_def'.mpr,
 rintros _ ⟨⟨⟨a,s⟩,asz⟩,rfl⟩,
 simp at asz ⊢,
 rcases (hf s) with ⟨si,e1⟩,
 show f a = 0,
 exact calc
  f a = (f a) * 1 : (mul_one (f a)).symm
  ... = (f a) * ((f s) * si) : by rw[← e1] 
  ... = ((f a) * (f s)) * si : by rw[mul_assoc]
  ... = 0 : by rw[← is_ring_hom.map_mul f,asz,is_ring_hom.map_zero f,zero_mul],
end

structure is_localization_data := 
 (inverts : inverts_data S f)
 (has_denom : has_denom_data S f)
 (ker_eq : ker f = submonoid_ann S) 

def is_localization : Prop := 
 (inverts S f) ∧ (has_denom S f) ∧ (ker f = submonoid_ann S) 

lemma localization_epi (hf : is_localization S f)
 (g₁ g₂ : B → C) [is_ring_hom g₁] [is_ring_hom g₂] 
  (e : g₁ ∘ f = g₂ ∘ f) : g₁ = g₂ := 
begin
 have e' : ∀ x, g₁ (f x) = g₂ (f x) := 
  λ x, @congr_fun _ _ (g₁ ∘ f) (g₂ ∘ f) e x,
 ext b,
 rcases hf.2.1 b with ⟨⟨s,a⟩,e1⟩,
 rcases hf.1 s with ⟨si,e2⟩,
 have e3 : b = (f a) * si := calc
  b = 1 * b : (one_mul b).symm
  ... = ((f s) * si) * b : by rw[← e2]
  ... = (f a) * si : by rw[mul_assoc (f s) si b,mul_comm si b,← mul_assoc,e1],
 have e4 : g₁ (f s) * (g₁ si) = 1 :=
  by simp[(is_ring_hom.map_mul g₁).symm,e2,(is_ring_hom.map_one g₁)],
 have e5 : g₁ (f s) * (g₂ si) = 1 :=
  by simp[(e' s),(is_ring_hom.map_mul g₂).symm,e2,(is_ring_hom.map_one g₂)],
 have e6 : g₁ si = g₂ si := comm_monoid.inv_unique e4 e5,
 exact calc
  g₁ b = g₁ (f a) * g₁ si : by rw[e3,is_ring_hom.map_mul g₁]
  ... = g₂ (f a) * g₂ si : by rw[e' a,e6]
  ... = g₂ b : by rw[← is_ring_hom.map_mul g₂,← e3],
end

section localization_initial 
variables (hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g) 

def is_localization_initial
 (hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g) 
 : B → C := λ b, g (hf.has_denom b).1.2 * (hg (hf.has_denom b).1.1).1

lemma useful (hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g) :
∀ a₁ a₂ : A, f a₁ = f a₂ → g a₁ = g a₂ := sorry -- proof is embedded in map_one below
 
instance (hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g) :
 is_ring_hom (is_localization_initial S f hf g hg) := 
{ map_one := begin 
    unfold is_localization_initial,
    rcases (hf.has_denom 1) with ⟨⟨s,a⟩,h⟩,
    show g a * (hg s).val = 1,
    change f s * 1 = f a at h,
    rw mul_one at h,
    have h2 := (hg s).property,
    have h3 : a - s ∈ ker f,
      show f (a - s) = 0,
      rw is_ring_hom.map_sub f,
      rw h,
      rw sub_self,
    suffices : g a = g s,
      rw this; exact h2,
    -- know f s = f a, want g s = g a
    -- this should be a lemma
    have h4 := hf.ker_eq,
    rw h4 at h3,
    cases h3 with t Ht,
    rcases t with ⟨⟨b,t⟩,h5⟩,
    change b = a - s at Ht,
    change b * t = 0 at h5,
    rw Ht at h5,
    rw sub_mul at h5,
    rw sub_eq_zero at h5,
    have h6 : g (a * t) = g (s * t),
      rw h5,
    rw is_ring_hom.map_mul g at h6,
    rw is_ring_hom.map_mul g at h6,
    rcases hg t with ⟨u,hu⟩,
    calc g a = g a * 1 : by rw mul_one
    ...      = g a * (g t * u) : by rw hu
    ...      = (g a * g t) * u : by rw mul_assoc
    ...      = (g s * g t) * u : by rw h6
    ...      = g s * (g t * u) : by rw mul_assoc
    ... = g s : by rw [hu,mul_one]
  end,
  map_add := begin
    intros x y,
    unfold is_localization_initial,
    rcases (hf.has_denom (x + y)) with ⟨⟨s3,a3⟩,h3⟩,
    change f s3 * (x + y) = f a3 at h3,
    rcases (hf.has_denom x) with ⟨⟨s1,a1⟩,h1⟩,
    change f s1 * x = f a1 at h1,
    rcases (hf.has_denom y) with ⟨⟨s2,a2⟩,h2⟩,
    change f s2 * y = f a2 at h2,
    show g a3 * (hg s3).val = g a1 * (hg s1).val + g a2 * (hg s2).val,
    rcases (hg s3) with ⟨t3,H3⟩,
    rcases (hg s1) with ⟨t1,H1⟩,
    rcases (hg s2) with ⟨t2,H2⟩,
    show g a3 * t3 = g a1 * t1 + g a2 * t2,
    /-
    h3 : f ↑s3 * (x + y) = f a3,
s1 : ↥S,
a1 : A,
h1 : f ↑s1 * x = f a1,
s2 : ↥S,
a2 : A,
h2 : f ↑s2 * y = f a2,
t3 : C,
H3 : g ↑s3 * t3 = 1,
t1 : C,
H1 : g ↑s1 * t1 = 1,
t2 : C,
H2 : g ↑s2 * t2 = 1

⊢ g a3 * t3 = g a1 * t1 + g a2 * t2

Idea now is to cancel the t's by multiplying by g s1 g s2 g s3, which is a unit because of
inverts_data g. Then our goal is

g(a3 s1 s2) = g(a1 s2 s3) + g(s1 a2 s3)
and hence our goal is g(a3 s1 s2 - a1 s2 s3 - s1 a2 s3) = 0.
But deom f(s1 x) = f (a1) etc I can deduce that
a3s2s1 - s3a2s1 - s3s2a1 is in ker(f)
so by the lemma f(z)=0 -> g(z)=0 we're done.

    -/

    sorry
  end,
  map_mul := begin
    intros x y,
    unfold is_localization_initial,
    rcases (hf.has_denom (x * y)) with ⟨⟨s3,a3⟩,h3⟩,
    change f s3 * (x * y) = f a3 at h3,
    rcases (hf.has_denom x) with ⟨⟨s1,a1⟩,h1⟩,
    change f s1 * x = f a1 at h1,
    rcases (hf.has_denom y) with ⟨⟨s2,a2⟩,h2⟩,
    change f s2 * y = f a2 at h2,
    show g a3 * (hg s3).val = g a1 * (hg s1).val * (g a2 * (hg s2).val),
    rcases (hg s3) with ⟨t3,H3⟩,
    rcases (hg s1) with ⟨t1,H1⟩,
    rcases (hg s2) with ⟨t2,H2⟩,
    show g a3 * t3 = g a1 * t1 * (g a2 * t2),
    sorry
  end
}

lemma is_localization_initial_comp 
 (hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g) :
  ∀ a : A, (is_localization_initial S f hf g hg (f a) = g a) := begin
  intro a,
  unfold is_localization_initial,
  rcases (hf.has_denom (f a)) with ⟨⟨s1,a1⟩,h1⟩,
  change f s1 * f a = f a1 at h1,
  show g a1 * (hg s1).val = g a,
  rcases (hg s1) with ⟨t1,H1⟩,
  show g a1 * t1 = g a,
  sorry,
end

end localization_initial

end localization_alt