text:
/-
Copyright (c) 2021 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import algebra.lie.ideal_operations
import algebra.lie.abelian
import order.preorder_hom

/-!
# Solvable Lie algebras

Like groups, Lie algebras admit a natural concept of solvability. We define this here via the
derived series and prove some related results. We also define the radical of a Lie algebra and
prove that it is solvable when the Lie algebra is Noetherian.

## Main definitions

  * `lie_algebra.derived_series_of_ideal`
  * `lie_algebra.derived_series`
  * `lie_algebra.is_solvable`
  * `lie_algebra.is_solvable_add`
  * `lie_algebra.radical`
  * `lie_algebra.radical_is_solvable`
  * `lie_algebra.derived_length_of_ideal`
  * `lie_algebra.derived_length`
  * `lie_algebra.derived_abelian_of_ideal`

## Tags

lie algebra, derived series, derived length, solvable, radical
-/

universes u v w w₁ w₂

variables (R : Type u) (L : Type v) (M : Type w) {L' : Type w₁}
variables [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L']
variables (I J : lie_ideal R L) {f : L' →ₗ⁅R⁆ L}

namespace lie_algebra

/-- A generalisation of the derived series of a Lie algebra, whose zeroth term is a specified ideal.

It can be more convenient to work with this generalisation when considering the derived series of
an ideal since it provides a type-theoretic expression of the fact that the terms of the ideal's
derived series are also ideals of the enclosing algebra.

See also `lie_ideal.derived_series_eq_derived_series_of_ideal_comap` and
`lie_ideal.derived_series_eq_derived_series_of_ideal_map` below. -/
def derived_series_of_ideal (k : ℕ) : lie_ideal R L → lie_ideal R L := (λ I, ⁅I, I⁆)^[k]

@[simp] lemma derived_series_of_ideal_zero :
  derived_series_of_ideal R L 0 I = I := rfl

@[simp] lemma derived_series_of_ideal_succ (k : ℕ) :
  derived_series_of_ideal R L (k + 1) I =
  ⁅derived_series_of_ideal R L k I, derived_series_of_ideal R L k I⁆ :=
function.iterate_succ_apply' (λ I, ⁅I, I⁆) k I

/-- The derived series of Lie ideals of a Lie algebra. -/
abbreviation derived_series (k : ℕ) : lie_ideal R L := derived_series_of_ideal R L k ⊤

lemma derived_series_def (k : ℕ) :
  derived_series R L k = derived_series_of_ideal R L k ⊤ := rfl

variables {R L}

local notation `D` := derived_series_of_ideal R L

lemma derived_series_of_ideal_add (k l : ℕ) : D (k + l) I = D k (D l I) :=
begin
  induction k with k ih,
  { rw [zero_add, derived_series_of_ideal_zero], },
  { rw [nat.succ_add k l, derived_series_of_ideal_succ, derived_series_of_ideal_succ, ih], },
end

lemma derived_series_of_ideal_le {I J : lie_ideal R L} {k l : ℕ} (h₁ : I ≤ J) (h₂ : l ≤ k) :
  D k I ≤ D l J :=
begin
  revert l, induction k with k ih; intros l h₂,
  { rw nat.le_zero_iff at h₂, rw [h₂, derived_series_of_ideal_zero], exact h₁, },
  { have h : l = k.succ ∨ l ≤ k, by rwa [le_iff_eq_or_lt, nat.lt_succ_iff] at h₂,
    cases h,
    { rw [h, derived_series_of_ideal_succ, derived_series_of_ideal_succ],
      exact lie_submodule.mono_lie _ _ _ _ (ih (le_refl k)) (ih (le_refl k)), },
    { rw derived_series_of_ideal_succ, exact le_trans (lie_submodule.lie_le_left _ _) (ih h), }, },
end

lemma derived_series_of_ideal_succ_le (k : ℕ) : D (k + 1) I ≤ D k I :=
derived_series_of_ideal_le (le_refl I) k.le_succ

lemma derived_series_of_ideal_le_self (k : ℕ) : D k I ≤ I :=
derived_series_of_ideal_le (le_refl I) (zero_le k)

lemma derived_series_of_ideal_mono {I J : lie_ideal R L} (h : I ≤ J) (k : ℕ) : D k I ≤ D k J :=
derived_series_of_ideal_le h (le_refl k)

lemma derived_series_of_ideal_antimono {k l : ℕ} (h : l ≤ k) : D k I ≤ D l I :=
derived_series_of_ideal_le (le_refl I) h

lemma derived_series_of_ideal_add_le_add (J : lie_ideal R L) (k l : ℕ) :
  D (k + l) (I + J) ≤ (D k I) + (D l J) :=
begin
  let D₁ : lie_ideal R L →ₘ lie_ideal R L :=
  { to_fun    := λ I, ⁅I, I⁆,
    monotone' := λ I J h, lie_submodule.mono_lie I J I J h h, },
  have h₁ : ∀ (I J : lie_ideal R L), D₁ (I ⊔ J) ≤ (D₁ I) ⊔ J,
  { simp [lie_submodule.lie_le_right, lie_submodule.lie_le_left, le_sup_right_of_le], },
  rw ← D₁.iterate_sup_le_sup_iff at h₁,
  exact h₁ k l I J,
end

lemma derived_series_of_bot_eq_bot (k : ℕ) : derived_series_of_ideal R L k ⊥ = ⊥ :=
by { rw eq_bot_iff, exact derived_series_of_ideal_le_self ⊥ k, }

lemma abelian_iff_derived_one_eq_bot : is_lie_abelian I ↔ derived_series_of_ideal R L 1 I = ⊥ :=
by rw [derived_series_of_ideal_succ, derived_series_of_ideal_zero,
  lie_submodule.lie_abelian_iff_lie_self_eq_bot]

lemma abelian_iff_derived_succ_eq_bot (I : lie_ideal R L) (k : ℕ) :
  is_lie_abelian (derived_series_of_ideal R L k I) ↔ derived_series_of_ideal R L (k + 1) I = ⊥ :=
by rw [add_comm, derived_series_of_ideal_add I 1 k, abelian_iff_derived_one_eq_bot]

end lie_algebra

namespace lie_ideal

open lie_algebra

variables {R L}

lemma derived_series_eq_derived_series_of_ideal_comap (k : ℕ) :
  derived_series R I k = (derived_series_of_ideal R L k I).comap I.incl :=
begin
  induction k with k ih,
  { simp only [derived_series_def, comap_incl_self, derived_series_of_ideal_zero], },
  { simp only [derived_series_def, derived_series_of_ideal_succ] at ⊢ ih, rw ih,
    exact comap_bracket_incl_of_le I
      (derived_series_of_ideal_le_self I k) (derived_series_of_ideal_le_self I k), },
end

lemma derived_series_eq_derived_series_of_ideal_map (k : ℕ) :
  (derived_series R I k).map I.incl = derived_series_of_ideal R L k I :=
by { rw [derived_series_eq_derived_series_of_ideal_comap, map_comap_incl, inf_eq_right],
     apply derived_series_of_ideal_le_self, }

lemma derived_series_eq_bot_iff (k : ℕ) :
  derived_series R I k = ⊥ ↔ derived_series_of_ideal R L k I = ⊥ :=
by rw [← derived_series_eq_derived_series_of_ideal_map, map_eq_bot_iff, ker_incl, eq_bot_iff]

lemma derived_series_add_eq_bot {k l : ℕ} {I J : lie_ideal R L}
  (hI : derived_series R I k = ⊥) (hJ : derived_series R J l = ⊥) :
  derived_series R ↥(I + J) (k + l) = ⊥ :=
begin
  rw lie_ideal.derived_series_eq_bot_iff at hI hJ ⊢,
  rw ← le_bot_iff,
  let D := derived_series_of_ideal R L, change D k I = ⊥ at hI, change D l J = ⊥ at hJ,
  calc D (k + l) (I + J) ≤ (D k I) + (D l J) : derived_series_of_ideal_add_le_add I J k l
                     ... ≤ ⊥ : by { rw [hI, hJ], simp, },
end

lemma derived_series_map_le (k : ℕ) :
  (derived_series R L' k).map f ≤ derived_series R L k :=
begin
  induction k with k ih,
  { simp only [derived_series_def, derived_series_of_ideal_zero, le_top], },
  { simp only [derived_series_def, derived_series_of_ideal_succ] at ih ⊢,
    exact le_trans (map_bracket_le f) (lie_submodule.mono_lie _ _ _ _ ih ih), },
end

lemma derived_series_map_eq (k : ℕ) (h : function.surjective f) :
  (derived_series R L' k).map f = derived_series R L k :=
begin
  induction k with k ih,
  { change (⊤ : lie_ideal R L').map f = ⊤,
    rw ←f.ideal_range_eq_map,
    exact f.ideal_range_eq_top_of_surjective h, },
  { simp only [derived_series_def, map_bracket_eq f h, ih, derived_series_of_ideal_succ], },
end

end lie_ideal

namespace lie_algebra

/-- A Lie algebra is solvable if its derived series reaches 0 (in a finite number of steps). -/
class is_solvable : Prop :=
(solvable : ∃ k, derived_series R L k = ⊥)

instance is_solvable_bot : is_solvable R ↥(⊥ : lie_ideal R L) :=
⟨⟨0, @subsingleton.elim _ lie_ideal.subsingleton_of_bot _ ⊥⟩⟩

instance is_solvable_add {I J : lie_ideal R L} [hI : is_solvable R I] [hJ : is_solvable R J] :
  is_solvable R ↥(I + J) :=
begin
  tactic.unfreeze_local_instances,
  obtain ⟨k, hk⟩ := hI,
  obtain ⟨l, hl⟩ := hJ,
  exact ⟨⟨k+l, lie_ideal.derived_series_add_eq_bot hk hl⟩⟩,
end

end lie_algebra

variables {R L}

namespace function

open lie_algebra

lemma injective.lie_algebra_is_solvable [h₁ : is_solvable R L] (h₂ : injective f) :
  is_solvable R L' :=
begin
  tactic.unfreeze_local_instances, obtain ⟨k, hk⟩ := h₁,
  use k,
  apply lie_ideal.bot_of_map_eq_bot h₂, rw [eq_bot_iff, ← hk],
  apply lie_ideal.derived_series_map_le,
end

lemma surjective.lie_algebra_is_solvable [h₁ : is_solvable R L'] (h₂ : surjective f) :
  is_solvable R L :=
begin
  tactic.unfreeze_local_instances, obtain ⟨k, hk⟩ := h₁,
  use k,
  rw [← lie_ideal.derived_series_map_eq k h₂, hk],
  simp only [lie_ideal.map_eq_bot_iff, bot_le],
end

end function

lemma lie_hom.is_solvable_range (f : L' →ₗ⁅R⁆ L) [h : lie_algebra.is_solvable R L'] :
  lie_algebra.is_solvable R f.range :=
f.surjective_range_restrict.lie_algebra_is_solvable

namespace lie_algebra

lemma solvable_iff_equiv_solvable (e : L' ≃ₗ⁅R⁆ L) : is_solvable R L' ↔ is_solvable R L :=
begin
  split; introsI h,
  { exact e.symm.injective.lie_algebra_is_solvable, },
  { exact e.injective.lie_algebra_is_solvable, },
end

lemma le_solvable_ideal_solvable {I J : lie_ideal R L} (h₁ : I ≤ J) (h₂ : is_solvable R J) :
  is_solvable R I :=
(lie_ideal.hom_of_le_injective h₁).lie_algebra_is_solvable

variables (R L)

@[priority 100]
instance of_abelian_is_solvable [is_lie_abelian L] : is_solvable R L :=
begin
  use 1,
  rw [← abelian_iff_derived_one_eq_bot, lie_abelian_iff_equiv_lie_abelian lie_ideal.top_equiv_self],
  apply_instance,
end

/-- The (solvable) radical of Lie algebra is the `Sup` of all solvable ideals. -/
def radical := Sup { I : lie_ideal R L | is_solvable R I }

/-- The radical of a Noetherian Lie algebra is solvable. -/
instance radical_is_solvable [is_noetherian R L] : is_solvable R (radical R L) :=
begin
  have hwf := lie_submodule.well_founded_of_noetherian R L L,
  rw ← complete_lattice.is_sup_closed_compact_iff_well_founded at hwf,
  refine hwf { I : lie_ideal R L | is_solvable R I } _ _,
  { use ⊥, exact lie_algebra.is_solvable_bot R L, },
  { intros I J hI hJ, apply lie_algebra.is_solvable_add R L; [exact hI, exact hJ], },
end

/-- The `→` direction of this lemma is actually true without the `is_noetherian` assumption. -/
lemma lie_ideal.solvable_iff_le_radical [is_noetherian R L] (I : lie_ideal R L) :
  is_solvable R I ↔ I ≤ radical R L :=
begin
  split; intros h,
  { exact le_Sup h, },
  { apply le_solvable_ideal_solvable h, apply_instance, },
end

lemma center_le_radical : center R L ≤ radical R L :=
have h : is_solvable R (center R L), { apply_instance, }, le_Sup h

/-- Given a solvable Lie ideal `I` with derived series `I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥`, this is the
natural number `k` (the number of inclusions).

For a non-solvable ideal, the value is 0. -/
noncomputable def derived_length_of_ideal (I : lie_ideal R L) : ℕ :=
Inf {k | derived_series_of_ideal R L k I = ⊥}

/-- The derived length of a Lie algebra is the derived length of its 'top' Lie ideal.

See also `lie_algebra.derived_length_eq_derived_length_of_ideal`. -/
noncomputable abbreviation derived_length : ℕ := derived_length_of_ideal R L ⊤

lemma derived_series_of_derived_length_succ (I : lie_ideal R L) (k : ℕ) :
  derived_length_of_ideal R L I = k + 1 ↔
  is_lie_abelian (derived_series_of_ideal R L k I) ∧ derived_series_of_ideal R L k I ≠ ⊥ :=
begin
  rw abelian_iff_derived_succ_eq_bot,
  let s := {k | derived_series_of_ideal R L k I = ⊥}, change Inf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s,
  have hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s,
  { intros k₁ k₂ h₁₂ h₁,
    suffices : derived_series_of_ideal R L k₂ I ≤ ⊥, { exact eq_bot_iff.mpr this, },
    change derived_series_of_ideal R L k₁ I = ⊥ at h₁, rw ← h₁,
    exact derived_series_of_ideal_antimono I h₁₂, },
  exact nat.Inf_upward_closed_eq_succ_iff hs k,
end

lemma derived_length_eq_derived_length_of_ideal (I : lie_ideal R L) :
  derived_length R I = derived_length_of_ideal R L I :=
begin
  let s₁ := {k | derived_series R I k = ⊥},
  let s₂ := {k | derived_series_of_ideal R L k I = ⊥},
  change Inf s₁ = Inf s₂,
  congr, ext k, exact I.derived_series_eq_bot_iff k,
end

variables {R L}

/-- Given a solvable Lie ideal `I` with derived series `I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥`, this is the
`k-1`th term in the derived series (and is therefore an Abelian ideal contained in `I`).

For a non-solvable ideal, this is the zero ideal, `⊥`. -/
noncomputable def derived_abelian_of_ideal (I : lie_ideal R L) : lie_ideal R L :=
match derived_length_of_ideal R L I with
| 0     := ⊥
| k + 1 := derived_series_of_ideal R L k I
end

lemma abelian_derived_abelian_of_ideal (I : lie_ideal R L) :
  is_lie_abelian (derived_abelian_of_ideal I) :=
begin
  dunfold derived_abelian_of_ideal,
  cases h : derived_length_of_ideal R L I with k,
  { exact is_lie_abelian_bot R L, },
  { rw derived_series_of_derived_length_succ at h, exact h.1, },
end

lemma derived_length_zero (I : lie_ideal R L) [hI : is_solvable R I] :
  derived_length_of_ideal R L I = 0 ↔ I = ⊥ :=
begin
  let s := {k | derived_series_of_ideal R L k I = ⊥}, change Inf s = 0 ↔ _,
  have hne : s ≠ ∅,
  { rw set.ne_empty_iff_nonempty,
    tactic.unfreeze_local_instances, obtain ⟨k, hk⟩ := hI, use k,
    rw [derived_series_def, lie_ideal.derived_series_eq_bot_iff] at hk, exact hk, },
  simp [hne],
end

lemma abelian_of_solvable_ideal_eq_bot_iff (I : lie_ideal R L) [h : is_solvable R I] :
  derived_abelian_of_ideal I = ⊥ ↔ I = ⊥ :=
begin
  dunfold derived_abelian_of_ideal,
  cases h : derived_length_of_ideal R L I with k,
  { rw derived_length_zero at h, rw h, refl, },
  { obtain ⟨h₁, h₂⟩ := (derived_series_of_derived_length_succ R L I k).mp h,
    have h₃ : I ≠ ⊥, { intros contra, apply h₂, rw contra, apply derived_series_of_bot_eq_bot, },
    change derived_series_of_ideal R L k I = ⊥ ↔ I = ⊥,
    split; contradiction, },
end

end lie_algebra

author: JLimperg


text:
import convex_body microid

open_locale topological_space

variables {V : Type}
[inner_product_space ℝ V] [finite_dimensional ℝ V]

def supp_locally_linear_with (U : set V) (K : convex_body V)
(x : V) :=
∀ v ∈ U, K.supp v = ⟪x, v⟫_ℝ

def supp_locally_linear (U : set V)
(K : convex_body V) :=
∃ x : V, supp_locally_linear_with U K x

def finsupp_sum {α : Type} (f : α →₀ ℝ) : ℝ :=
f.support.sum f.to_fun

noncomputable def finsupp_weighted_sum {α : Type} (w : α →₀ ℝ) (f : α → V) : V :=
w.support.sum (λ a, w a • f a)

structure supp_locally_linear'' (u : V) (ε : ℝ) (K : convex_body V) : Prop :=
/- (map_add : ∀ x y z, x ∈ U → y ∈ U → z ∈ U → x + y - z ∈ U → K.supp (x + y - z) = K.supp x + K.supp y - K.supp z)
(map_smul : ∀ (c : ℝ) x, x ∈ U → c • x ∈ U → K.supp (c • x) = c • K.supp x) -/
--(map_ll : ∀ (c : ℝ) x y z, x ∈ U → y ∈ U → z ∈ U → x + c • (y - z) ∈ U → K.supp (x + c • (y - z)) = K.supp x + c • (K.supp y - K.supp z))
(map_smul : ∀ (c δ : ℝ) x, δ • x + u ∈ metric.ball u ε → δ • (c • x) + u ∈ metric.ball u ε → K.supp (δ • (c • x) + u) - K.supp u = c * (K.supp (δ • x + u) - K.supp u))
(map_add : ∀ (δ : ℝ) x y, δ • x + u ∈ metric.ball u ε → δ • y + u ∈ metric.ball u ε → δ • (x + y) + u ∈ metric.ball u ε → K.supp (δ • (x + y) + u) - K.supp u = (K.supp (δ • x + u) - K.supp u) + (K.supp (δ • y + u) - K.supp u))
(map_hom : ∀ (δ : ℝ), δ • u ∈ metric.ball u ε → K.supp (δ • u) = δ • K.supp u)

structure supp_locally_linear' {ι : Type} (basis : basis ι ℝ V) (u : V) (ε : ℝ) (K : convex_body V) : Prop :=
--(ι : Type)
--(basis : basis ι ℝ V)
--(basis_mem : ∀ k : ι, basis k ∈ metric.ball u ε)
(linear : ∀ v : V, v ∈ metric.ball u ε →
K.supp v = (basis.repr v).sum (λ i ci, ci * K.supp (basis i)))

noncomputable def transform_into_ball (u : V) (ε : ℝ)
(v : V) : V :=
(ε / (2 * ∥v∥)) • v + u

lemma transform_into_ball_mem_ball (u : V) {ε : ℝ} (εpos : ε > 0)
(v : V) : transform_into_ball u ε v ∈ metric.ball u ε :=
begin
  simp only [transform_into_ball, metric.mem_ball, dist_eq_norm],
  simp only [add_sub_cancel, norm_smul, norm_div, norm_mul],
  simp only [real.norm_eq_abs, abs_eq_self.mpr (le_of_lt εpos)],
  simp only [abs_two, abs_norm_eq_norm],
  ring_nf,
  simp only [mul_inv],
  conv {
    to_rhs,
    rw [←one_mul ε],
  },
  rw [mul_lt_mul_right εpos, mul_comm, mul_assoc],
  by_cases h : ∥v∥ = 0,
  {
    simp only [h],
    simp only [mul_zero, zero_lt_one],
  },
  {
    rw [inv_mul_cancel h],
    ring_nf,
    exact half_lt_self (zero_lt_one),
  },
end

noncomputable def ll_extension (u : V) (ε : ℝ)
(f : V → ℝ) : V → ℝ :=
λ v, ((2 * ∥v∥) / ε) * (f (transform_into_ball u ε v) - f u)

lemma supp_locally_linear_iff {ι : Type} {b : basis ι ℝ V}
{u : V} {ε : ℝ} (εpos : ε > 0)
(hb : ∀ k : ι, b k ∈ metric.ball u ε)
(K : convex_body V) :
supp_locally_linear (metric.ball u ε) K ↔
supp_locally_linear' b u ε K :=
begin
  split,
  {
    rintro ⟨x, h⟩,
    refine ⟨_⟩,
    {
      intros v hv,
      rw [h v hv],
      simp only [h (b _) (hb _)],
      --simp only [←real_inner_smul_right],
      simp only [←smul_eq_mul],
      simp only [←finsupp.inner_sum],
      rw [←finsupp.total_apply],
      rw [basis.total_repr],
    },
  },
  {
    rintro ⟨hlin⟩,
    let f' : (ι →₀ ℝ) → ℝ := λ f, f.sum (λ i ci, ci * K.supp (b i)),
    let f := f' ∘ b.repr,
    have flin : is_linear_map ℝ f,
    {
      refine ⟨_, _⟩,
      {
        intros x y,
        simp only [f, f', function.comp_app],
        rw [map_add, finsupp.sum_add_index'],
        {
          simp only [zero_mul, eq_self_iff_true, implies_true_iff],
        },
        {
          simp only [add_mul, eq_self_iff_true, forall_forall_const, implies_true_iff],
        },
      },
      {
        intros d x,
        simp only [f, f', function.comp_app],
        rw [map_smul, finsupp.sum_smul_index', finsupp.smul_sum],
        {simp only [smul_mul_assoc]},
        {
          intro i,
          simp only [zero_mul],
        },
      },
    },
    have feq: ∀ v : V, v ∈ metric.ball u ε → f v = K.supp v,
    {
      intros v hv,
      symmetry,
      apply hlin,
      exact hv,
    },
    obtain ⟨hadd, hsmul⟩ := flin,
    let x := of_dual' ⟨_, hadd, hsmul⟩,
    refine ⟨x, _⟩,
    intros v hv,
    rw [←feq v hv],
    simp only [x, of_dual'],
    rw [inner_product_space.to_dual_symm_apply],
    refl,
  }
end

/-lemma inner_transform_into_ball (u : V) {ε : ℝ} (εpos : ε > 0)
(v w : V) :
(2 * ∥w∥ / ε) * (⟪v, (transform_into_ball u ε w)⟫_ℝ - ⟪v, u⟫_ℝ) =
⟪v, w⟫_ℝ := sorry

lemma ll_extension_eq_inner  {u : V} {ε : ℝ} (εpos : ε > 0)
{K : convex_body V} {x : V}
(h : supp_locally_linear_with (metric.ball u ε) K x) :
ll_extension u εpos K.supp = (λ v, ⟪x, v⟫_ℝ) :=
begin
  funext v,
  simp only [ll_extension],
  rw [h _ (transform_into_ball_mem_ball u εpos _)],
  rw [h u (metric.mem_ball_self εpos)],
  rw [inner_transform_into_ball u εpos],
end -/

/- lemma supp_locally_linear_iff_ll_extension_linear {u : V} {ε : ℝ} (εpos : ε > 0)
(K : convex_body V) :
supp_locally_linear (metric.ball u ε) K ↔ is_linear_map ℝ (ll_extension u εpos K.supp) :=
begin
  split,
  {
    rintro ⟨x, hx⟩,
    refine ⟨_, _⟩,
    all_goals {
      intros x y,
      simp only [ll_extension],
      repeat {rw [hx _ (transform_into_ball_mem_ball u εpos _)]},
      repeat {rw [hx u (metric.mem_ball_self εpos)]},
      repeat {rw [inner_transform_into_ball u εpos]},
      simp only [inner_add_right, inner_smul_right, smul_eq_mul],
    },
  },
  {
    rintro ⟨hadd, hsmul⟩,
    let f : V →ₗ[ℝ] ℝ := ⟨_, hadd, hsmul⟩,
    let x := of_dual' f,
  },
end -/

lemma supp_integrable {k : ℕ} (u : V)
{μ : measure_theory.finite_measure (microid_generator_space V k)} :
measure_theory.integrable (λ G, (body_of_microid_generator G).supp u) μ.val :=
begin
  let M := support_eval u '' (set.univ : set (microid_generator_space V k)),
  have gcp : is_compact (set.univ : set (microid_generator_space V k)) := compact_space.compact_univ,
  have Mcp : is_compact M := gcp.image supp_eval_continuous,
  have Mbdd := Mcp.bounded,
  rw [bounded_iff_forall_norm_le] at Mbdd,
  obtain ⟨C, hC⟩ := Mbdd,
  refine ⟨_, _⟩,
  {
    exact supp_eval_strongly_measurable.ae_strongly_measurable,
  },
  {
    apply measure_theory.has_finite_integral_of_bounded,
    rotate,
    {exact C},
    {
      apply filter.eventually_of_forall,
      intro G,
      apply hC,
      exact set.mem_image_of_mem _ (set.mem_univ _),
    },
  },
end

lemma exists_basis_in_ball {ε : ℝ} (u : V) (εpos : ε > 0) :
∃ (ι : Type) (b : basis ι ℝ V), ∀ k : ι, b k ∈ metric.ball u ε :=
begin
  have := linear_independent_empty ℝ V,
  let s := this.extend (set.empty_subset (metric.ball u ε)),
  have sli := this.linear_independent_extend (set.empty_subset (metric.ball u ε)),
  have sball : s ⊆ metric.ball u ε := this.extend_subset _,
  let b : basis s ℝ V := basis.mk _ _, rotate,
  {
    intro x, exact x,
  },
  {
    exact sli,
  },
  {
    rw [←ball_spans_submodule ⊤ u submodule.mem_top εpos],
    rw [submodule.span_le],
    simp only [subtype.range_coe_subtype, set.set_of_mem_eq],
    simp only [submodule.top_coe, set.inter_univ],
    exact this.subset_span_extend _,
  },
  refine ⟨_, b, _⟩,
  intro k,
  rw [basis.mk_apply],
  exact sball k.property,
end

lemma microid_supp_locally_linear_of_generators {k : ℕ} {ε : ℝ} {u : V}
(εpos : ε > 0)
(μ : microid_measure V k)
(h : ∀ G ∈ msupport μ,
supp_locally_linear (metric.ball u ε) (body_of_microid_generator G)) :
supp_locally_linear (metric.ball u ε) (microid_of_measure μ) :=
begin
  obtain ⟨ι, b, hb⟩ := exists_basis_in_ball u εpos,
  simp only [supp_locally_linear_iff εpos hb] at h ⊢,
  refine ⟨_⟩,
  {
    intros v hv,
    simp only [supp_microid_eq_integral],
    simp only [finsupp.sum],
    simp only [←measure_theory.integral_mul_left],
    rw [←measure_theory.integral_finset_sum],
    refine integral_eq_of_eq_on_msupport _ _ _,
    any_goals {apply measure_theory.integrable_finset_sum},
    any_goals {intros G hG},
    any_goals {apply measure_theory.integrable.const_mul},
    any_goals {apply supp_integrable},
    {
      obtain ⟨hlin'⟩ := h G hG,
      exact hlin' v hv,
    },
  },
end

lemma normal_face_singleton_iff_locally_linear_with
{U : set V} (oU : is_open U)
{K : convex_body V}
{x : V} :
supp_locally_linear_with U K x ↔
∀ u ∈ U, (K.normal_face u).val = {x} :=
begin
  rw [metric.is_open_iff] at oU,
  split,
  {
    intros h u hu,
    obtain ⟨ε, εpos, εball⟩ := oU u hu,
    have ss : (K.normal_face u).val ⊆ {x},
    {
      intros z hz,
      simp only [set.mem_singleton_iff],
      rw [←sub_eq_zero, ←real_inner_self_nonpos],
      rw [inner_sub_right, sub_nonpos],
      simp only [convex_body.normal_face, K.normal_face_supp u, set.mem_set_of] at hz,
      suffices hs : ∃ δ : ℝ, δ > 0 ∧ ⟪u + δ • (z - x), z⟫_ℝ ≤ ⟪u + δ • (z - x), x⟫_ℝ,
      {
        rcases hs with ⟨δ, δpos, hs⟩,
        simp only [inner_add_left, real_inner_smul_left] at hs,
        rw [real_inner_comm z u, real_inner_comm x u] at hs,
        simp only [hz, h u hu] at hs,
        simpa only [add_le_add_iff_left, mul_le_mul_left δpos] using hs,
      },
      by_cases hc : z - x = 0,
      {
        refine ⟨1, zero_lt_one, _⟩,
        rw [hc, smul_zero, add_zero],
        rw [real_inner_comm x u, real_inner_comm z u, ←h u hu],
        rw [hz.2],
      },
      {
        refine ⟨ε / (2 * ∥z - x∥), _, _⟩,
        {
          refine div_pos εpos _,
          simp only [zero_lt_mul_left, zero_lt_bit0, zero_lt_one, norm_pos_iff, ne.def, hc, not_false_iff],
        },
        {
          have : u + (ε / (2 * ∥z - x∥)) • (z - x) ∈ U,
          {
            apply εball,
            simp only [metric.mem_ball, dist_self_add_left],
            simp only [norm_smul, norm_div, norm_mul],
            simp only [real.norm_eq_abs, abs_eq_self.mpr (le_of_lt εpos)],
            simp only [abs_two, abs_norm_eq_norm],
            ring_nf,
            simp only [mul_inv],
            conv {
              to_rhs,
              rw [←one_mul ε],
            },
            rw [mul_lt_mul_right εpos, mul_comm, mul_assoc],
            change z - x ≠ 0 at hc,
            rw [←norm_ne_zero_iff] at hc,
            rw [inv_mul_cancel hc],
            ring_nf,
            exact half_lt_self (zero_lt_one),
          },
          have heq := h _ this,
          rw [real_inner_comm] at heq,
          rw [←heq],
          refine le_trans _ (K.inner_le_supp hz.1),
          exact le_of_eq (real_inner_comm _ _),
        },
      },
    },
    apply subset_antisymm,
    {
      exact ss,
    },
    {
      obtain ⟨y, hy⟩ := K.normal_face_nonempty u,
      have := ss hy,
      rw [set.mem_singleton_iff] at this,
      rw [set.singleton_subset_iff, ←this],
      exact hy,
    },
  },
  {
    intros h u hu,
    replace h := h u hu,
    have := set.mem_singleton x,
    simp only [←h, convex_body.normal_face, K.normal_face_supp] at this,
    exact this.2.symm,
  },
end

lemma normal_face_singleton_iff_locally_linear
{U : set V} (oU : is_open U)
{K : convex_body V} :
supp_locally_linear U K ↔
∃ x : V, ∀ u ∈ U, (K.normal_face u).val = {x} :=
begin
  apply exists_congr,
  intro x,
  exact normal_face_singleton_iff_locally_linear_with oU,
end

author: datokrat

repo: triangle-bodies


text:
/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen
-/
import algebra.algebra.tower
import algebra.ring.equiv
import group_theory.monoid_localization
import ring_theory.ideal.basic
import ring_theory.non_zero_divisors
import tactic.ring_exp

/-!
# Localizations of commutative rings

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

We characterize the localization of a commutative ring `R` at a submonoid `M` up to
isomorphism; that is, a commutative ring `S` is the localization of `R` at `M` iff we can find a
ring homomorphism `f : R →+* S` satisfying 3 properties:
1. For all `y ∈ M`, `f y` is a unit;
2. For all `z : S`, there exists `(x, y) : R × M` such that `z * f y = f x`;
3. For all `x, y : R`, `f x = f y` iff there exists `c ∈ M` such that `x * c = y * c`.

In the following, let `R, P` be commutative rings, `S, Q` be `R`- and `P`-algebras
and `M, T` be submonoids of `R` and `P` respectively, e.g.:
```
variables (R S P Q : Type*) [comm_ring R] [comm_ring S] [comm_ring P] [comm_ring Q]
variables [algebra R S] [algebra P Q] (M : submonoid R) (T : submonoid P)
```

## Main definitions

 * `is_localization (M : submonoid R) (S : Type*)` is a typeclass expressing that `S` is a
   localization of `R` at `M`, i.e. the canonical map `algebra_map R S : R →+* S` is a
   localization map (satisfying the above properties).
 * `is_localization.mk' S` is a surjection sending `(x, y) : R × M` to `f x * (f y)⁻¹`
 * `is_localization.lift` is the ring homomorphism from `S` induced by a homomorphism from `R`
   which maps elements of `M` to invertible elements of the codomain.
 * `is_localization.map S Q` is the ring homomorphism from `S` to `Q` which maps elements
   of `M` to elements of `T`
 * `is_localization.ring_equiv_of_ring_equiv`: if `R` and `P` are isomorphic by an isomorphism
   sending `M` to `T`, then `S` and `Q` are isomorphic
 * `is_localization.alg_equiv`: if `Q` is another localization of `R` at `M`, then `S` and `Q`
   are isomorphic as `R`-algebras

## Main results

 * `localization M S`, a construction of the localization as a quotient type, defined in
   `group_theory.monoid_localization`, has `comm_ring`, `algebra R` and `is_localization M`
   instances if `R` is a ring. `localization.away`, `localization.at_prime` and `fraction_ring`
   are abbreviations for `localization`s and have their corresponding `is_localization` instances

## Implementation notes

In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally `rewrite` one
structure with an isomorphic one; one way around this is to isolate a predicate characterizing
a structure up to isomorphism, and reason about things that satisfy the predicate.

A previous version of this file used a fully bundled type of ring localization maps,
then used a type synonym `f.codomain` for `f : localization_map M S` to instantiate the
`R`-algebra structure on `S`. This results in defining ad-hoc copies for everything already
defined on `S`. By making `is_localization` a predicate on the `algebra_map R S`,
we can ensure the localization map commutes nicely with other `algebra_map`s.

To prove most lemmas about a localization map `algebra_map R S` in this file we invoke the
corresponding proof for the underlying `comm_monoid` localization map
`is_localization.to_localization_map M S`, which can be found in `group_theory.monoid_localization`
and the namespace `submonoid.localization_map`.

To reason about the localization as a quotient type, use `mk_eq_of_mk'` and associated lemmas.
These show the quotient map `mk : R → M → localization M` equals the surjection
`localization_map.mk'` induced by the map `algebra_map : R →+* localization M`.
The lemma `mk_eq_of_mk'` hence gives you access to the results in the rest of the file,
which are about the `localization_map.mk'` induced by any localization map.

The proof that "a `comm_ring` `K` which is the localization of an integral domain `R` at `R \ {0}`
is a field" is a `def` rather than an `instance`, so if you want to reason about a field of
fractions `K`, assume `[field K]` instead of just `[comm_ring K]`.

## Tags
localization, ring localization, commutative ring localization, characteristic predicate,
commutative ring, field of fractions
-/

open function
open_locale big_operators

section comm_semiring
variables {R : Type*} [comm_semiring R] (M : submonoid R) (S : Type*) [comm_semiring S]
variables [algebra R S] {P : Type*} [comm_semiring P]

/-- The typeclass `is_localization (M : submodule R) S` where `S` is an `R`-algebra
expresses that `S` is isomorphic to the localization of `R` at `M`. -/
class is_localization : Prop :=
(map_units [] : ∀ y : M, is_unit (algebra_map R S y))
(surj [] : ∀ z : S, ∃ x : R × M, z * algebra_map R S x.2 = algebra_map R S x.1)
(eq_iff_exists [] : ∀ {x y}, algebra_map R S x = algebra_map R S y ↔ ∃ c : M, ↑c * x = ↑c * y)

variables {M S}

namespace is_localization

section is_localization

variables [is_localization M S]

section

variables (M)

lemma of_le (N : submonoid R) (h₁ : M ≤ N)
  (h₂ : ∀ r ∈ N, is_unit (algebra_map R S r)) : is_localization N S :=
{ map_units := λ r, h₂ r r.2,
  surj := λ s, by { obtain ⟨⟨x, y, hy⟩, H⟩ := is_localization.surj M s, exact ⟨⟨x, y, h₁ hy⟩, H⟩ },
  eq_iff_exists := λ x y, begin
    split,
    { rw is_localization.eq_iff_exists M,
      rintro ⟨c, hc⟩,
      exact ⟨⟨c, h₁ c.2⟩, hc⟩ },
    { rintro ⟨c, h⟩,
      simpa only [set_like.coe_mk, map_mul, (h₂ c c.2).mul_right_inj] using
        congr_arg (algebra_map R S) h }
  end }

variables (S)

/-- `is_localization.to_localization_with_zero_map M S` shows `S` is the monoid localization of
`R` at `M`. -/
@[simps]
def to_localization_with_zero_map : submonoid.localization_with_zero_map M S :=
{ to_fun := algebra_map R S,
  map_units' := is_localization.map_units _,
  surj' := is_localization.surj _,
  eq_iff_exists' := λ _ _, is_localization.eq_iff_exists _ _,
  .. algebra_map R S }

/-- `is_localization.to_localization_map M S` shows `S` is the monoid localization of `R` at `M`. -/
abbreviation to_localization_map : submonoid.localization_map M S :=
(to_localization_with_zero_map M S).to_localization_map

@[simp]
lemma to_localization_map_to_map :
  (to_localization_map M S).to_map = (algebra_map R S : R →*₀ S) := rfl

lemma to_localization_map_to_map_apply (x) :
  (to_localization_map M S).to_map x = algebra_map R S x := rfl

end

variables (M)

/-- Given a localization map `f : M →* N`, a section function sending `z : N` to some
`(x, y) : M × S` such that `f x * (f y)⁻¹ = z`. -/
noncomputable def sec (z : S) : R × M :=
classical.some $ is_localization.surj _ z

@[simp] lemma to_localization_map_sec : (to_localization_map M S).sec = sec M := rfl

/-- Given `z : S`, `is_localization.sec M z` is defined to be a pair `(x, y) : R × M` such
that `z * f y = f x` (so this lemma is true by definition). -/
lemma sec_spec (z : S) :
  z * algebra_map R S (is_localization.sec M z).2 =
    algebra_map R S (is_localization.sec M z).1 :=
classical.some_spec $ is_localization.surj _ z

/-- Given `z : S`, `is_localization.sec M z` is defined to be a pair `(x, y) : R × M` such
that `z * f y = f x`, so this lemma is just an application of `S`'s commutativity. -/
lemma sec_spec' (z : S) :
  algebra_map R S (is_localization.sec M z).1 =
    algebra_map R S (is_localization.sec M z).2 * z :=
by rw [mul_comm, sec_spec]

variables {R M}

lemma map_right_cancel {x y} {c : M} (h : algebra_map R S (c * x) = algebra_map R S (c * y)) :
  algebra_map R S x = algebra_map R S y :=
(to_localization_map M S).map_right_cancel h

lemma map_left_cancel {x y} {c : M} (h : algebra_map R S (x * c) = algebra_map R S (y * c)) :
  algebra_map R S x = algebra_map R S y :=
(to_localization_map M S).map_left_cancel h

lemma eq_zero_of_fst_eq_zero {z x} {y : M}
  (h : z * algebra_map R S y = algebra_map R S x) (hx : x = 0) : z = 0 :=
by { rw [hx, (algebra_map R S).map_zero] at h,
     exact (is_unit.mul_left_eq_zero (is_localization.map_units S y)).1 h}

variables (M S)

lemma map_eq_zero_iff (r : R) :
  algebra_map R S r = 0 ↔ ∃ m : M, ↑m * r = 0 :=
begin
  split,
  intro h,
  { obtain ⟨m, hm⟩ := (is_localization.eq_iff_exists M S).mp
      ((algebra_map R S).map_zero.trans h.symm),
    exact ⟨m, by simpa using hm.symm⟩ },
  { rintro ⟨m, hm⟩,
    rw [← (is_localization.map_units S m).mul_right_inj, mul_zero, ← ring_hom.map_mul, hm,
      ring_hom.map_zero] }
end

variables {M}

/-- `is_localization.mk' S` is the surjection sending `(x, y) : R × M` to
`f x * (f y)⁻¹`. -/
noncomputable def mk' (x : R) (y : M) : S :=
(to_localization_map M S).mk' x y

@[simp] lemma mk'_sec (z : S) :
  mk' S (is_localization.sec M z).1 (is_localization.sec M z).2 = z :=
(to_localization_map M S).mk'_sec _

lemma mk'_one (x) : mk' S x (1 : M) = algebra_map R S x :=
(to_localization_map M S).mk'_one _

@[simp]
lemma mk'_spec (x) (y : M) :
  mk' S x y * algebra_map R S y = algebra_map R S x :=
(to_localization_map M S).mk'_spec _ _

@[simp]
lemma mk'_spec' (x) (y : M) :
  algebra_map R S y * mk' S x y = algebra_map R S x :=
(to_localization_map M S).mk'_spec' _ _

@[simp]
lemma mk'_spec_mk (x) (y : R) (hy : y ∈ M) :
  mk' S x ⟨y, hy⟩ * algebra_map R S y = algebra_map R S x :=
mk'_spec S x ⟨y, hy⟩

@[simp]
lemma mk'_spec'_mk (x) (y : R) (hy : y ∈ M) :
  algebra_map R S y * mk' S x ⟨y, hy⟩ = algebra_map R S x :=
mk'_spec' S x ⟨y, hy⟩

variables {S}

theorem eq_mk'_iff_mul_eq {x} {y : M} {z} :
  z = mk' S x y ↔ z * algebra_map R S y = algebra_map R S x :=
(to_localization_map M S).eq_mk'_iff_mul_eq

theorem mk'_eq_iff_eq_mul {x} {y : M} {z} :
  mk' S x y = z ↔ algebra_map R S x = z * algebra_map R S y :=
(to_localization_map M S).mk'_eq_iff_eq_mul

theorem mk'_add_eq_iff_add_mul_eq_mul {x} {y : M} {z₁ z₂} :
  mk' S x y + z₁ = z₂ ↔ algebra_map R S x + z₁ * algebra_map R S y = z₂ * algebra_map R S y :=
by rw [←mk'_spec S x y, ←is_unit.mul_left_inj (is_localization.map_units S y), right_distrib]

variables (M)

lemma mk'_surjective (z : S) : ∃ x (y : M), mk' S x y = z :=
let ⟨r, hr⟩ := is_localization.surj _ z in ⟨r.1, r.2, (eq_mk'_iff_mul_eq.2 hr).symm⟩

variables (S)

include M

/-- The localization of a `fintype` is a `fintype`. Cannot be an instance. -/
noncomputable def fintype' [fintype R] : fintype S :=
have _ := classical.prop_decidable, by exactI
fintype.of_surjective (function.uncurry $ is_localization.mk' S)
                      (λ a, prod.exists'.mpr $ is_localization.mk'_surjective M a)

omit M

variables {M S}

/-- Localizing at a submonoid with 0 inside it leads to the trivial ring. -/
def unique_of_zero_mem (h : (0 : R) ∈ M) : unique S :=
unique_of_zero_eq_one $ by simpa using is_localization.map_units S ⟨0, h⟩

lemma mk'_eq_iff_eq {x₁ x₂} {y₁ y₂ : M} :
  mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebra_map R S (y₂ * x₁) = algebra_map R S (y₁ * x₂) :=
(to_localization_map M S).mk'_eq_iff_eq

lemma mk'_eq_iff_eq' {x₁ x₂} {y₁ y₂ : M} :
  mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebra_map R S (x₁ * y₂) = algebra_map R S (x₂ * y₁) :=
(to_localization_map M S).mk'_eq_iff_eq'

lemma mk'_mem_iff {x} {y : M} {I : ideal S} : mk' S x y ∈ I ↔ algebra_map R S x ∈ I :=
begin
  split;
  intro h,
  { rw [← mk'_spec S x y, mul_comm],
    exact I.mul_mem_left ((algebra_map R S) y) h },
  { rw ← mk'_spec S x y at h,
    obtain ⟨b, hb⟩ := is_unit_iff_exists_inv.1 (map_units S y),
    have := I.mul_mem_left b h,
    rwa [mul_comm, mul_assoc, hb, mul_one] at this }
end

protected lemma eq {a₁ b₁} {a₂ b₂ : M} :
  mk' S a₁ a₂ = mk' S b₁ b₂ ↔ ∃ c : M, ↑c * (↑b₂ * a₁) = c * (a₂ * b₁) :=
(to_localization_map M S).eq

lemma mk'_eq_zero_iff (x : R) (s : M) :
  mk' S x s = 0 ↔ ∃ (m : M), ↑m * x = 0 :=
by rw [← (map_units S s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff M]

@[simp] lemma mk'_zero (s : M) : is_localization.mk' S 0 s = 0 :=
by rw [eq_comm, is_localization.eq_mk'_iff_mul_eq, zero_mul, map_zero]

lemma ne_zero_of_mk'_ne_zero {x : R} {y : M} (hxy : is_localization.mk' S x y ≠ 0) : x ≠ 0 :=
begin
  rintro rfl,
  exact hxy (is_localization.mk'_zero _)
end

section ext

variables [algebra R P] [is_localization M P]

lemma eq_iff_eq {x y} :
  algebra_map R S x = algebra_map R S y ↔ algebra_map R P x = algebra_map R P y :=
(to_localization_map M S).eq_iff_eq (to_localization_map M P)

lemma mk'_eq_iff_mk'_eq {x₁ x₂}
  {y₁ y₂ : M} : mk' S x₁ y₁ = mk' S x₂ y₂ ↔ mk' P x₁ y₁ = mk' P x₂ y₂ :=
(to_localization_map M S).mk'_eq_iff_mk'_eq (to_localization_map M P)

lemma mk'_eq_of_eq {a₁ b₁ : R} {a₂ b₂ : M} (H : ↑a₂ * b₁ = ↑b₂ * a₁) :
  mk' S a₁ a₂ = mk' S b₁ b₂ :=
(to_localization_map M S).mk'_eq_of_eq H

lemma mk'_eq_of_eq' {a₁ b₁ : R} {a₂ b₂ : M} (H : b₁ * ↑a₂ = a₁ * ↑b₂) :
  mk' S a₁ a₂ = mk' S b₁ b₂ :=
(to_localization_map M S).mk'_eq_of_eq' H

variables (S)

@[simp] lemma mk'_self {x : R} (hx : x ∈ M) : mk' S x ⟨x, hx⟩ = 1 :=
(to_localization_map M S).mk'_self _ hx

@[simp] lemma mk'_self' {x : M} : mk' S (x : R) x = 1 :=
(to_localization_map M S).mk'_self' _

lemma mk'_self'' {x : M} : mk' S x.1 x = 1 :=
mk'_self' _

end ext

lemma mul_mk'_eq_mk'_of_mul (x y : R) (z : M) :
  (algebra_map R S) x * mk' S y z = mk' S (x * y) z :=
(to_localization_map M S).mul_mk'_eq_mk'_of_mul _ _ _

lemma mk'_eq_mul_mk'_one (x : R) (y : M) :
  mk' S x y = (algebra_map R S) x * mk' S 1 y :=
((to_localization_map M S).mul_mk'_one_eq_mk' _ _).symm

@[simp] lemma mk'_mul_cancel_left (x : R) (y : M) :
  mk' S (y * x : R) y = (algebra_map R S) x :=
(to_localization_map M S).mk'_mul_cancel_left _ _

lemma mk'_mul_cancel_right (x : R) (y : M) :
  mk' S (x * y) y = (algebra_map R S) x :=
(to_localization_map M S).mk'_mul_cancel_right _ _

@[simp] lemma mk'_mul_mk'_eq_one (x y : M) :
  mk' S (x : R) y * mk' S (y : R) x = 1 :=
by rw [←mk'_mul, mul_comm]; exact mk'_self _ _

lemma mk'_mul_mk'_eq_one' (x : R) (y : M) (h : x ∈ M) :
  mk' S x y * mk' S (y : R) ⟨x, h⟩ = 1 :=
mk'_mul_mk'_eq_one ⟨x, h⟩ _

section

variables (M)

lemma is_unit_comp (j : S →+* P) (y : M) :
  is_unit (j.comp (algebra_map R S) y) :=
(to_localization_map M S).is_unit_comp j.to_monoid_hom _

end

/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `comm_semiring`s
`g : R →+* P` such that `g(M) ⊆ units P`, `f x = f y → g x = g y` for all `x y : R`. -/
lemma eq_of_eq {g : R →+* P} (hg : ∀ y : M, is_unit (g y)) {x y}
  (h : (algebra_map R S) x = (algebra_map R S) y) :
  g x = g y :=
@submonoid.localization_map.eq_of_eq _ _ _ _ _ _ _
  (to_localization_map M S) g.to_monoid_hom hg _ _ h

lemma mk'_add (x₁ x₂ : R) (y₁ y₂ : M) :
  mk' S (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ + mk' S x₂ y₂ :=
mk'_eq_iff_eq_mul.2 $ eq.symm
begin
  rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
    mul_comm (_ * _), ←mul_assoc, add_comm, ←map_mul, mul_mk'_eq_mk'_of_mul,
    mk'_add_eq_iff_add_mul_eq_mul],
  simp only [map_add, submonoid.coe_mul, map_mul],
  ring
end

lemma mul_add_inv_left {g : R →+* P} (h : ∀ y : M, is_unit (g y)) (y : M) (w z₁ z₂ : P) :
  w * ↑(is_unit.lift_right (g.to_monoid_hom.restrict M) h y)⁻¹ + z₁ = z₂
    ↔ w + g y * z₁ = g y * z₂ :=
begin
  rw [mul_comm, ←one_mul z₁, ←units.inv_mul (is_unit.lift_right (g.to_monoid_hom.restrict M) h y),
    mul_assoc, ←mul_add, units.inv_mul_eq_iff_eq_mul, units.inv_mul_cancel_left,
    is_unit.coe_lift_right],
  simp only [ring_hom.to_monoid_hom_eq_coe, monoid_hom.restrict_apply, ring_hom.coe_monoid_hom]
end

lemma lift_spec_mul_add {g : R →+* P} (hg : ∀ y : M, is_unit (g y)) (z w w' v) :
  ((to_localization_with_zero_map M S).lift g.to_monoid_with_zero_hom hg) z * w + w' = v
    ↔ g ((to_localization_map M S).sec z).1 * w + g ((to_localization_map M S).sec z).2 * w'
      = g ((to_localization_map M S).sec z).2 * v :=
begin
  show  (_ * _) * _ + _ = _ ↔  _ = _,
  erw [mul_comm, ←mul_assoc, mul_add_inv_left hg, mul_comm],
  refl
end

/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `comm_semiring`s
`g : R →+* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` sending `z : S` to `g x * (g y)⁻¹`, where `(x, y) : R × M` are such that
`z = f x * (f y)⁻¹`. -/
noncomputable def lift {g : R →+* P} (hg : ∀ y : M, is_unit (g y)) : S →+* P :=
{ map_add' :=
  begin
    intros x y,
    erw [(to_localization_map M S).lift_spec, mul_add, mul_comm, eq_comm, lift_spec_mul_add,
      add_comm, mul_comm,mul_assoc,mul_comm,mul_assoc, lift_spec_mul_add],
    simp_rw ←mul_assoc,
    show g _ * g _ * g _ + g _ * g _ * g _ = g _ * g _ * g _,
    simp_rw [←map_mul g, ←map_add g],
    apply @eq_of_eq _ _ _ S _ _ _ _ _ g hg,
    simp only [sec_spec', to_localization_map_sec, map_add, map_mul],
    ring
  end,
  .. @submonoid.localization_with_zero_map.lift _ _ _ _ _ _ _
      (to_localization_with_zero_map M S) g.to_monoid_with_zero_hom hg }

variables {g : R →+* P} (hg : ∀ y : M, is_unit (g y))

/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `comm_semiring`s
`g : R →* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : R, y ∈ M`. -/
lemma lift_mk' (x y) :
  lift hg (mk' S x y) = g x * ↑(is_unit.lift_right (g.to_monoid_hom.restrict M) hg y)⁻¹ :=
(to_localization_map M S).lift_mk' _ _ _

lemma lift_mk'_spec (x v) (y : M) :
  lift hg (mk' S x y) = v ↔ g x = g y * v :=
(to_localization_map M S).lift_mk'_spec _ _ _ _

@[simp] lemma lift_eq (x : R) :
  lift hg ((algebra_map R S) x) = g x :=
(to_localization_map M S).lift_eq _ _

lemma lift_eq_iff {x y : R × M} :
  lift hg (mk' S x.1 x.2) = lift hg (mk' S y.1 y.2) ↔ g (x.1 * y.2) = g (y.1 * x.2) :=
(to_localization_map M S).lift_eq_iff _

@[simp] lemma lift_comp : (lift hg).comp (algebra_map R S) = g :=
ring_hom.ext $ monoid_hom.ext_iff.1 $ (to_localization_map M S).lift_comp _

@[simp] lemma lift_of_comp (j : S →+* P) :
  lift (is_unit_comp M j) = j :=
ring_hom.ext $ monoid_hom.ext_iff.1 $ (to_localization_map M S).lift_of_comp j.to_monoid_hom

variables (M)
/-- See note [partially-applied ext lemmas] -/
lemma monoid_hom_ext ⦃j k : S →* P⦄
  (h : j.comp (algebra_map R S : R →* S) = k.comp (algebra_map R S)) : j = k :=
submonoid.localization_map.epic_of_localization_map (to_localization_map M S) $
  monoid_hom.congr_fun h

/-- See note [partially-applied ext lemmas] -/
lemma ring_hom_ext ⦃j k : S →+* P⦄
  (h : j.comp (algebra_map R S) = k.comp (algebra_map R S)) : j = k :=
ring_hom.coe_monoid_hom_injective $ monoid_hom_ext M $ monoid_hom.ext $ ring_hom.congr_fun h

/- This is not an instance because the submonoid `M` would become a metavariable
  in typeclass search. -/
lemma alg_hom_subsingleton [algebra R P] : subsingleton (S →ₐ[R] P) :=
⟨λ f g, alg_hom.coe_ring_hom_injective $ is_localization.ring_hom_ext M $
  by rw [f.comp_algebra_map, g.comp_algebra_map]⟩

/-- To show `j` and `k` agree on the whole localization, it suffices to show they agree
on the image of the base ring, if they preserve `1` and `*`. -/
protected lemma ext (j k : S → P) (hj1 : j 1 = 1) (hk1 : k 1 = 1)
  (hjm : ∀ a b, j (a * b) = j a * j b) (hkm : ∀ a b, k (a * b) = k a * k b)
  (h : ∀ a, j (algebra_map R S a) = k (algebra_map R S a)) : j = k :=
monoid_hom.mk.inj (monoid_hom_ext M $ monoid_hom.ext h : (⟨j, hj1, hjm⟩ : S →* P) = ⟨k, hk1, hkm⟩)

variables {M}

lemma lift_unique {j : S →+* P}
  (hj : ∀ x, j ((algebra_map R S) x) = g x) : lift hg = j :=
ring_hom.ext $ monoid_hom.ext_iff.1 $ @submonoid.localization_map.lift_unique
  _ _ _ _ _ _ _ (to_localization_map M S) g.to_monoid_hom hg j.to_monoid_hom hj

@[simp] lemma lift_id (x) : lift (map_units S : ∀ y : M, is_unit _) x = x :=
(to_localization_map M S).lift_id _

lemma lift_surjective_iff :
  surjective (lift hg : S → P) ↔ ∀ v : P, ∃ x : R × M, v * g x.2 = g x.1 :=
(to_localization_map M S).lift_surjective_iff hg

lemma lift_injective_iff :
  injective (lift hg : S → P) ↔ ∀ x y, algebra_map R S x = algebra_map R S y ↔ g x = g y :=
(to_localization_map M S).lift_injective_iff hg

section map

variables {T : submonoid P} {Q : Type*} [comm_semiring Q] (hy : M ≤ T.comap g)
variables [algebra P Q] [is_localization T Q]

section

variables (Q)

/-- Map a homomorphism `g : R →+* P` to `S →+* Q`, where `S` and `Q` are
localizations of `R` and `P` at `M` and `T` respectively,
such that `g(M) ⊆ T`.

We send `z : S` to `algebra_map P Q (g x) * (algebra_map P Q (g y))⁻¹`, where
`(x, y) : R × M` are such that `z = f x * (f y)⁻¹`. -/
noncomputable def map (g : R →+* P) (hy : M ≤ T.comap g) : S →+* Q :=
@lift R _ M _ _ _ _ _ _ ((algebra_map P Q).comp g) (λ y, map_units _ ⟨g y, hy y.2⟩)

end

lemma map_eq (x) :
  map Q g hy ((algebra_map R S) x) = algebra_map P Q (g x) :=
lift_eq (λ y, map_units _ ⟨g y, hy y.2⟩) x

@[simp] lemma map_comp :
  (map Q g hy).comp (algebra_map R S) = (algebra_map P Q).comp g :=
lift_comp $ λ y, map_units _ ⟨g y, hy y.2⟩

lemma map_mk' (x) (y : M) :
  map Q g hy (mk' S x y) = mk' Q (g x) ⟨g y, hy y.2⟩ :=
@submonoid.localization_map.map_mk' _ _ _ _ _ _ _ (to_localization_map M S)
g.to_monoid_hom _ (λ y, hy y.2) _ _ (to_localization_map T Q) _ _

@[simp] lemma map_id (z : S) (h : M ≤ M.comap (ring_hom.id R) := le_refl M) :
  map S (ring_hom.id _) h z = z :=
lift_id _

lemma map_unique (j : S →+* Q)
  (hj : ∀ x : R, j (algebra_map R S x) = algebra_map P Q (g x)) : map Q g hy = j :=
lift_unique (λ y, map_units _ ⟨g y, hy y.2⟩) hj

/-- If `comm_semiring` homs `g : R →+* P, l : P →+* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
lemma map_comp_map {A : Type*} [comm_semiring A] {U : submonoid A} {W} [comm_semiring W]
  [algebra A W] [is_localization U W] {l : P →+* A} (hl : T ≤ U.comap l) :
  (map W l hl).comp (map Q g hy : S →+* _) = map W (l.comp g) (λ x hx, hl (hy hx)) :=
ring_hom.ext $ λ x, @submonoid.localization_map.map_map _ _ _ _ _ P _ (to_localization_map M S) g _
_ _ _ _ _ _ _ _ _ (to_localization_map U W) l _ x

/-- If `comm_semiring` homs `g : R →+* P, l : P →+* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
lemma map_map {A : Type*} [comm_semiring A] {U : submonoid A} {W} [comm_semiring W]
  [algebra A W] [is_localization U W] {l : P →+* A} (hl : T ≤ U.comap l) (x : S) :
  map W l hl (map Q g hy x) = map W (l.comp g) (λ x hx, hl (hy hx)) x :=
by rw ←map_comp_map hy hl; refl

lemma map_smul (x : S) (z : R) :
  map Q g hy (z • x : S) = g z • map Q g hy x :=
by rw [algebra.smul_def, algebra.smul_def, ring_hom.map_mul, map_eq]

section

variables (S Q)

/-- If `S`, `Q` are localizations of `R` and `P` at submonoids `M, T` respectively, an
isomorphism `j : R ≃+* P` such that `j(M) = T` induces an isomorphism of localizations
`S ≃+* Q`. -/
@[simps]
noncomputable def ring_equiv_of_ring_equiv (h : R ≃+* P) (H : M.map h.to_monoid_hom = T) :
  S ≃+* Q :=
have H' : T.map h.symm.to_monoid_hom = M,
by { rw [← M.map_id, ← H, submonoid.map_map], congr, ext, apply h.symm_apply_apply },
{ to_fun := map Q (h : R →+* P) (M.le_comap_of_map_le (le_of_eq H)),
  inv_fun := map S (h.symm : P →+* R) (T.le_comap_of_map_le (le_of_eq H')),
  left_inv := λ x, by { rw [map_map, map_unique _ (ring_hom.id _), ring_hom.id_apply],
                        intro x, convert congr_arg (algebra_map R S) (h.symm_apply_apply x).symm },
  right_inv := λ x, by { rw [map_map, map_unique _ (ring_hom.id _), ring_hom.id_apply],
                         intro x, convert congr_arg (algebra_map P Q) (h.apply_symm_apply x).symm },
  .. map Q (h : R →+* P) _ }

end

lemma ring_equiv_of_ring_equiv_eq_map {j : R ≃+* P} (H : M.map j.to_monoid_hom = T) :
  (ring_equiv_of_ring_equiv S Q j H : S →+* Q) =
    map Q (j : R →+* P) (M.le_comap_of_map_le (le_of_eq H)) := rfl

@[simp] lemma ring_equiv_of_ring_equiv_eq {j : R ≃+* P} (H : M.map j.to_monoid_hom = T) (x) :
  ring_equiv_of_ring_equiv S Q j H ((algebra_map R S) x) = algebra_map P Q (j x) :=
map_eq _ _

lemma ring_equiv_of_ring_equiv_mk' {j : R ≃+* P} (H : M.map j.to_monoid_hom = T) (x : R) (y : M) :
  ring_equiv_of_ring_equiv S Q j H (mk' S x y) =
    mk' Q (j x) ⟨j y, show j y ∈ T, from H ▸ set.mem_image_of_mem j y.2⟩ :=
map_mk' _ _ _

end map

section alg_equiv

variables {Q : Type*} [comm_semiring Q] [algebra R Q] [is_localization M Q]

section

variables (M S Q)

/-- If `S`, `Q` are localizations of `R` at the submonoid `M` respectively,
there is an isomorphism of localizations `S ≃ₐ[R] Q`. -/
@[simps]
noncomputable def alg_equiv : S ≃ₐ[R] Q :=
{ commutes' := ring_equiv_of_ring_equiv_eq _,
  .. ring_equiv_of_ring_equiv S Q (ring_equiv.refl R) M.map_id }

end

@[simp]
lemma alg_equiv_mk' (x : R) (y : M) : alg_equiv M S Q (mk' S x y) = mk' Q x y:=
map_mk' _ _ _

@[simp]
lemma alg_equiv_symm_mk' (x : R) (y : M) : (alg_equiv M S Q).symm (mk' Q x y) = mk' S x y:=
map_mk' _ _ _

end alg_equiv

end is_localization

section

variables (M)

lemma is_localization_of_alg_equiv [algebra R P] [is_localization M S] (h : S ≃ₐ[R] P) :
  is_localization M P :=
begin
  constructor,
  { intro y,
    convert (is_localization.map_units S y).map h.to_alg_hom.to_ring_hom.to_monoid_hom,
    exact (h.commutes y).symm },
  { intro y,
    obtain ⟨⟨x, s⟩, e⟩ := is_localization.surj M (h.symm y),
    apply_fun h at e,
    simp only [h.map_mul, h.apply_symm_apply, h.commutes] at e,
    exact ⟨⟨x, s⟩, e⟩ },
  { intros x y,
    rw [← h.symm.to_equiv.injective.eq_iff, ← is_localization.eq_iff_exists M S,
      ← h.symm.commutes, ← h.symm.commutes],
    refl }
end

lemma is_localization_iff_of_alg_equiv [algebra R P] (h : S ≃ₐ[R] P) :
  is_localization M S ↔ is_localization M P :=
⟨λ _, by exactI is_localization_of_alg_equiv M h,
  λ _, by exactI is_localization_of_alg_equiv M h.symm⟩

lemma is_localization_iff_of_ring_equiv (h : S ≃+* P) :
  is_localization M S ↔
    @@is_localization _ M P _ (h.to_ring_hom.comp $ algebra_map R S).to_algebra :=
begin
  letI := (h.to_ring_hom.comp $ algebra_map R S).to_algebra,
  exact is_localization_iff_of_alg_equiv M { commutes' := λ _, rfl, ..h },
end

variable (S)

lemma is_localization_of_base_ring_equiv [is_localization M S] (h : R ≃+* P) :
  @@is_localization _ (M.map h.to_monoid_hom) S _
    ((algebra_map R S).comp h.symm.to_ring_hom).to_algebra :=
begin
  constructor,
  { rintros ⟨_, ⟨y, hy, rfl⟩⟩,
    convert is_localization.map_units S ⟨y, hy⟩,
    dsimp only [ring_hom.algebra_map_to_algebra, ring_hom.comp_apply],
    exact congr_arg _ (h.symm_apply_apply _) },
  { intro y,
    obtain ⟨⟨x, s⟩, e⟩ := is_localization.surj M y,
    refine ⟨⟨h x, _, _, s.prop, rfl⟩, _⟩,
    dsimp only [ring_hom.algebra_map_to_algebra, ring_hom.comp_apply] at ⊢ e,
    convert e; exact h.symm_apply_apply _ },
  { intros x y,
    rw [ring_hom.algebra_map_to_algebra, ring_hom.comp_apply, ring_hom.comp_apply,
      is_localization.eq_iff_exists M S],
    simp_rw ← h.to_equiv.apply_eq_iff_eq,
    change (∃ (c : M), h (c * h.symm x) = h (c * h.symm y)) ↔ _,
    simp only [ring_equiv.apply_symm_apply, ring_equiv.map_mul],
    exact ⟨λ ⟨c, e⟩, ⟨⟨_, _, c.prop, rfl⟩, e⟩, λ ⟨⟨_, c, h, e₁⟩, e₂⟩, ⟨⟨_, h⟩, e₁.symm ▸ e₂⟩⟩ }
end

lemma is_localization_iff_of_base_ring_equiv (h : R ≃+* P) :
  is_localization M S ↔ @@is_localization _ (M.map h.to_monoid_hom) S _
    ((algebra_map R S).comp h.symm.to_ring_hom).to_algebra :=
begin
  refine ⟨λ _, by exactI is_localization_of_base_ring_equiv _ _ h, _⟩,
  letI := ((algebra_map R S).comp h.symm.to_ring_hom).to_algebra,
  intro H,
  convert @@is_localization_of_base_ring_equiv _ _ _ _ _ _ H h.symm,
  { erw [submonoid.map_equiv_eq_comap_symm, submonoid.comap_map_eq_of_injective],
    exact h.to_equiv.injective },
  rw [ring_hom.algebra_map_to_algebra, ring_hom.comp_assoc],
  simp only [ring_hom.comp_id, ring_equiv.symm_symm, ring_equiv.symm_to_ring_hom_comp_to_ring_hom],
  apply algebra.algebra_ext,
  intro r,
  rw ring_hom.algebra_map_to_algebra
end

end

variables (M S)

include M

lemma non_zero_divisors_le_comap [is_localization M S] :
  non_zero_divisors R ≤ (non_zero_divisors S).comap (algebra_map R S)  :=
begin
  rintros a ha b (e : b * algebra_map R S a = 0),
  obtain ⟨x, s, rfl⟩ := mk'_surjective M b,
  rw [← @mk'_one R _ M, ← mk'_mul, ← (algebra_map R S).map_zero, ← @mk'_one R _ M,
    is_localization.eq] at e,
  obtain ⟨c, e⟩ := e,
  rw [mul_zero, mul_zero, submonoid.coe_one, one_mul, ←mul_assoc] at e,
  rw mk'_eq_zero_iff,
  exact ⟨c, ha _ e⟩
end

lemma map_non_zero_divisors_le [is_localization M S] :
  (non_zero_divisors R).map (algebra_map R S) ≤ non_zero_divisors S  :=
submonoid.map_le_iff_le_comap.mpr (non_zero_divisors_le_comap M S)

end is_localization

namespace localization

open is_localization

/-! ### Constructing a localization at a given submonoid -/

variables {M}

section

instance [subsingleton R] : unique (localization M) :=
⟨⟨1⟩, begin intro a, induction a, induction default, congr, refl, refl end⟩

/-- Addition in a ring localization is defined as `⟨a, b⟩ + ⟨c, d⟩ = ⟨b * c + d * a, b * d⟩`.

Should not be confused with `add_localization.add`, which is defined as
`⟨a, b⟩ + ⟨c, d⟩ = ⟨a + c, b + d⟩`.
-/
@[irreducible] protected def add (z w : localization M) : localization M :=
localization.lift_on₂ z w
  (λ a b c d, mk ((b : R) * c + d * a) (b * d)) $
λ a a' b b' c c' d d' h1 h2, mk_eq_mk_iff.2
begin
  rw r_eq_r' at h1 h2 ⊢,
  cases h1 with t₅ ht₅,
  cases h2 with t₆ ht₆,
  use t₅ * t₆,
  dsimp only,
  calc  (↑t₅ * ↑t₆) * ((↑b' * ↑d') * ((b : R) * c + d * a)) =
      (t₆ * (d' * c)) * (t₅ * (b' * b)) + (t₅ * (b' * a)) * (t₆ * (d' * d)) : by ring
      ... = (t₅ * t₆) * ((b * d)  * (b' * c' + d' * a')) : by rw [ht₆, ht₅]; ring
end

instance : has_add (localization M) := ⟨localization.add⟩

lemma add_mk (a b c d) : (mk a b : localization M) + mk c d = mk (b * c + d * a) (b * d) :=
by { unfold has_add.add localization.add, apply lift_on₂_mk }

lemma add_mk_self (a b c) : (mk a b : localization M) + mk c b = mk (a + c) b :=
begin
  rw [add_mk, mk_eq_mk_iff, r_eq_r'],
  refine (r' M).symm ⟨1, _⟩,
  simp only [submonoid.coe_one, submonoid.coe_mul],
  ring
end

private meta def tac := `[
{ intros,
  simp only [add_mk, localization.mk_mul, ← localization.mk_zero 1],
  refine mk_eq_mk_iff.mpr (r_of_eq _),
  simp only [submonoid.coe_mul],
  ring }]

instance : comm_semiring (localization M) :=
{ zero := 0,
  one  := 1,
  add  := (+),
  mul  := (*),
  npow := localization.npow _,
  nsmul := (•),
  nsmul_zero' := λ x, localization.induction_on x
    (λ x, by simp only [smul_mk, zero_nsmul, mk_zero]),
  nsmul_succ' := λ n x, localization.induction_on x
    (λ x, by simp only [smul_mk, succ_nsmul, add_mk_self]),
  add_assoc      := λ m n k, localization.induction_on₃ m n k (by tac),
  zero_add       := λ y, localization.induction_on y (by tac),
  add_zero       := λ y, localization.induction_on y (by tac),
  add_comm       := λ y z, localization.induction_on₂ z y (by tac),
  left_distrib   := λ m n k, localization.induction_on₃ m n k (by tac),
  right_distrib  := λ m n k, localization.induction_on₃ m n k (by tac),
  .. localization.comm_monoid_with_zero M }

/--For any given denominator `b : M`, the map `a ↦ a / b` is an `add_monoid_hom` from `R` to
  `localization M`-/
@[simps]
def mk_add_monoid_hom (b : M) : R →+ localization M :=
{ to_fun := λ a, mk a b,
  map_zero' := mk_zero _,
  map_add' := λ x y, (add_mk_self _ _ _).symm }

lemma mk_sum {ι : Type*} (f : ι → R) (s : finset ι) (b : M) :
  mk (∑ i in s, f i) b = ∑ i in s, mk (f i) b :=
(mk_add_monoid_hom b).map_sum f s

lemma mk_list_sum (l : list R) (b : M) :
  mk l.sum b = (l.map $ λ a, mk a b).sum :=
(mk_add_monoid_hom b).map_list_sum l

lemma mk_multiset_sum (l : multiset R) (b : M) :
  mk l.sum b = (l.map $ λ a, mk a b).sum :=
(mk_add_monoid_hom b).map_multiset_sum l

instance {S : Type*} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] :
  distrib_mul_action S (localization M) :=
{ smul_zero := λ s, by simp only [←localization.mk_zero 1, localization.smul_mk, smul_zero],
  smul_add := λ s x y, localization.induction_on₂ x y $
    prod.rec $ by exact λ r₁ x₁, prod.rec $ by exact λ r₂ x₂,
      by simp only [localization.smul_mk, localization.add_mk, smul_add, mul_comm _ (s • _),
                    mul_comm _ r₁, mul_comm _ r₂, smul_mul_assoc] }

instance {S : Type*} [semiring S] [mul_semiring_action S R] [is_scalar_tower S R R] :
  mul_semiring_action S (localization M) :=
{ ..localization.mul_distrib_mul_action }

instance {S : Type*} [semiring S] [module S R] [is_scalar_tower S R R] :
  module S (localization M) :=
{ zero_smul := localization.ind $ prod.rec $
    by { intros, simp only [localization.smul_mk, zero_smul, mk_zero] },
  add_smul := λ s₁ s₂, localization.ind $ prod.rec $
    by { intros, simp only [localization.smul_mk, add_smul, add_mk_self] },
  ..localization.distrib_mul_action }

instance {S : Type*} [comm_semiring S] [algebra S R] : algebra S (localization M) :=
{ to_ring_hom :=
  ring_hom.comp
  { to_fun := (monoid_of M).to_map,
    map_zero' := by rw [← mk_zero (1 : M), mk_one_eq_monoid_of_mk],
    map_add' := λ x y,
      by simp only [← mk_one_eq_monoid_of_mk, add_mk, submonoid.coe_one, one_mul, add_comm],
    .. localization.monoid_of M } (algebra_map S R),
  smul_def' := λ s, localization.ind $ prod.rec $ begin
    intros r x,
    dsimp,
    simp only [←mk_one_eq_monoid_of_mk, mk_mul, localization.smul_mk, one_mul, algebra.smul_def],
  end,
  commutes' := λ s, localization.ind $ prod.rec $ begin
    intros r x,
    dsimp,
    simp only [←mk_one_eq_monoid_of_mk, mk_mul, localization.smul_mk, one_mul, mul_one,
               algebra.commutes],
  end }

instance : is_localization M (localization M) :=
{ map_units := (localization.monoid_of M).map_units,
  surj := (localization.monoid_of M).surj,
  eq_iff_exists := λ _ _, (localization.monoid_of M).eq_iff_exists }

end

@[simp] lemma to_localization_map_eq_monoid_of :
  to_localization_map M (localization M) = monoid_of M := rfl

lemma monoid_of_eq_algebra_map (x) :
  (monoid_of M).to_map x = algebra_map R (localization M) x :=
rfl

lemma mk_one_eq_algebra_map (x) : mk x 1 = algebra_map R (localization M) x := rfl

lemma mk_eq_mk'_apply (x y) : mk x y = is_localization.mk' (localization M) x y :=
by rw [mk_eq_monoid_of_mk'_apply, mk', to_localization_map_eq_monoid_of]

@[simp] lemma mk_eq_mk' : (mk : R → M → localization M) = is_localization.mk' (localization M) :=
mk_eq_monoid_of_mk'

lemma mk_algebra_map {A : Type*} [comm_semiring A] [algebra A R] (m : A) :
  mk (algebra_map A R m) 1 = algebra_map A (localization M) m :=
by rw [mk_eq_mk', mk'_eq_iff_eq_mul, submonoid.coe_one, map_one, mul_one]; refl

lemma mk_nat_cast (m : ℕ) : (mk m 1 : localization M) = m :=
by simpa using @mk_algebra_map R _ M ℕ _ _ m

variables [is_localization M S]

section

variables (M S)

/-- The localization of `R` at `M` as a quotient type is isomorphic to any other localization. -/
@[simps]
noncomputable def alg_equiv : localization M ≃ₐ[R] S :=
is_localization.alg_equiv M _ _

/-- The localization of a singleton is a singleton. Cannot be an instance due to metavariables. -/
noncomputable def _root_.is_localization.unique (R Rₘ) [comm_semiring R] [comm_semiring Rₘ]
  (M : submonoid R) [subsingleton R] [algebra R Rₘ] [is_localization M Rₘ] : unique Rₘ :=
have inhabited Rₘ := ⟨1⟩,
by exactI (alg_equiv M Rₘ).symm.injective.unique

end

@[simp] lemma alg_equiv_mk' (x : R) (y : M) :
  alg_equiv M S (mk' (localization M) x y) = mk' S x y :=
alg_equiv_mk' _ _

@[simp] lemma alg_equiv_symm_mk' (x : R) (y : M) :
  (alg_equiv M S).symm (mk' S x y) = mk' (localization M) x y :=
alg_equiv_symm_mk' _ _

lemma alg_equiv_mk (x y) :
  alg_equiv M S (mk x y) = mk' S x y :=
by rw [mk_eq_mk', alg_equiv_mk']

lemma alg_equiv_symm_mk (x : R) (y : M) :
  (alg_equiv M S).symm (mk' S x y) = mk x y :=
by rw [mk_eq_mk', alg_equiv_symm_mk']

end localization

end comm_semiring

section comm_ring
variables {R : Type*} [comm_ring R] {M : submonoid R} (S : Type*) [comm_ring S]
variables [algebra R S] {P : Type*} [comm_ring P]

namespace localization

/-- Negation in a ring localization is defined as `-⟨a, b⟩ = ⟨-a, b⟩`. -/
@[irreducible] protected def neg (z : localization M) : localization M :=
localization.lift_on z (λ a b, mk (-a) b) $
  λ a b c d h, mk_eq_mk_iff.2
begin
  rw r_eq_r' at h ⊢,
  cases h with t ht,
  use t,
  rw [mul_neg, mul_neg, ht],
  ring_nf,
end

instance : has_neg (localization M) := ⟨localization.neg⟩

lemma neg_mk (a b) : -(mk a b : localization M) = mk (-a) b :=
by { unfold has_neg.neg localization.neg, apply lift_on_mk }

instance : comm_ring (localization M) :=
{ zsmul := (•),
  zsmul_zero' := λ x, localization.induction_on x
    (λ x, by simp only [smul_mk, zero_zsmul, mk_zero]),
  zsmul_succ' := λ n x, localization.induction_on x
    (λ x, by simp [smul_mk, add_mk_self, -mk_eq_monoid_of_mk', add_comm (n : ℤ) 1, add_smul]),
  zsmul_neg' := λ n x, localization.induction_on x
    (λ x, by { rw [smul_mk, smul_mk, neg_mk, ← neg_smul], refl }),
  neg            := has_neg.neg,
  sub            := λ x y, x + -y,
  sub_eq_add_neg := λ x y, rfl,
  add_left_neg   := λ y, by exact localization.induction_on y
  begin
    intros,
    simp only [add_mk, localization.mk_mul, neg_mk, ← mk_zero 1],
    refine mk_eq_mk_iff.mpr (r_of_eq _),
    simp only [submonoid.coe_mul],
    ring
  end,
   .. localization.comm_semiring }

lemma sub_mk (a c) (b d) : (mk a b : localization M) - mk c d = mk (d * a - b * c) (b * d) :=
calc  mk a b - mk c d
    = mk a b + (- mk c d) : sub_eq_add_neg _ _
... = mk a b + (mk (-c) d) : by rw neg_mk
... = mk (b * (-c) + d * a) (b * d) : add_mk _ _ _ _
... = mk (d * a - b * c) (b * d) : by congr'; ring

lemma mk_int_cast (m : ℤ) : (mk m 1 : localization M) = m :=
by simpa using @mk_algebra_map R _ M ℤ _ _ m

end localization

namespace is_localization

variables {R M} (S) {K : Type*} [is_localization M S]

lemma to_map_eq_zero_iff {x : R} (hM : M ≤ non_zero_divisors R) :
  algebra_map R S x = 0 ↔ x = 0 :=
begin
  rw ← (algebra_map R S).map_zero,
  split; intro h,
  { cases (eq_iff_exists M S).mp h with c hc,
    rw [mul_zero, mul_comm] at hc,
    exact hM c.2 x hc },
  { rw h },
end

protected lemma injective (hM : M ≤ non_zero_divisors R) :
  injective (algebra_map R S) :=
begin
  rw injective_iff_map_eq_zero (algebra_map R S),
  intros a ha,
  rwa to_map_eq_zero_iff S hM at ha
end

protected lemma to_map_ne_zero_of_mem_non_zero_divisors [nontrivial R]
  (hM : M ≤ non_zero_divisors R) {x : R} (hx : x ∈ non_zero_divisors R) : algebra_map R S x ≠ 0 :=
show (algebra_map R S).to_monoid_with_zero_hom x ≠ 0,
from map_ne_zero_of_mem_non_zero_divisors (algebra_map R S) (is_localization.injective S hM) hx

variables {S}

lemma sec_snd_ne_zero [nontrivial R] (hM : M ≤ non_zero_divisors R) (x : S) :
  ((sec M x).snd : R) ≠ 0 :=
non_zero_divisors.coe_ne_zero ⟨(sec M x).snd.val, hM (sec M x).snd.property⟩

lemma sec_fst_ne_zero [nontrivial R] [no_zero_divisors S] (hM : M ≤ non_zero_divisors R) {x : S}
  (hx : x ≠ 0) : (sec M x).fst ≠ 0 :=
begin
  have hsec := sec_spec M x,
  intro hfst,
  rw [hfst, map_zero, mul_eq_zero, _root_.map_eq_zero_iff] at hsec,
  { exact or.elim hsec hx (sec_snd_ne_zero hM x) },
  { exact is_localization.injective S hM }
end

variables (S M) (Q : Type*) [comm_ring Q] {g : R →+* P} [algebra P Q]

/-- Injectivity of a map descends to the map induced on localizations. -/
lemma map_injective_of_injective
  (hg : function.injective g) [is_localization (M.map g : submonoid P) Q] :
  function.injective (map Q g M.le_comap_map : S → Q) :=
begin
  rw injective_iff_map_eq_zero,
  intros z hz,
  obtain ⟨a, b, rfl⟩ := mk'_surjective M z,
  rw [map_mk', mk'_eq_zero_iff] at hz,
  obtain ⟨⟨m', hm'⟩, hm⟩ := hz,
  rw submonoid.mem_map at hm',
  obtain ⟨n, hn, hnm⟩ := hm',
  rw [subtype.coe_mk, ← hnm,  ← map_mul, ← map_zero g] at hm,
  rw [mk'_eq_zero_iff],
  exact ⟨⟨n, hn⟩, hg hm⟩,
end

variables {S Q M}

variables (A : Type*) [comm_ring A] [is_domain A]

/-- A `comm_ring` `S` which is the localization of a ring `R` without zero divisors at a subset of
non-zero elements does not have zero divisors.
See note [reducible non-instances]. -/
@[reducible]
theorem no_zero_divisors_of_le_non_zero_divisors
  [algebra A S] {M : submonoid A} [is_localization M S]
  (hM : M ≤ non_zero_divisors A) : no_zero_divisors S :=
{ eq_zero_or_eq_zero_of_mul_eq_zero :=
    begin
      intros z w h,
      cases surj M z with x hx,
      cases surj M w with y hy,
      have : z * w * algebra_map A S y.2 * algebra_map A S x.2 =
        algebra_map A S x.1 * algebra_map A S y.1,
      by rw [mul_assoc z, hy, ←hx]; ring,
      rw [h, zero_mul, zero_mul, ← (algebra_map A S).map_mul] at this,
      cases eq_zero_or_eq_zero_of_mul_eq_zero ((to_map_eq_zero_iff S hM).mp this.symm) with H H,
      { exact or.inl (eq_zero_of_fst_eq_zero hx H) },
      { exact or.inr (eq_zero_of_fst_eq_zero hy H) },
    end }

/-- A `comm_ring` `S` which is the localization of an integral domain `R` at a subset of
non-zero elements is an integral domain.
See note [reducible non-instances]. -/
@[reducible]
theorem is_domain_of_le_non_zero_divisors
  [algebra A S] {M : submonoid A} [is_localization M S]
  (hM : M ≤ non_zero_divisors A) : is_domain S :=
begin
  apply no_zero_divisors.to_is_domain _,
  { exact ⟨⟨(algebra_map A S) 0, (algebra_map A S) 1,
                      λ h, zero_ne_one (is_localization.injective S hM h)⟩⟩ },
  { exact no_zero_divisors_of_le_non_zero_divisors _ hM }
end

variables {A}

/-- The localization at of an integral domain to a set of non-zero elements is an integral domain.
See note [reducible non-instances]. -/
@[reducible]
theorem is_domain_localization {M : submonoid A} (hM : M ≤ non_zero_divisors A) :
  is_domain (localization M) :=
is_domain_of_le_non_zero_divisors _ hM

end is_localization

open is_localization

/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements. -/
lemma is_field.localization_map_bijective
  {R Rₘ : Type*} [comm_ring R] [comm_ring Rₘ]
  {M : submonoid R} (hM : (0 : R) ∉ M) (hR : is_field R)
  [algebra R Rₘ] [is_localization M Rₘ] : function.bijective (algebra_map R Rₘ) :=
begin
  letI := hR.to_field,
  replace hM := le_non_zero_divisors_of_no_zero_divisors hM,
  refine ⟨is_localization.injective _ hM, λ x, _⟩,
  obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M x,
  obtain ⟨n, hn⟩ := hR.mul_inv_cancel (non_zero_divisors.ne_zero $ hM hm),
  exact ⟨r * n, by erw [eq_mk'_iff_mul_eq, ←map_mul, mul_assoc, mul_comm n, hn, mul_one]⟩
end

/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements. -/
lemma field.localization_map_bijective
  {K Kₘ : Type*} [field K] [comm_ring Kₘ] {M : submonoid K} (hM : (0 : K) ∉ M)
  [algebra K Kₘ] [is_localization M Kₘ] : function.bijective (algebra_map K Kₘ) :=
(field.to_is_field K).localization_map_bijective hM
-- this looks weird due to the `letI` inside the above lemma, but trying to do it the other
-- way round causes issues with defeq of instances, so this is actually easier.

section algebra

variables {R S} {Rₘ Sₘ : Type*} [comm_ring Rₘ] [comm_ring Sₘ]
variables [algebra R Rₘ] [is_localization M Rₘ]
variables [algebra S Sₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ]

section

variables (S M)

/-- Definition of the natural algebra induced by the localization of an algebra.
Given an algebra `R → S`, a submonoid `R` of `M`, and a localization `Rₘ` for `M`,
let `Sₘ` be the localization of `S` to the image of `M` under `algebra_map R S`.
Then this is the natural algebra structure on `Rₘ → Sₘ`, such that the entire square commutes,
where `localization_map.map_comp` gives the commutativity of the underlying maps.

This instance can be helpful if you define `Sₘ := localization (algebra.algebra_map_submonoid S M)`,
however we will instead use the hypotheses `[algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ]` in lemmas
since the algebra structure may arise in different ways.
-/
noncomputable def localization_algebra : algebra Rₘ Sₘ :=
(map Sₘ (algebra_map R S)
    (show _ ≤ (algebra.algebra_map_submonoid S M).comap _, from M.le_comap_map)
  : Rₘ →+* Sₘ).to_algebra

end

section

variables [algebra Rₘ Sₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ]

variables (S Rₘ Sₘ)
include S

lemma is_localization.map_units_map_submonoid (y : M) : is_unit (algebra_map R Sₘ y) :=
begin
  rw is_scalar_tower.algebra_map_apply _ S,
  exact is_localization.map_units Sₘ ⟨algebra_map R S y, algebra.mem_algebra_map_submonoid_of_mem y⟩
end

@[simp] lemma is_localization.algebra_map_mk' (x : R) (y : M) :
  algebra_map Rₘ Sₘ (is_localization.mk' Rₘ x y) =
    is_localization.mk' Sₘ (algebra_map R S x) ⟨algebra_map R S y,
      algebra.mem_algebra_map_submonoid_of_mem y⟩ :=
begin
  rw [is_localization.eq_mk'_iff_mul_eq, subtype.coe_mk, ← is_scalar_tower.algebra_map_apply,
      ← is_scalar_tower.algebra_map_apply, is_scalar_tower.algebra_map_apply R Rₘ Sₘ,
      is_scalar_tower.algebra_map_apply R Rₘ Sₘ, ← _root_.map_mul,
      mul_comm, is_localization.mul_mk'_eq_mk'_of_mul],
  exact congr_arg (algebra_map Rₘ Sₘ) (is_localization.mk'_mul_cancel_left x y)
end

variables (M)

/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
-/
lemma is_localization.algebra_map_eq_map_map_submonoid :
  algebra_map Rₘ Sₘ = map Sₘ (algebra_map R S)
    (show _ ≤ (algebra.algebra_map_submonoid S M).comap _, from M.le_comap_map) :=
eq.symm $ is_localization.map_unique _ (algebra_map Rₘ Sₘ) (λ x,
  by rw [← is_scalar_tower.algebra_map_apply R S Sₘ, ← is_scalar_tower.algebra_map_apply R Rₘ Sₘ])

/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
-/
lemma is_localization.algebra_map_apply_eq_map_map_submonoid (x) :
  algebra_map Rₘ Sₘ x = map Sₘ (algebra_map R S)
    (show _ ≤ (algebra.algebra_map_submonoid S M).comap _, from M.le_comap_map)
    x :=
fun_like.congr_fun (is_localization.algebra_map_eq_map_map_submonoid _ _ _ _) x

variables {R}

lemma is_localization.lift_algebra_map_eq_algebra_map :
  @is_localization.lift R _ M Rₘ _ _ Sₘ _ _ (algebra_map R Sₘ)
    (is_localization.map_units_map_submonoid S Sₘ) =
    algebra_map Rₘ Sₘ :=
is_localization.lift_unique _ (λ x, (is_scalar_tower.algebra_map_apply _ _ _ _).symm)

end

variables (Rₘ Sₘ)

/-- Injectivity of the underlying `algebra_map` descends to the algebra induced by localization. -/
lemma localization_algebra_injective (hRS : function.injective (algebra_map R S)) :
  function.injective (@algebra_map Rₘ Sₘ _ _ (localization_algebra M S)) :=
is_localization.map_injective_of_injective M Rₘ Sₘ hRS

end algebra

end comm_ring

author: leanprover-community

repo: mathlib


text:
import data.complex.basic
import linear_algebra.sesquilinear_form
import linear_algebra.bilinear_form

/-
positive definite Hermitian sesquilinear forms do not seem to be in Lean yet
but sesquilinear forms are
-/

namespace complex

lemma eq_conj_iff_im_zero {z : ℂ} : conj z = z ↔ z.im = 0 :=
⟨λ h, eq_zero_of_neg_eq (congr_arg im h),
 λ h, ext rfl $ show -z.im = _, by rw h; exact neg_zero⟩

end complex
-- should be in mathlib
instance antihom_of_hom (R S : Type*) [comm_ring R] [comm_ring S] (f : R → S) [is_ring_hom f] : is_ring_anti_hom f :=
{ map_one := is_ring_hom.map_one f,
  map_mul := by {intros x y, show f (x * y) = _, rw [is_ring_hom.map_mul f, mul_comm], refl},
  map_add := λ _ _, is_ring_hom.map_add f }

noncomputable def complex.conj_anti_equiv : ring_anti_equiv ℂ ℂ := ⟨{to_fun := complex.conj, inv_fun := complex.conj,
  left_inv := complex.conj_conj, right_inv := complex.conj_conj}⟩

variables {α : Type*} {β : Type*} [ring α] [add_comm_group β] [module α β] {I : ring_anti_equiv α α} {S : sesq_form α β I}

namespace sesq_form

def is_Hermitian (S : sesq_form α β I) : Prop := ∀ (x y : β), I (S x y) = S y x

lemma Herm (HS : is_Hermitian S) (x y : β) : I (S x y) = S y x := HS x y

variables (V : Type*) [add_comm_group V] [module ℂ V]

lemma Herm_self_im_zero {S : sesq_form ℂ V complex.conj_anti_equiv} (HS : is_Hermitian S) (v : V) : (S v v).im = 0 :=
complex.eq_conj_iff_im_zero.1 $ Herm HS v v

-- only to be used for Hermitian forms
def is_positive_definite (S : sesq_form ℂ V complex.conj_anti_equiv) : Prop :=
(∀ v : V, (S v v).re ≥ 0) ∧ ∀ v : V, S v v = 0 → v = 0

end sesq_form

open sesq_form

noncomputable theory

variables (V : Type*) [add_comm_group V] [module ℂ V] (H : sesq_form ℂ V complex.conj_anti_equiv) (HS : is_Hermitian S)

--definition E.bilin (v w : V) : ℝ := (H v w).im
definition S.bilin (v w : V) : ℝ := (H v w).re

def module_of_module {R : Type*} [comm_ring R] {S : Type} [comm_ring S]
(f : ring_hom R S) {V : Type*} [add_comm_group V] [module S V] : module R V :=
{ smul := λ r v, (f r) • v,
  one_smul := λ v, show (f 1) • v = v, by rw f.map_one; exact one_smul S v,
  mul_smul := λ x y v, begin convert mul_smul (f x) (f y) v, rw ←f.map_mul, refl, end,
  smul_add := λ r, smul_add (f r),
  smul_zero := λ r, smul_zero (f r),
  add_smul := λ r s v, begin convert add_smul (f r) (f s) v, rw ←f.map_add, refl, end,
  zero_smul := λ v, begin dsimp, convert zero_smul S v, exact f.map_zero, end }

def real.to_complex.ring_hom : ring_hom ℝ ℂ := --by refine_struct {to_fun := coe}; simp #exit
{ to_fun := coe,
  map_one' := by simp,
  map_mul' := by simp,
  map_zero' := by simp,
  map_add' := by simp }

instance real.vector_space_of_complex.vecgtor_space: module ℝ V := module_of_module real.to_complex.ring_hom
def E : bilin_form ℝ V := { bilin := λ v w, (H v w).im,
  bilin_add_left := by simp [H.sesq_add_left],
  bilin_smul_left := _,
  bilin_add_right := _,
  bilin_smul_right := _ }

-- Def of E
-- E alternating
-- H(v,w)=E(iv,w)+iE(v,w)
-- H non-degenerate -> E non-degenerate

author: kbuzzard

repo: xena

save_path: github-repos/lean/kbuzzard-xena


text:
import GMLInit.Data.Index.Basic
import GMLInit.Data.Index.Bind
import GMLInit.Data.Index.Map
import GMLInit.Data.Index.Pi

protected abbrev List.arr {α β} (xs : List α) (ys : List β) : List (Index xs → β) :=
  xs.pi (β := fun _ => β) fun _ => ys

namespace Index
variable {α β} {xs : List α} {ys : List β}

def arr : (Index xs → Index ys) → Index (List.arr xs ys) := pi (β := fun _ => β) (f := fun _ => ys)

def unarr : Index (List.arr xs ys) → Index xs → Index ys := unpi (β := fun _ => β) (f := fun _ => ys)

theorem unarr_arr (h : Index xs → Index ys) : unarr (arr h) = h := by
  rw [arr, unarr, unpi_pi]

theorem arr_unarr (k : Index (List.arr xs ys)) : arr (unarr k) = k := by
  rw [arr, unarr, pi_unpi]

theorem arr_eq_iff_eq_unarr (h : Index xs → Index ys) (k : Index (List.arr xs ys)) : arr h = k ↔ h = unarr k := by
  constr
  · intro h; rw [←h, unarr_arr]
  · intro h; rw [h, arr_unarr]

theorem unarr_eq_iff_eq_arr (k : Index (List.arr xs ys)) (h : Index xs → Index ys) : unarr k = h ↔ k = arr h := by
  constr
  · intro h; rw [←h, arr_unarr]
  · intro h; rw [h, unarr_arr]

def arrEquiv (xs : List α) (ys : List β) : Equiv (Index xs → Index ys) (Index (List.arr xs ys)) where
  fwd := arr
  rev := unarr
  spec := by
    intros
    constr
    · intro | rfl => exact unarr_arr ..
    · intro | rfl => exact arr_unarr ..

end Index

author: fgdorais

repo: GMLInit

save_path: github-repos/lean/fgdorais-GMLInit


text:
import
field_theory.finite.polynomial
import data.nat.basic

open mv_polynomial
open polynomial

section polys

  set_option class.instance_max_depth 200

  parameters {α : Type} [field α] [fintype α] [decidable_eq α] [nonempty α]
  parameters {σ : Type*} [decidable_eq σ]
  parameters {τ : Type*} [decidable_eq τ]

  -- The vanishing lemma (Lemma 1.1 i in Tao's exposition on the Polynomial Method)
  lemma vanishing (d : ℕ) (p : polynomial α) (hp : nat_degree p ≤ d):
    -- For any single-variable polynomials whose degree is at most d
    -- and is not the zero polynomial
    p ≠ 0 →
    -- It has at most d roots
    p.roots.card ≤ d
      :=
  begin
    intros hp0,
    have hpd := polynomial.card_roots' hp0,
    transitivity (nat_degree p), exact hpd, exact hp,
  end

  -- The vanishing lemma rewritten (Lemma 1.1 i in Tao's exposition on the Polynomial Method)
  lemma vanishing_contrapos (d : ℕ) (p : polynomial α) (hp : nat_degree p ≤ d):
    -- For any single-variable polynomials whose degree is at most d
     -- If it has more than d roots
    p.roots.card > d →
    -- It is the zero polynomial
    p = 0
      :=
  begin
    contrapose, simp, apply vanishing, exact hp,
  end

  --The vanishing lemma (applied specifically to finsets)
  lemma vanishing' (d : ℕ) (p : polynomial α) (hp : nat_degree p ≤ d):
    -- If it reaches zero on more than d points of some set
    ∀ (S: finset α),
    let ZPS : multiset α := (multiset.filter (λ x, x ∈ S) p.roots) in
                                --p.roots ∩ S.val in -- we can remove duplicates from the finset, because a finset intersected with a multiset is a finset
                                -- (finset.filter (λ x, x ∈ S) p.roots.to_finset) in
                                --finset.univ.filter (λ x, x ∈ p.roots ∧ x ∈ S) in
                                --let ZPS : finset α:= finset.univ.filter (λ x, polynomial.eval x p = 0 ∧ x ∈ S) in
      ZPS.card > d →
      -- Then it vanishes on every point of that set
      --ZPS.card = S.card
      --ZPS = S.val
      ∀ (x : α), polynomial.eval x p = 0
      :=
  begin
    intros S ZPS hZPS,
    have hr := multiset.filter_le (λ x, x ∈ S) p.roots,
    replace hr := multiset.card_le_of_le hr,
    have hpd : p.roots.card > d := by apply lt_of_lt_of_le hZPS hr,
    -- It suffices to prove that p is the zero polynomial
    suffices : p = 0, {
      rw this, simp,
    },
    apply vanishing_contrapos d p hp, exact hpd,
  end

-- The vanishing lemma for multivariate polynomials, which requires the degree of the poly be less than the cardinality of the field
-- A variant of Lemma 1.2 in Tao (Schwartz-Zippel lemma).
  lemma vanishing_mv (n d : ℕ) (hn : n ≥ 1) (p : mv_polynomial (fin n) α) (hp : total_degree p ≤ d) (hd : d < fintype.card α):
    -- If a d-degree polynomial is zero on all the points of a finite field
    (∀ x, mv_polynomial.eval x p = 0 )→
    -- Then it is the zero polynomial
    p = 0
      :=
  begin
    intros hZero,

    --Polynomials where the max degree is < |F| means it can't eval 0 everywhere
    apply mv_polynomial.eq_zero_of_eval_eq_zero (fin n) α p _,

    -- And now we want to prove that the max degree of each variable < |F|
    swap, exact hZero, clear hZero,
    have hpd := lt_of_le_of_lt hp hd, clear hp hd,
    rw mv_polynomial.mem_restrict_degree_iff_sup, intros i,
    apply nat.le_pred_of_lt,

    -- So first we prove that the max degree of each variable <= total degree
    -- Note: mv_polynomial.degree_of n p = multiset.count n p.degrees
    have hp : mv_polynomial.degree_of i p ≤ p.total_degree, {

      -- Rewrite to an expression involving supremums and sums
      rw total_degree_eq,
      rw degree_of, rw degrees,
      rw multiset.count_sup,
      simp only [finsupp.count_to_multiset, finsupp.card_to_multiset],

      -- A positive element <= sum of positive elements
      apply finset.sup_mono_fun,
      intros b hb,
      rw finsupp.sum_fintype, simp,
      apply finset.single_le_sum,
        intros i hi, simp,
        simp,
      simp,

    },

    -- And then since total degree < |F|, we have that the max degree of each variable < |F|
    exact lt_of_le_of_lt hp hpd,
  end

parameters {n : ℕ} (V : subspace α (mv_polynomial (fin n) α)) (A : finset (fin n → α))

def zero_set : set (mv_polynomial (fin n) α) := {p ∈ V.carrier | ∀ a ∈ A, mv_polynomial.eval a p = 0}

def zero_set_subspace : subspace α (mv_polynomial (fin n) α) :=
{ carrier := zero_set,
  zero_mem' := ⟨submodule.zero_mem _, by simp⟩,
  add_mem' := λ _ _ hx hy, ⟨submodule.add_mem _ hx.1 hy.1, λ _ hp, by simp [hx.2 _ hp, hy.2 _ hp]⟩,
  smul_mem' := λ _ _ hp, ⟨submodule.smul_mem _ _ hp.1, λ _ hx, by simp [hp.2 _ hx]⟩ }

  -- The interpolation lemma (Lemma 1.1(ii) in Tao's exposition on the Polynomial Method)
  lemma interpolation':
    /- Let n,d ≥ 1 be integers  -/
    ∀ n d: ℕ, n ≥ 1 → d ≥ 1 →
    /- Then for any set E, where E is a subset of vector space F...-/
    ∀ (E: finset α),
    /- ...such that the size of E is at least d+n choose n... -/
    E.card < d →
    /- ...there exists a nonzero polynomial p of degree at most d ... -/
    ∃ p : polynomial α, nat_degree (p) ≤ d ∧ p ≠ 0 ∧
    /- ...such that the poly evaluates to zero on all points of E. -/
    /- That is, filtering the set by where the polynomial is zero and E is the same as just filtering by E-/
    --let ZP := finset.univ.filter (λ x, mv_polynomial.eval x p = 0) in E ⊆ ZP
    --∀ e ∈ E , mv_polynomial.eval e p = 0
    finset.filter (λ (a : α), p.eval a = 0 ∧ a ∈ E) = finset.filter (λ (a : α), a ∈ E)
     :=

  begin
    intros n d hn hd E hE,
    -- The vector space of d-degree polys has d+1 dimensions
    --have vs :=
    -- The vector space of functions that take you from E to F has d dim
    --      Since you can write a function that takes in d variables as a d-dim tuple
    -- And so the function that takes you from one vector space to the next has a nontrivial kernel
    -- So the polynomial exists in that nontrivial kernel (a nontrivial d-dim function that takes you from E to all 0s).

    -- probably can use Lemma 9.2. or lemma_9_2_pre in section_9
    -- lemma lemma_9_2_pre : (vector_space.dim α zero_set_subspace) + A.card ≥ (vector_space.dim α V) :=

    sorry,
  end

  -- The interpolation lemma (Lemma 1.4 in Tao's exposition on the Polynomial Method)
  lemma interpolation:
    /- Let n,d ≥ 1 be integers  -/
    ∀ n d: ℕ, n ≥ 1 → d ≥ 1 →
    /- Then for any set E, where E is a subset of vector space F^n...-/
    ∀ (E: finset (fin n → α)),
    /- ...such that the size of E is at least d+n choose n... -/
    E.card < (d+n).choose(n) →
    /- ...there exists a nonzero polynomial p of degree at most d ... -/
    ∃ p : mv_polynomial (fin n) α, total_degree (p) ≤ d ∧ p ≠ 0 ∧
    /- ...such that the poly evaluates to zero on all points of E. -/
    /- That is, filtering the set by where the polynomial is zero and E is the same as just filtering by E-/
    --let ZP := finset.univ.filter (λ x, mv_polynomial.eval x p = 0) in E ⊆ ZP
    --∀ e ∈ E , mv_polynomial.eval e p = 0
    finset.filter (λ (a : fin n → α), ⇑(eval a) p = 0 ∧ a ∈ E) = finset.filter (λ (a : fin n → α), a ∈ E)
     :=

  begin
    intros n d hn hd E hE,
    sorry,
  end

  -- def fin_eq_unit: (fin 1) ≃ unit :=  -- "unit" means "punit.{0}"
  -- {
  --   to_fun := (λ x, punit.star),-- or,  begin intro f, apply punit.star, end,
  --   inv_fun := λ u: unit, {
  --       val := 0,
  --       is_lt := nat.zero_lt_succ 0, -- proof that 0 < 1
  --     },
  --   left_inv := begin --a proof that  inv_fun (to_fun x) = x
  --       intro x, simp, cases x, cases x_is_lt,
  --         refl,
  --         exfalso, apply nat.not_succ_le_zero x_val, exact x_is_lt_a,
  --     end,
  --   right_inv := begin  --a proof that  to_fun (inv_fun x) = x
  --       intro u, cases u, simp,
  --     end
  -- }

  -- def transform: mv_polynomial (fin 1) α → polynomial α :=
  --   begin

  --     intro p,
  --     have eq := punit_alg_equiv α, have eq_imp := eq.to_fun, apply eq_imp,
  --     have eq2 := rename_equiv α fin_eq_unit, have eq2_imp := eq2.to_fun, apply eq2_imp,
  --     exact p,
  --   end

    -- A line in a finite field passes through the point "u" and extends in direction "v"
  def line  (n: ℕ)
    (u : fin n → α)  (v : fin n → α)
    : finset (fin n → α) :=
    finset.univ.filter (λ k, (∃ t: α, k = u + t•v ))

  -- The rigidity lemma (Lemma 1.6 in Tao's exposition on the Polynomial Method)
  lemma rigidity:
    /- Let α be a finite field (call it F).-/
    /- Let n,d ≥ 1 be integers  -/
    ∀ n d: ℕ,
    n ≥ 1 → d ≥ 1 →
    /- For all polynomials p of degree at most d ... -/
    ∀ p : mv_polynomial (fin n) α, total_degree (p) ≤ d  →
    /- And for all lines in the field ... -/
    ∀ (u v : fin n → α),
    let L := line n u v in
    /- If the polynomial is zero along more than d points of the line -/
    let ZPL : finset (fin n → α):= (line n u v).filter (λ x, mv_polynomial.eval x p = 0) in
      (ZPL.card > d) →
    /- Then it is zero along the entire line -/
      --(ZPL.card = L.card)
      ∀ x ∈ line n u v, mv_polynomial.eval x p = 0
      :=
  begin
    intros n d hn hd p hp u v L ZPL hZPL x hxL,
                                                  -- u_i + X_0^1 * v_i    (and note we refer to "X_0" as "t")
    let q : (fin n) →  mv_polynomial (fin 1) α := (λi, (mv_polynomial.C (u i)) + (monomial (finsupp.single 0 1) (v i))),

    -- would probably use mv_polynomial.map_mv_polynomial_eq_eval₂

    -- deterministic timeout!
    have f := comp p q,

    --have f := (λ t : α, comp p q),
    -- have h := rename g p,
    -- have j := transform h,

    -- Show that the one-dimensional polynomial j(t) vanishes on the set of all t
    -- have T : finset α := finset.univ.filter (λ x, true), -- finset.univ.filter (λ x, x ∈ L), --
    -- have h0 := vanishing d j hj T,

    -- Which means the set of all ZPL is also all zero.

    sorry

  -- have f := (λ t : ℕ, p.eval (u + t•v)),
    -- have g : polynomial α := finsupp.mk _ f _,

    -- have f := (λ t : α, p.eval (u + t•v)),
    -- have g : polynomial α := finsupp.mk _ f _,

    -- have f : polynomial α := ↑(λ t : α, p.eval (u + t•v)),
    -- have f : polynomial α := ↑(λ t : α, p.eval (u) + t•p.eval(v)),

    --apply vanishing d p hp L, -- Invoke the vanishing lemma to show it suffices to prove that |ZPL| > d
    --exact hZPL,-- Use our assumption that |ZPL| > d
  end

-- The finite field nikodym theorem (the contradictory statement that implies false)
theorem nikodym_contra:
    /- Let α be a finite field (call it F).-/
    /- Let n,d ≥ 1 be integers  -/
    ∀ n d: ℕ,
    n ≥ 1 → d ≥ 1 →
     /- with d < |F|. -/
    (d < fintype.card α) →
    /- Then for any set E, where E is a subset of vector space F^n...-/
    ∀ (E: finset (fin n → α)),

    /- ...and E has that property that -/
    (
      /- for every point x ∈ F^n-/
      ∀ (x : fin n → α),
      /- you can find a line (that goes through x in the direction of any v ∈ F^n) -/
      ∃ (v : fin n → α),
      --let L := line n x v in
      /- that intersects E at more than d points...-/
        --(E ∩ line n x v).card > d
        ((line n x v).filter (λ e, e ∈ E)).card > d
    ) →
    /- ...then the size of E must be at least d+n choose n. -/
      E.card < (d+n).choose(n) → false :=
begin
  intros n d hn hd hd2 E hl hE,

  -- We know by interpolation that there exists a nonzero degree d poly that is 0 on all of E
  have hp := interpolation n d hn hd E hE,
  rcases hp with ⟨p, hpd, hp0, hpE⟩,

  -- Make the contradiction to prove that p=0
  apply hp0,

  -- To prove p=0, it suffices to prove that it evaluates to 0 everywhere
  suffices : ∀ x : fin n → α, mv_polynomial.eval x p = 0, {
    exact vanishing_mv n d hn p hpd hd2 this,
  },

  intros x,

  -- Show that for every point x, there is a line that goes through x that intersects E (which is in the zero set) at more than d places...
  specialize hl x, cases hl with v hl,

  -- And also use rigidity to show that if we can prove the line is 0 at more than d places, then it is zero everywhere
  have hr := rigidity n d hn hd, specialize hr p hpd x v, apply hr,

  -- Proving the line is 0 at more than d places...
  {
    -- to prove |ZP ∩ line | > d, it suffices to prove |E ∩ ZP ∩ line  | > d
    have hzp := finset.card_filter_le  (finset.filter (λ (x : fin n → α), ⇑(eval x) p = 0) (line n x v)) (λ x, x ∈ E),
    apply gt_of_ge_of_gt hzp,
    -- show |E ∩ ZP ∩ line| is the same as |E ∩ line|
    rw finset.filter_filter,
    rw hpE,
    -- then use hl which says |E ∩ line| > d
    apply hl,
  },

  -- Proving every x is on the line
  {rw line, simp},
end

-- The finite field nikodym theorem (proof by contradiction)
theorem nikodym:
    /- Let α be a finite field (call it F).-/
    /- Let n,d ≥ 1 be integers  -/
    ∀ n d: ℕ,
    n ≥ 1 → d ≥ 1 →
     /- with d < |F|. -/
    (d < fintype.card α) →
    /- Then for any set E, where E is a subset of vector space F^n...-/
    ∀ (E: finset (fin n → α)),

    /- ...and E has that property that -/
    (
      /- for every point x ∈ F^n-/
      ∀ (x : fin n → α),
      /- you can find a line (that goes through x in the direction of any v ∈ F^n) -/
      ∃ (v : fin n → α),
      let L := line n x v in
      /- that intersects E at more than d points...-/
        --(E ∩ L).card > d
        ((line n x v).filter (λ e, e ∈ E)).card > d
    ) →
    /- ...then the size of E must be at least d+n choose n. -/
      E.card ≥ (d+n).choose(n) :=
begin
  intros  n d hn hd hd2 E hl,
  -- To prove P, we prove ¬ P → false (which is the same as ¬¬ P)
  -- That is, to prove hE, we prove ¬ hE → false
  have nhEimpfalse: ( (E.card < (d+n).choose(n)) → false) := nikodym_contra n d hn hd hd2 E hl,
  -- Then we bring our current goal hE into the hypothesis as ¬hE
  by_contra nhE,
  -- Then we make it clear that nhE and the hypothesis of nhE → false are the same
  simp at nhE nhEimpfalse,
  -- Then since nhE -> false, and nhE, we have a contradiction
  contradiction,
end

end polys

author: anshula

repo: nikodym-lean

save_path: github-repos/lean/anshula-nikodym-lean