text:
import matrix
import matrix_inner_product
import common_lemmas
import linear_algebra.nonsingular_inverse

open_locale big_operators
open matrix
open Matrix

------------------------------------------------------------------------------
-- ℝ lemmas

lemma real.lt_of_lt_pow_two {a b : ℝ} : a^2 < b^2 → 0 ≤ a → 0 ≤ b → a < b
:= begin
    intros h an bn,
    rw <- real.sqrt_mul_self an,
    rw <- real.sqrt_mul_self bn,
    iterate 2 { rw pow_two at h },
    apply (real.sqrt_lt _).mpr, assumption,
    rw <- pow_two; apply pow_two_nonneg,
end

lemma real.add_squares_le_square_add (x y : ℝ): 0 ≤ x → 0 ≤ y → x^2 + y^2 ≤ (x + y)^2
:= begin
    intros xn yn,
    repeat { rw pow_two },
    repeat { rw mul_add },
    repeat { rw add_mul },
    have f1: x * x + y * x + (x * y + y * y) = (x * x + y * y) + (x * y + y * x), {
        ring,
    },
    rw f1,
    simp [add_nonneg, mul_nonneg, *],
end

------------------------------------------------------------------------------
-- (pure) ℂ lemmas

@[simp]
lemma complex.abs_nonneg' (c : ℂ) : 0 ≤ c.abs := by apply complex.abs_nonneg

@[simp]
lemma complex.norm_sq_nonneg' (c : ℂ) : 0 ≤ complex.norm_sq c := by apply complex.norm_sq_nonneg

@[simp]
lemma complex.conj_mul (c : ℂ) : c.conj * c = c.norm_sq
:= begin
    rw mul_comm,
    apply complex.mul_conj,
end

@[simp]
lemma complex.conj_mul' (c : ℂ) : c * c.conj = c.norm_sq
:= begin
    apply complex.mul_conj,
end

lemma complex.re_div_eq_div_re (a b : ℂ) : a.im = 0 → b.im = 0 → (a / b).re = a.re / b.re
:= begin
    intros ap bp,
    have f1: a = a.re, {
        cases a,
        cases b,
        cases ap,
        cases bp,
        simp at *,
        refl,
    },
    have f2: b = b.re, {
        cases a,
        cases b,
        cases ap,
        cases bp,
        simp at *,
        refl,
    },
    have f3: (a / b) = (a.re / b.re), {
        rw f1,
        rw f2,
        simp,
    },
    rw f3,
    norm_cast,
end

lemma complex.re_add_eq_add_re (a b : ℂ) : (a + b).re = a.re + b.re
:= begin
    exact rfl,
end

----------------------------------------------------------------------------------------
-- ℂ + is_R_or_C

lemma complex.mul_conj_abs_square (c : ℂ) : (c†) * c = |c| ^ 2
:= begin
    simp,
    apply_mod_cast complex.norm_sq_eq_abs,
end

lemma complex.abs_of_real' (x : ℝ) : |x| = |(x : ℂ)|
:= begin
    refl,
end

lemma complex.re_conj_eq_re (c : ℂ): (c†).re = c.re
:= begin
    refl,
end

lemma complex.conj_sum_dist {n} (f : fin n → ℂ)
        : (∑ k, (f k)†) = (∑ k, (f k))†
:= begin
    exact finset.univ.sum_hom complex.conj,
end

@[simp]
lemma complex.norm_sq_eq_mul_abs (c : ℂ) : |c| * |c| = c.norm_sq
:= begin
    rw complex.norm_sq_eq_abs,
    rw pow_two, simp,
end

----------------------------------------------------------------------------------------
-- matrix type-cast helpers

section matrix_cast

variables {α : Type} [semiring α]
variables {m n : Type} [fintype m] [fintype n]
variables {m' n' : Type} [fintype m'] [fintype n']

variables (s : α) (M : matrix m n α) (N : matrix m n α)

lemma matrix_congr (h1: m = m') (h2: n = n') : matrix m n α = matrix m' n' α
:= begin
    congr; assumption,
end

lemma push_cast_matrix_smul (h1: m = m') (h2: n = n')
        : cast (matrix_congr h1 h2) (s • M) = s • (cast (matrix_congr h1 h2) M)
:= begin
    apply cast_eq_of_heq,
    tactic.unfreeze_local_instances,
    cases h1,
    cases h2,
    congr' 1; try {assumption},
end

lemma push_cast_matrix_add (h1: m = m') (h2: n = n')
        : cast (matrix_congr h1 h2) (M + N) = (cast (matrix_congr h1 h2) M) + (cast (matrix_congr h1 h2) N)
:= begin
    apply cast_eq_of_heq,
    tactic.unfreeze_local_instances,
    cases h1,
    cases h2,
    congr; try {assumption},
end

end matrix_cast

section matrix_cast_apply

variables {α : Type}
variables {m n m' n': Type} [fintype m] [fintype n] [fintype m'] [fintype n']
variables (A : matrix m n α) (B : matrix m' n' α)

lemma A_eq (m_eq: m = m') (n_eq: n = n') : matrix m n α = matrix m' n' α
:= begin
    congr; assumption,
end

-- for easier pattern matching with matrix
lemma matrix_cast_apply (m_eq: m = m') (n_eq: n = n') (i' : m') (j' : n')
    : (cast (A_eq m_eq n_eq) A) i' j' = A (cast m_eq.symm i') (cast n_eq.symm j')
:= begin
    apply cast_apply2,
end

end matrix_cast_apply

----------------------------------------------------------------------------------------
-- Matrix lemmas

section matrix

variables {m n o : ℕ}
variables {A : Matrix m n} {B : Matrix n o}
variables {s : Vector n}

@[simp]
lemma Matrix_zero_neq_one {n} : 0 ≠ (I (n+1))
:= begin
    intro h,
    have c3: (1 : ℂ) = 0, {
        calc (1 : ℂ) = (I (n+1)) 0 0 : by simp
              ... = (0 : Square (n+1)) 0 0 : by {rw h}
              ... = 0 : by simp,
    },
    have c4: (1 : ℝ) = 0, {
        apply_mod_cast c3,
    },
    linarith,
end

lemma Matrix_nonzero_has_nonzero_val : A ≠ 0 → (∃ i j, A i j ≠ 0)
:= begin
    contrapose!, intros h,
    apply matrix.ext, intros i j,
    apply h,
end

lemma Vector_nonzero_has_nonzero_val : s ≠ 0 → (∃ i, s i 0 ≠ 0)
:= begin
    contrapose!, intros h,
    apply matrix.ext, intros i j,
    have j0 : j = 0, cases j, simp, cases j0, clear j0, simp,
    apply h,
end

-- Special case of 1 × 1 matrix.
lemma matrix_mul_cancel_left_square_one {n} {x : Vector n} {y z : Square 1} : x ⬝ y = x ⬝ z → x ≠ 0 → y = z
:= begin
    intros h xn,
    apply matrix.ext, intros i j,
    rw <- matrix.ext_iff at h,

    cases (Vector_nonzero_has_nonzero_val xn) with k kp,

    specialize h k j,

    iterate 2 {
        rw matrix.mul_apply at h,
        rw finset.sum_fin_eq_sum_range at h,
        rw finset.sum_range_one at h,
        rw dif_pos at h; try {solve1 {linarith}}, simp at h,
    },

    have i0 : i = 0, cases i; simp, cases i0; clear i0,
    have j0 : j = 0, cases j; simp, cases j0; clear j0,
    simp at *,

    cases h, {
        assumption,
    }, {
        exfalso,
        apply kp; assumption,
    }
end

-- Special case of 1 × 1 matrix.
lemma matrix_mul_square_one {x y : Square 1} {i j : fin 1}: (x ⬝ y) i j = x i j * y i j
:= begin
    unfold matrix.mul matrix.dot_product,
    have i0 : i = 0, cases i; simp, cases i0; clear i0,
    have j0 : j = 0, cases j; simp, cases j0; clear j0,
    rw finset.sum_fin_eq_sum_range,
    rw finset.sum_range_one,
    rw dif_pos; simp,
end

-- Special case of 1 × 1 matrix.
lemma matrix_mul_comm_square_one {x y : Square 1} : x ⬝ y = y ⬝ x
:= begin
    apply matrix.ext, intros i j,
    iterate 2 { rw matrix_mul_square_one },
    ring,
end

-- Special case of 1 × 1 matrix.
@[simp]
lemma id_one_apply {x y : fin 1} : (I 1) x y = 1
:= begin
    have xp: x = 0, by simp,
    have yp: y = 0, by simp,
    cases xp,
    cases yp,
    simp,
end

-- Slightly relaxed version of matrix.smul_apply for easier matching.
-- Note the scalar type is ℝ, not ℂ.
lemma Matrix.real_smul_apply {a : ℝ} {i : fin m} {j : fin n}
        : (a • A) i j = a * A i j := rfl

-- Slightly relaxed version of matrix.mul_smul for easier matching.
-- Note the scalar type is ℝ, not ℂ.
lemma Matrix.mul_real_smul {a : ℝ} : A ⬝ (a • B) = a • (A ⬝ B)
:= by {apply matrix.mul_smul,}

end matrix

----------------------------------------------------------------------------------------
-- adjoint lemmas

@[simp]
theorem adjoint_zero {m n} : (0 : Matrix m n)† = 0
:= begin
    apply matrix.ext, intros i j,
    unfold adjoint, simp,
end

@[simp]
theorem adjoint_one {n} : (1 : Matrix n n)† = 1
:= begin
    apply matrix.ext,
    intros i j,
    unfold adjoint,
    by_cases i = j, {
        simp [h],
    }, {
        rw matrix.one_apply_ne h,
        have h' : ¬ j = i, {
            cc,
        },
        rw matrix.one_apply_ne h',
        simp,
    }
end

section adjoint

variables {m n : ℕ}
variables (x y : Matrix m n)

@[simp]
theorem adjoint_involutive : x†† = x
:= begin
    apply matrix.ext,
    intros i j,
    unfold adjoint,
    simp,
end

theorem adjoint_inj : (x†) = (y†) → x = y
:= begin
    intros h,
    apply matrix.ext, intros i j,
    rw <- matrix.ext_iff at h,
    specialize h j i,
    unfold adjoint at h,
    apply complex.conj_inj.mp h,
end

lemma adjoint_add : ((x + y)†) = (x†) + (y†)
:= begin
    apply matrix.ext, intros i j, simp,
    unfold adjoint, simp,
end

lemma adjoint_neg (x : Matrix m n): (-x)† = -(x†)
:= begin
    apply matrix.ext, intros i j,
    simp, unfold adjoint, simp,
end

lemma adjoint_smul (s : ℂ) : (s • x)† = (s†) • (x†)
:= begin
    apply matrix.ext, intros i j,
    unfold has_scalar.smul,
    unfold adjoint,
    simp,
end

lemma adjoint_apply (x : Matrix m n) (i : fin n) (j : fin m) : (x†) i j = ((x j i)†)
:= begin
    unfold adjoint,
end

end adjoint

---------------------------------------------------------------------------------------------
-- Adjoint + mul lemmas

section adjoint_mul

variables {m n o : ℕ}
variable (A : Matrix m n)
variable (B : Matrix n o)

lemma conj_mul_eq_dot_product (i : fin m) (j : fin o)
        : ((A ⬝ B) i j)† = dot_product (λ k, (B k j)†)
                                       (λ k, (A i k)†)
:= begin
    unfold matrix.dot_product,
    unfold matrix.mul,
    unfold matrix.dot_product,
    rw <- complex.conj_sum_dist, {
        congr,
        refine funext _,
        intro k,
        simp,
        ring,
    },
end

theorem adjoint_mul : (A ⬝ B)† = (B†) ⬝ (A†)
:= begin
    apply matrix.ext,
    intros j i,
    apply conj_mul_eq_dot_product,
end

end adjoint_mul

----------------------------------------------------------------------------------------
-- Vector + adjoint lemmas

section vector_adjoint

variables {n : ℕ} (s : Vector n)

lemma dot_adjoint_eq_sum_mul_conj
            : dot_product (s† 0) (λ j, s j 0)
            = ∑ j, ((s j 0)†) * (s j 0)
:= begin
    congr,
end

lemma dot_adjoint_eq_sum_squre
            : dot_product (s† 0) (λ j, s j 0)
            = ∑ j, |s j 0| ^ 2
:= begin
    rw dot_adjoint_eq_sum_mul_conj,
    congr,
    apply funext,
    intros x,
    apply complex.mul_conj_abs_square,
end

example : (((s†) ⬝ s) 0 0) = ((∑ i, |s i 0| ^ 2) : ℂ)
:= begin
    apply dot_adjoint_eq_sum_squre,
end

@[simp]
lemma sum_square_one_if_mul_adjoint_one : ((s†) ⬝ s) = 1 → (∑ i, |s i 0| ^ 2) = 1
:= begin
    intros h,
    unfold matrix.mul at h,
    rw <- matrix.ext_iff at h,
    specialize h 0 0,
    rw dot_adjoint_eq_sum_squre at h,
    simp at h,
    apply_mod_cast h,
end

lemma mul_adjoint_one_if_sum_square_one : (∑ i, |s i 0| ^ 2) = 1 → ((s†) ⬝ s) = 1
:= begin
    intros h,
    apply matrix.ext,
    intros i j,
    have i_eq : i = 0, {
        cases i with i ip; simp,
    },
    have j_eq : j = 0, {
        cases i with i ip; simp,
    },
    cases i_eq,
    cases j_eq,
    simp,
    unfold matrix.mul,
    rw dot_adjoint_eq_sum_squre,
    apply_mod_cast h,
end

end vector_adjoint

----------------------------------------------------------------------------------------
-- unit lemmas

lemma unfold_unit {n} {s : Vector n} : s.unit -> (s†) ⬝ s = 1 := by {tautology}

lemma unit_nonzero {n : ℕ} {s : Vector n} : s.unit → s ≠ 0
:= begin
    contrapose!, intros h c,

    rw <- matrix.ext_iff at h, simp at h,

    unfold matrix.unit at c,
    rw <- matrix.ext_iff at c,
    specialize (c 0 0),
    unfold matrix.mul matrix.dot_product at c, simp at c,

    have h1: ∑ (i : fin n), s† 0 i * s i 0 = 0, {
        apply finset.sum_eq_zero, intros i ip,
        rw h, simp,
    },

    have c2: (0 : ℂ) = 1, {
        rw <- h1,
        rw <- c,
    },
    norm_num at c2,
end

----------------------------------------------------------------------------------------
-- std_basis lemmas

section std_basis

variables {m : Type*} [fintype m]
variables [decidable_eq m]

@[simp]
lemma std_basis_eq_zero {n : m} : ∀ {j i}, ¬ j = n → std_basis n j i = 0
:= begin
    intros j i h,
    unfold std_basis,
    exact if_neg h,
end

@[simp]
lemma std_basis_eq_one {n : m} : ∀ {j i}, j = n → std_basis n j i = 1
:= begin
    intros j i h,
    rw h,
    unfold std_basis,
    simp,
end

variables {n : ℕ} {i j : fin n}

@[simp]
theorem std_basis_unit : (std_basis i).unit
:= begin
    apply mul_adjoint_one_if_sum_square_one,
    rw finset.sum_eq_single i, {
        simp,
    }, {
        intros b bp h,
        rw std_basis_eq_zero h; simp,
    }, {
        intro h,
        exfalso,
        apply h; simp,
    }
end

@[simp]
lemma std_basis_adjoint_apply {s : fin n} : ∀ x, ((std_basis s)†) x i = (std_basis s) i x
:= begin
    unfold Matrix.adjoint,
    intros x,
    by_cases c : i = s, {
        rw std_basis_eq_one c, simp,
    }, {
        rw std_basis_eq_zero c, simp,
    }
end

@[simp]
lemma std_basis_inner_product : ((std_basis i)†) ⬝ (std_basis i) = 1
:= begin
    apply std_basis_unit,
end

lemma std_basis_inner_product_eq_zero : ¬ i = j → ((std_basis i)†) ⬝ (std_basis j) = 0
:= begin
    intros h,

    apply matrix.ext, intros v w,
    unfold matrix.mul matrix.dot_product Matrix.adjoint,
    have v0 : v = 0, by simp,
    have w0 : w = 0, by simp,
    rw v0, rw w0, simp,

    rw finset.sum_eq_single i; simp [std_basis_eq_zero h],

    intros b h',
    left,
    rw std_basis_eq_zero h',
end

@[simp]
lemma inner_product_std_basis_cancel_left {s : Vector n}
        : ((std_basis i)† ⬝ s) 0 0 = s i 0
:= begin
    unfold matrix.mul adjoint std_basis,
    unfold matrix.dot_product,
    rw finset.sum_eq_single i; simp; cc,
end

@[simp]
lemma adjoint_inner_product_std_basis_cancel_left {s : Vector n}
        : ((std_basis i)† ⬝ s)† 0 0 = (s i 0)†
:= begin
    unfold matrix.mul adjoint std_basis,
    unfold matrix.dot_product,
    rw finset.sum_eq_single i; simp; cc,
end

end std_basis

----------------------------------------------------------------------------------------
-- lemmas about matrix_std_basis from mathlib

section matrix_std_basis

variables {m n: Type*} [fintype m] [fintype n]
variables [decidable_eq m] [decidable_eq n]
variables {α : Type} [semiring α]

@[simp]
lemma std_basis_matrix_eq_given {i' : m} {j' : n} {v : α}
        : ∀ {i j}, i = i' ∧ j = j' → std_basis_matrix i' j' v i j = v
:= begin
    intros i j h,
    cases h with h1 h2,
    rw h1,
    rw h2,
    unfold std_basis_matrix,
    simp,
end

lemma std_basis_matrix_eq_zero {i' : m} {j' : n} {v : α}
        : ∀ {i j}, ¬ i = i' ∨ ¬ j = j' → std_basis_matrix i' j' v i j = 0
:= begin
    intros i j h,
    unfold std_basis_matrix,
    rwa if_neg,
    by_contradiction c,
    cases c with c1 c2,
    cases h, {
        apply h; assumption,
    }, {
        apply h; assumption,
    }
end

lemma std_basis_eq_std_basis_matrix {n : m}
        : std_basis n = matrix.std_basis_matrix n 0 1
:= begin
    apply matrix.ext,
    intros i j,
    have jp : j = 0, {
        cases j with j jp,
        simp,
    },
    cases jp,
    simp,
    by_cases i = n, {
        cases h,
        simp,
    }, {
        rw std_basis_eq_zero h,
        rw std_basis_matrix_eq_zero,
        left, assumption,
    }
end

end matrix_std_basis

----------------------------------------------------------------------------------------
-- state vector decomposition into standard basis vectors

theorem Vector_decomposition {n} (s : Vector n) : s = ∑ i, s i 0 • std_basis i
:= begin
    apply matrix.ext,
    intros i j,
    cases j with j jp,
    have jeq: j = 0, {
        linarith,
    },
    cases jeq,
    simp,
    rw finset.sum_eq_single i, {
        simp,
    }, {
        intros b bp h,
        rw std_basis_eq_zero h.symm; simp,
    }, {
        intros c,
        exfalso,
        apply c; simp,
    }
end

------------------------------------------------------------------------------
-- kron_loc lemmas

section kron_loc

variables {n m : ℕ}

@[simp]
lemma kron_loc_composition (x : fin (n*m)): kron_loc (kron_div x) (kron_mod x) = x
:= begin
    unfold kron_div kron_mod kron_loc,
    cases x with x xp,
    simp,
    have f1: 0 < m, {
        cases m, {
            exfalso,
            simp at xp,
            assumption,
        }, {
            simp,
        }
    },
    symmetry,
    apply nat_decompose_mul_add, assumption,
end

@[simp]
lemma kron_div_kron_loc {k : fin n} {j : fin m} : kron_div (kron_loc k j) = k
:= begin
    unfold kron_div kron_loc, simp,
    cases k with k kp,
    cases j with j jp,
    simp,
    rw nat_add_mul_left_div_left, {
        rw nat.div_eq_zero; simp *,
    }, {
        linarith,
    }
end

@[simp]
lemma kron_mod_kron_loc {k : fin n} {j : fin m} : kron_mod (kron_loc k j) = j
:= begin
    unfold kron_mod kron_loc, simp,
    cases k with k kp,
    cases j with j jp,
    simp,
    rw nat_add_mul_left_mod_left, {
        rw nat.mod_eq_of_lt; assumption,
    }
end

lemma kron_loc_inj (a b : fin n) (c d : fin m) : kron_loc a c = kron_loc b d → a = b ∧ c = d
:= begin
    intros h,
    cases a with a ap,
    cases b with b bp,
    cases c with c cp,
    cases d with d dp,
    simp,
    unfold kron_loc at h, simp at h,
    apply add_mul_congr; try {assumption},
end

lemma kron_loc_inj_iff (a b : fin n) (c d : fin m) : kron_loc a c = kron_loc b d ↔ a = b ∧ c = d
:= begin
    split, {
        apply kron_loc_inj,
    }, {
        intros h, rcases h with ⟨h1, h2⟩,
        cases h1, cases h2, clear h1 h2, refl,
    }
end

end kron_loc

---------------------------------------------------------------------------------------------
-- kron lemmas

section kron

variables {m n p q : ℕ}
variables (A : Matrix m n) (B : Matrix p q)

theorem adjoint_kron : (A ⊗ B)† = (A†) ⊗ (B†)
:= begin
    apply matrix.ext,
    intros j i,
    unfold kron,
    unfold Matrix.adjoint,
    simp,
end

theorem mul_to_kron (r : fin m) (s : fin n) (v : fin p) (w : fin q)
        : A r s * B v w = (A ⊗ B) (kron_loc r v) (kron_loc s w)
:= begin
    unfold kron,
    unfold kron_loc,
    unfold kron_div kron_mod,
    cases r with r hr,
    cases s with s hs,
    cases v with v hv,
    cases w with w hw,
    simp,
    congr, {
        rw nat_add_mul_left_div_left,
        rw nat.div_eq_of_lt hv; refl,
        linarith,
    }, {
        rw nat_add_mul_left_div_left,
        rw nat.div_eq_of_lt hw; refl,
        linarith,
    }, {
        rw nat_add_mul_left_mod_left,
        rw nat.mod_eq_of_lt hv,
    }, {
        rw nat_add_mul_left_mod_left,
        rw nat.mod_eq_of_lt hw,
    }
end

theorem kron_ext_mul (M : Matrix (m*p) (n*q))
        : (∀ (r : fin m) (s : fin n) (v : fin p) (w : fin q)
           , A r s * B v w = M (kron_loc r v) (kron_loc s w))
          → A ⊗ B = M
:= begin
    intro h,
    rw <- matrix.ext_iff,
    intros x y,
    unfold kron,
    rw h,
    unfold kron_loc,
    unfold kron_div kron_mod,
    simp,
    congr, {
        cases x with x hx,
        simp,
        rw add_comm,
        apply nat.mod_add_div,
    }, {
        cases y with y hy,
        simp,
        rw add_comm,
        apply nat.mod_add_div,
    }
end

theorem kron_ext_mul_iff {M : Matrix (m*p) (n*q)}
        : A ⊗ B = M
          ↔ (∀ (r : fin m) (s : fin n) (v : fin p) (w : fin q)
           , A r s * B v w = M (kron_loc r v) (kron_loc s w))
:= begin
    split, intros h, {
        intros, rw mul_to_kron, rw h,
    }, {
        apply kron_ext_mul,
    }
end

@[simp]
lemma kron_zero_left {p q m n} {x : Matrix m n} : (0 : Matrix p q) ⊗ x = 0
:= begin
    apply kron_ext_mul, intros r s v w, simp,
end

@[simp]
lemma kron_zero_right {p q m n} {x : Matrix m n} : x ⊗ (0 : Matrix p q) = 0
:= begin
    apply kron_ext_mul, intros r s v w, simp,
end

theorem kron_id : (I m) ⊗ (I n) = I (m * n)
:= begin
    apply kron_ext_mul,
    intros r s v w,
    by_cases h1: r = s, {
        rw <- h1,
        clear h1,
        by_cases h2: v = w, {
            rw <- h2,
            clear h2,
            simp,
        }, {
            have f1: (I n) v w = 0, {
                apply if_neg, exact h2,
            },
            rw f1,
            simp,
            have f2: (kron_loc r v) ≠ (kron_loc r w), {
                unfold kron_loc,
                intro h,
                apply h2,
                rw fin.eq_iff_veq at h,
                simp at h,
                apply fin.coe_injective,
                exact h,
            },
            symmetry,
            apply if_neg,
            exact f2,
        }
    }, {
        have f1: (I m) r s = 0, {
            apply if_neg, exact h1,
        },
        rw f1,
        simp,
        have f2: (kron_loc r v) ≠ (kron_loc s w), {
            unfold kron_loc,
            intro h,
            apply h1,
            rw fin.eq_iff_veq at h,
            cases v with v vh,
            cases w with w wh,
            simp at h,
            cases add_mul_congr h vh wh with e1 e2,
            apply fin.coe_injective,
            exact e1,
        },
        symmetry,
        apply if_neg,
        exact f2,
    }
end

-- kron distributive over addition
theorem kron_dist_over_add_right (C : Matrix p q) : A ⊗ (B + C) = A ⊗ B + A ⊗ C
:= begin
    apply matrix.ext, intros i j,
    unfold kron, simp,
    ring,
end

theorem kron_dist_over_add_left (C : Matrix p q) : (B + C) ⊗ A = B ⊗ A + C ⊗ A
:= begin
    apply matrix.ext, intros i j,
    unfold kron, simp,
    ring,
end

lemma kron_dist_over_sub_right (C : Matrix p q) : A ⊗ (B - C) = A ⊗ B - A ⊗ C
:= begin
    apply matrix.ext, intros i j,
    unfold kron, simp,
    ring,
end

lemma kron_dist_over_sub_left (C : Matrix p q) : (B - C) ⊗ A = B ⊗ A - C ⊗ A
:= begin
    apply matrix.ext, intros i j,
    unfold kron, simp,
    ring,
end

@[simp]
lemma kron_smul_right {s : ℂ} : A ⊗ (s • B) = s • (A ⊗ B)
:= begin
    apply kron_ext_mul, intros r s v w,
    simp,
    rw <- mul_assoc,
    rw mul_comm (A r s),
    rw mul_assoc,
    congr' 1,
    apply mul_to_kron,
end

@[simp]
lemma kron_smul_left {s : ℂ} : (s • A) ⊗ B = s • (A ⊗ B)
:= begin
    apply kron_ext_mul, intros r s v w,
    simp,
    rw mul_assoc,
    congr' 1,
    apply mul_to_kron,
end

lemma kron_id_left : (I 1) ⊗ A = cast (by simp) A
:= begin
    apply matrix.ext, intros i j,
    unfold kron kron_div kron_mod,
    cases i with i ip,
    cases j with j jp,
    simp,
    rw matrix_cast_apply; try {simp},

    have ip': i < m, by linarith,
    have jp': j < n, by linarith,

    congr' 2, {
        rw nat.mod_eq_of_lt ip',
    }, {
        rw nat.mod_eq_of_lt jp',
    },
end

lemma kron_id_right : A ⊗ (I 1) = cast (by simp) A
:= begin
    apply matrix.ext, intros i j,
    unfold kron kron_div kron_mod,
    cases i with i ip,
    cases j with j jp,
    simp,
    rw matrix_cast_apply; try {simp},
    congr' 2,
end

-- Special case of 1 × 1 matrix.
@[simp] lemma kron_one_one : (I 1) ⊗ (I 1) = I 1
:= begin
    rw kron_id_right, refl,
end

-- Special case of 1 × 1 matrix.
@[simp] lemma kron_id_left_square_one (M : Square 1) : (I 1) ⊗ M = M
:= begin
    unfold kron kron_div kron_mod,
    apply matrix.ext, intros i j, simp,
    congr,
end

-- Special case of 1 × 1 matrix.
@[simp] lemma kron_id_right_square_one (M : Square 1) : M ⊗ (I 1) = M
:= begin
    unfold kron kron_div kron_mod,
    apply matrix.ext, intros i j, simp,
end

-- Special case of 1 × 1 matrix.
lemma kron_square_one_eq_mul {x y : Square 1} : x ⊗ y = x ⬝ y
:= begin
    apply matrix.ext, intros i j,
    have i0 : i = ⟨0, by simp⟩, cases i; simp; linarith,
    have j0 : j = ⟨0, by simp⟩, cases j; simp; linarith,
    cases i0, clear i0,
    cases j0, clear j0,
    unfold kron kron_div kron_mod, simp,

    have f1: (x ⬝ y) ⟨0, by simp⟩ ⟨0, by simp⟩ = x 0 0 * y 0 0, {
        simp, apply matrix_mul_square_one,
    },
    rw <- f1, refl,
end

-- Special case of 1 × 1 matrix.
lemma kron_cancel_left {x : Matrix m n} {y z : Square 1} : x ⊗ y = x ⊗ z → x ≠ 0 → y = z
:= begin
    intros h xn,

    apply matrix.ext, intros i j,
    rw <- matrix.ext_iff at h,
    rcases (Matrix_nonzero_has_nonzero_val xn) with ⟨r, ⟨s, h1⟩⟩,
    specialize h ⟨r, by {cases r, linarith}⟩ ⟨s, by {cases s, linarith}⟩,
    unfold kron kron_div kron_mod at h, simp at h,

    cases h, {
        have i0 : i = 0, cases i; simp, cases i0; clear i0,
        have j0 : j = 0, cases j; simp, cases j0; clear j0,
        simp,
        assumption,
    }, {
        exfalso, apply h1, assumption,
    }
end

lemma kron_diagonal {n m} {A : fin n → ℂ} {B : fin m → ℂ}
    : (matrix.diagonal A) ⊗ (matrix.diagonal B)
        = matrix.diagonal (λ i, A (kron_div i) * B (kron_mod i))
:= begin
    apply kron_ext_mul, intros r s v w,
    by_cases h1: r = s, {
        cases h1, clear h1,
        by_cases h2: v = w, {
            cases h2, clear h2, simp,
        }, {
            have : (kron_loc r v) ≠ (kron_loc r w),
            {
                intros c,
                rw kron_loc_inj_iff at c,
                cc,
            },
            rw matrix.diagonal_apply_ne h2,
            rw matrix.diagonal_apply_ne this,
            simp,
        }
    }, {
        have : (kron_loc r v) ≠ (kron_loc s w),
        {
            intros c,
            rw kron_loc_inj_iff at c,
            cc,
        },
        rw matrix.diagonal_apply_ne h1,
        rw matrix.diagonal_apply_ne this,
        simp,
    },
end

end kron

----------------------------------------------------------------------------------------
-- theorem kron_std_basis

-- Kronecker product of two standard basis vector is another standard basis vector.
theorem kron_std_basis {n m : ℕ} (i : fin n) (j : fin m)
        : kron (std_basis i) (std_basis j)
          = std_basis ⟨m * (i : ℕ) + (j : ℕ), fin_add_mul_lt i j⟩
:= begin
    apply kron_ext_mul,
    intros r s v w,
    unfold kron_loc,
    by_cases h1: r = i, {
        rw h1,
        simp,
        by_cases h2: v = j, {
            rw h2,
            simp,
        }, {
            rw std_basis_eq_zero h2,
            rw std_basis_eq_zero,
            simp,
            intro c,
            apply h2,
            apply fin.coe_injective,
            exact c,
        }
    }, {
        rw std_basis_eq_zero h1,
        simp,
        rw std_basis_eq_zero,
        simp,
        intro c,
        cases (add_mul_congr c v.property j.property) with f1 f2,
        apply h1,
        apply fin.coe_injective,
        exact f1,
    }
end

------------------------------------------------------------------------------------------------
-- kron assoc

section kron_assoc

variables {m n p q r s: ℕ} (a : Matrix m n) (b : Matrix p q) (c : Matrix r s)

lemma kron_assoc_cast : Matrix ((m * p) * r) ((n * q) * s) = Matrix (m * (p * r)) (n * (q * s))
:= begin
    ring,
end

theorem kron_assoc : a ⊗ (b ⊗ c) = cast kron_assoc_cast ((a ⊗ b) ⊗ c)
:= begin
    apply matrix.ext, intros i j,
    unfold kron,

    cases i with i ip,
    cases j with j jp,
    unfold kron_div kron_mod,
    simp,
    rw matrix_cast_apply; simp <|> skip, {
        rw mul_assoc,
        congr' 3, {
            rw coe_cast_fin; try { solve1 {ring <|> simp} <|> simp },
            ring, symmetry; apply nat.div_div_eq_div_mul,
        }, {
            rw coe_cast_fin; try { solve1 {ring <|> simp} <|> simp },
            ring, symmetry; apply nat.div_div_eq_div_mul,
        }, {
            simp, rw coe_cast_fin; try { solve1 {ring <|> simp} <|> simp },
            apply nat.mod_mul_left_div_self,
        }, {
            simp, rw coe_cast_fin; try { solve1 {ring <|> simp} <|> simp },
            apply nat.mod_mul_left_div_self,
        }, {
            simp, rw coe_cast_fin; try { solve1 {ring <|> simp} <|> simp },
        }, {
            simp, rw coe_cast_fin; try { solve1 {ring <|> simp} <|> simp },
        }
    }, {
        ring,
    }, {
        ring,
    }
end

lemma kron_assoc_l2r : (a ⊗ b) ⊗ c = cast kron_assoc_cast.symm (a ⊗ (b ⊗ c))
:= begin
    rw kron_assoc,
    rw cast_roundtrip,
end

end kron_assoc

------------------------------------------------------------------------------
-- kron_mixed_prod

section kron_sum_mul_mul

variables {α : Type} [comm_semiring α]
variables {n m : ℕ}
variables (f : fin n → α)
variables (g : fin m → α)

def kron_to_prod (i : fin (n * m)) : fin n × fin m := ⟨kron_div i, kron_mod i⟩

lemma kron_to_prod_inj (i j : fin (n * m)) : kron_to_prod i = kron_to_prod j → i = j
:= begin
    cases i with i ih,
    cases j with j jh,
    unfold kron_to_prod kron_div kron_mod, simp, intros p q,
    have f1: (i / m * m) = (j / m * m), {
        exact congr (congr_arg has_mul.mul p) rfl,
    },
    have mp : 0 < m, {
        have f1 : 0 < n * m, {
            linarith,
        },
        apply pos_of_mul_pos_left f1, simp,
    },
    let h1 := nat_decompose_mul_add i mp,
    let h2 := nat_decompose_mul_add j mp,
    rw h1,
    rw h2,
    congr; assumption,
end

lemma kron_sum_mul_mul : (∑ x, f x) * (∑ x, g x) = ∑ (x : fin (n * m)), f (kron_div x) * g (kron_mod x)
:= begin
    rw finset.sum_mul_sum,
    rw <- finset.sum_preimage (λ x : fin (n*m), (⟨kron_div x, kron_mod x⟩ : fin n × fin m)),
    congr, {
        ext; simp,
    }, {
        simp,
        unfold set.inj_on,
        intros,
        apply kron_to_prod_inj,
        assumption,
    }, {
        intros x h1 h2,
        exfalso,
        apply h2, clear h2,
        simp,
        use (m * x.fst + x.snd), {
            cases x,
            simp,
            apply_mod_cast fin_add_mul_lt,
        }, {
            cases x,
            simp,
        }
    }
end

end kron_sum_mul_mul

section kron_mixed_prod

variables {n m o : ℕ} (a : Matrix m n) (c : Matrix n o)
variables {q r s : ℕ} (b : Matrix q r) (d : Matrix r s)

theorem kron_mixed_prod : (a ⊗ b) ⬝ (c ⊗ d) = (a ⬝ c) ⊗ (b ⬝ d)
:= begin
    apply matrix.ext, intros i j,
    unfold matrix.mul,
    unfold kron,
    simp,
    unfold matrix.dot_product,
    rw kron_sum_mul_mul,
    congr,
    apply funext, intro x,
    ring,
end

lemma kron_mixed_prod_I_left : ((I q) ⊗ a) ⬝ (b ⊗ c) = b ⊗ (a ⬝ c)
:= begin
    have : b ⊗ (a ⬝ c) = ((I q) ⬝ b) ⊗ (a ⬝ c), by simp,
    rw this, clear this,
    rw kron_mixed_prod,
end

lemma kron_mixed_prod_I_right : (b ⊗ a) ⬝ ((I r) ⊗ c) = b ⊗ (a ⬝ c)
:= begin
    have : b ⊗ (a ⬝ c) = (b ⬝ (I r)) ⊗ (a ⬝ c), by simp,
    rw this, clear this,
    rw kron_mixed_prod,
end

end kron_mixed_prod

------------------------------------------------------------------------------
-- kron + unit lemmas

section unit_kron

variables {n : ℕ} {s : Vector n}
variables {m : ℕ} {t : Vector m}

lemma unit_kron_of_unit : s.unit → t.unit → (s ⊗ t).unit
:= begin
    unfold matrix.unit,
    intros su tu,
    rw adjoint_kron,
    rw kron_mixed_prod,
    rw su,
    rw tu,
    simp,
end

lemma unit_kron_right : (s ⊗ t).unit → s.unit → t.unit
:= begin
    unfold matrix.unit, intros h su,
    rw adjoint_kron at h,
    rw kron_mixed_prod at h,
    rw su at h,
    rw kron_id_left at h,
    apply h,
end

lemma unit_kron_left : (s ⊗ t).unit → t.unit → s.unit
:= begin
    unfold matrix.unit, intros h tu,
    rw adjoint_kron at h,
    rw kron_mixed_prod at h,
    rw tu at h,
    rw kron_id_right at h,
    apply h,
end

end unit_kron

------------------------------------------------------------------------------------------------
-- unitary lemmas

section unitary

variables {n : ℕ} (U: Matrix n n)

lemma unfold_unitary {U : Matrix n n} : U.unitary → (U†) ⬝ U = 1 := by tautology

-- Compatbility with `is_unit U.det`.
lemma unitary_is_unit_det : U.unitary → is_unit U.det
:= begin
    unfold Matrix.unitary,
    intro h,
    apply matrix.is_unit_det_of_left_inverse; assumption,
end

-- Compatbility with `is_unit U`.
lemma unitary_is_unit : U.unitary → is_unit U
:= begin
    intros h,
    rw matrix.is_unit_iff_is_unit_det,
    apply unitary_is_unit_det; assumption,
end

-- Unitary matrix has a right inverse.
lemma unitary_mul_inv_right : U.unitary → U ⬝ U⁻¹ = 1
:= begin
    intro h,
    rw matrix.mul_nonsing_inv,
    apply unitary_is_unit_det; assumption,
end

-- Unitary matrix has a left inverse.
lemma unitary_mul_inv_left : U.unitary → U⁻¹ ⬝ U = 1
:= begin
    intro h,
    rw matrix.nonsing_inv_mul,
    apply unitary_is_unit_det; assumption,
end

-- U† is the inverse.
lemma unitary_inv_eq_adjoint : U.unitary → (U⁻¹) = (U†)
:= begin
    intros h,
    have f1: (U†) ⬝ U ⬝ (U⁻¹) = (U⁻¹), {
        unfold Matrix.unitary at h,
        rw h, simp,
    },
    rw <- f1,
    rw matrix.mul_assoc,
    rw unitary_mul_inv_right; simp <|> assumption,
end

-- Unitary property `U† ⬝ U = 1` can be stated the other way around.
theorem unitary_comm : U.unitary ↔ U ⬝ (U†) = 1
:= begin
    split; intros h; apply matrix.nonsing_inv_left_right; assumption,
end

-- Unitary matrix is also normal.
-- (But, not all normal matrices are unitary.)
theorem unitary_normal : U.unitary → U.normal
:= begin
    unfold Matrix.normal,
    unfold Matrix.unitary,
    intros h,
    rw h,
    symmetry, rw <- unitary_comm, assumption,
end

end unitary

section unitary_and_vector

variables {n : ℕ} (U : Matrix n n)
variables (v : Vector n) (w : Vector n)

-- Unitary operator is norm-preserving.
-- The angle between two quantum states preserves under any unitary operations
theorem unitary_preserve_norm : (U†) ⬝ U = 1 → ((U ⬝ v)†) ⬝ (U ⬝ w) = (v†) ⬝ w
:= begin
    intros up,
    rw adjoint_mul,
    rw <- matrix.mul_assoc,
    rw matrix.mul_assoc (v†),
    rw up; simp [*],
end

-- Unitary matrix presevese the validity of quantum state.
example : (U†) ⬝ U = 1 → (v†) ⬝ v = 1 → ((U ⬝ v)†) ⬝ (U ⬝ v) = 1
:= begin
    intros up pp,
    rw unitary_preserve_norm; assumption,
end

example : U.unitary → ((U ⬝ v)†) ⬝ (U ⬝ w) = (v†) ⬝ w
:= begin
    intros h,
    apply unitary_preserve_norm; assumption,
end

example : U.unitary → (w†) ⬝ w = 1 → ((U ⬝ w)†) ⬝ (U ⬝ w) = 1
:= begin
    intros h wu,
    rw unitary_preserve_norm; assumption,
end

end unitary_and_vector

------------------------------------------------------------------------------
-- Matrix.inner_product & Matrix.norm & Matrix.dist

namespace Matrix

noncomputable
def inner_product {n} (x y : Vector n) := (x† ⬝ y) 0 0

noncomputable
instance {n : ℕ} : has_inner ℂ (Vector n) := ⟨inner_product⟩

noncomputable
def norm {n} (x : Vector n) := real.sqrt (is_R_or_C.re (inner_product x x))

noncomputable
instance {n : ℕ} : has_norm (Vector n) := ⟨norm⟩

/-- Distance between two vectors -/
noncomputable
def dist {n : ℕ} (x y : Vector n) := norm (x - y)

noncomputable
instance {n : ℕ} : has_dist (Vector n) := ⟨Matrix.dist⟩

end Matrix

notation `⟪` X `,` Y `⟫` := @has_inner.inner ℂ _ _ X Y

------------------------------------------------------------------------------
-- Matrix inner product operator is compatible with matrix.inner_product.
-- So are norm and dist.

section inner_product_compat

variables {n : ℕ} (s t : Vector n)

lemma Matrix_inner_eq_matrix_inner : ⟪s,t⟫ = ⟪ λ i, s i 0, λ i, t i 0 ⟫
:= begin
    unfold inner inner_product Matrix.inner_product matrix.mul, congr,
end

lemma Matrix_norm_eq_matrix_norm : ∥s∥ = ∥ (λ i, s i 0) ∥
:= begin
    unfold has_norm.norm Matrix.norm matrix.norm, congr,
end

lemma Matrix_dist_eq_matrix_dist : Matrix.dist s t = matrix.dist (λ i, s i 0) (λ i, t i 0)
:= begin
    unfold Matrix.dist matrix.dist,
    unfold has_norm.norm Matrix.norm matrix.norm, congr,
end

end inner_product_compat

------------------------------------------------------------------------------
-- Vector normed_group

section normed_group

variables {m : ℕ}

noncomputable
instance : metric_space (Vector m) := {
dist               := dist,
dist_self          :=
    begin
        intros x, unfold has_dist.dist, rw Matrix_dist_eq_matrix_dist,
        unfold matrix.dist, simp,
    end,
eq_of_dist_eq_zero :=
    begin
        intros x y, unfold has_dist.dist, rw Matrix_dist_eq_matrix_dist,
        intros h,
        have : (λ (i : fin m), x i 0) = (λ (i : fin m), y i 0),
        { apply matrix.eq_of_dist_eq_zero h, },
        apply matrix.ext, intros i j,
        have j0: j = 0, { simp, },
        cases j0, clear j0, simp,
        change (λ (i : fin m), x i 0) i = (λ (i : fin m), y i 0) i,
        cc,
    end,
dist_comm          :=
    begin
        intros x y, unfold has_dist.dist, iterate 2 { rw Matrix_dist_eq_matrix_dist },
        apply matrix.dist_comm,
    end,
dist_triangle      :=
    begin
        intros x y z, unfold has_dist.dist, iterate 2 { rw Matrix_dist_eq_matrix_dist },
        apply matrix.dist_triangle,
    end,
}

lemma Matrix.dist_eq (x y : Vector m) : dist x y = ∥x - y∥ := by refl

noncomputable
instance : normed_group (Vector m) := ⟨ Matrix.dist_eq ⟩

end normed_group

------------------------------------------------------------------------------
-- Vector inner_product_space

section inner_product_space

variables {m : ℕ}

lemma Matrix_smul_apply (a : ℂ) (s : Vector m)
        : (λ i, (a • s) i 0) = a • (λ i, s i 0)
:= begin
    apply funext, intros i,
    apply smul_apply,
end

noncomputable
instance : normed_space ℂ (Vector m) := {
norm_smul_le :=
    begin
        intros,
        iterate 2 { rw Matrix_norm_eq_matrix_norm },
        rw Matrix_smul_apply,
        unfold has_norm.norm,
        rw matrix.norm_smul,
        simp,
    end
}

noncomputable
instance : inner_product_space ℂ (Vector m) := {
norm_sq_eq_inner :=
    begin
        intros x,
        rw Matrix_inner_eq_matrix_inner,
        rw Matrix_norm_eq_matrix_norm,
        apply has_norm_sq_eq_re_inner_product_self,
    end,
conj_sym :=
    begin
        intros x y,
        iterate 2 { rw Matrix_inner_eq_matrix_inner, },
        unfold inner,
        rw <- conj_inner_product, simp,
    end,
add_left :=
    begin
        intros x y z,
        iterate 3 { rw Matrix_inner_eq_matrix_inner, },
        unfold inner,
        apply inner_product_add_left,
    end,
smul_left :=
    begin
        intros x y r,
        iterate 2 { rw Matrix_inner_eq_matrix_inner, },
        unfold inner,
        apply inner_product_smul_l,
    end,
}

end inner_product_space

------------------------------------------------------------------------------
-- Matrix inner product lemmas

section inner_product_lemmas

variables {n : ℕ}
variables {x y z : Vector n}

lemma norm_eq_one_of_unit : x.unit → ∥x∥ = 1
:= begin
    intros xu,
    unfold has_norm.norm,
    unfold Matrix.norm Matrix.inner_product,
    rw unfold_unit xu, simp,
end

lemma inner_product_bound_of_unit : x.unit → y.unit → |⟪x,y⟫| ≤ 1
:= begin
    intros xu yu,
    have f1: |⟪x,y⟫| ≤ ∥x∥ * ∥y∥, {
        unfold has_inner.inner has_norm.norm,
        apply matrix.cauchy_schwarz_inequality_alt,
    },
    rw norm_eq_one_of_unit xu at f1,
    rw norm_eq_one_of_unit yu at f1,
    calc |inner x y| ≤ 1 * 1 : f1
                  ...= 1 : by simp,
end

lemma inner_product_zero_iff : x† ⬝ y = 0 ↔ ⟪x,y⟫ = 0
:= begin
    unfold inner Matrix.inner_product, split; intros h, {
        rw h, simp,
    }, {
        apply matrix.ext, intros i j,
        have i0 : i = 0, cases i; simp, cases i0; clear i0,
        have j0 : j = 0, cases j; simp, cases j0; clear j0,
        simp at *, assumption,
    }
end

lemma Matrix_inner_self_eq_norm_sq : ⟪x,x⟫.re = ∥x∥^2
:= begin
    rw Matrix_inner_eq_matrix_inner,
    rw Matrix_norm_eq_matrix_norm,
    unfold inner,
    rw has_norm_sq_eq_re_inner_product_self; simp,
end

lemma Matrix_inner_self_im_zero : ⟪x,x⟫.im = 0
:= begin
    rw Matrix_inner_eq_matrix_inner,
    unfold inner,
    rw <- is_R_or_C.im_to_complex,
    apply inner_product_self_im_zero,
end

lemma complex.re_eq_self_of_im_zero (x : ℂ) : x.im = 0 → (x.re : ℂ) = x
:= begin
    cases x, simp, intros h,
    rw h, split,
end

lemma Matrix_inner_self_real : (⟪x,x⟫.re : ℂ) = ⟪x,x⟫
:= begin
    apply complex.re_eq_self_of_im_zero,
    apply Matrix_inner_self_im_zero,
end

lemma norm_eq_one_iff_unit {n : ℕ} {x : Vector n} : x.unit ↔ ∥x∥ = 1
:= begin
    split; intros h,
    { apply norm_eq_one_of_unit, assumption, },
    {
        unfold matrix.unit,
        apply matrix.ext, intros i j,
        have : i = 0, by simp, cases this, clear this,
        have : j = 0, by simp, cases this, clear this,
        change ⟪x, x⟫ = 1,

        have h2: ∥x∥^2 = 1,
        { rw h, simp, },
        rw <- Matrix_inner_self_real,
        rw Matrix_inner_self_eq_norm_sq,
        apply_mod_cast h2,
    }
end

lemma norm_smul_norm_inv_eq_one {n : ℕ} {s : Vector n} : ∥s∥ ≠ 0 → ∥(∥s∥⁻¹ • s)∥ = 1
:= begin
    intros h,
    rw _root_.norm_smul, simp,
    ring,
    apply mul_inv_cancel h,
end

end inner_product_lemmas

author: duckki

repo: lean-quantum

save_path: github-repos/lean/duckki-lean-quantum


text:
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import data.set.function
import logic.function.iterate

/-!
# Fixed points of a self-map

In this file we define

* the predicate `is_fixed_pt f x := f x = x`;
* the set `fixed_points f` of fixed points of a self-map `f`.

We also prove some simple lemmas about `is_fixed_pt` and `∘`, `iterate`, and `semiconj`.

## Tags

fixed point
-/

universes u v

variables {α : Type u} {β : Type v} {f fa g : α → α} {x y : α} {fb : β → β} {m n k : ℕ}

namespace function

/-- A point `x` is a fixed point of `f : α → α` if `f x = x`. -/
def is_fixed_pt (f : α → α) (x : α) := f x = x

/-- Every point is a fixed point of `id`. -/
lemma is_fixed_pt_id (x : α) : is_fixed_pt id x := (rfl : _)

namespace is_fixed_pt

instance [h : decidable_eq α] {f : α → α} {x : α} : decidable (is_fixed_pt f x) :=
h (f x) x

/-- If `x` is a fixed point of `f`, then `f x = x`. This is useful, e.g., for `rw` or `simp`.-/
protected lemma eq (hf : is_fixed_pt f x) : f x = x := hf

/-- If `x` is a fixed point of `f` and `g`, then it is a fixed point of `f ∘ g`. -/
protected lemma comp (hf : is_fixed_pt f x) (hg : is_fixed_pt g x) : is_fixed_pt (f ∘ g) x :=
calc f (g x) = f x : congr_arg f hg
         ... = x   : hf

/-- If `x` is a fixed point of `f`, then it is a fixed point of `f^[n]`. -/
protected lemma iterate (hf : is_fixed_pt f x) (n : ℕ) : is_fixed_pt (f^[n]) x :=
iterate_fixed hf n

/-- If `x` is a fixed point of `f ∘ g` and `g`, then it is a fixed point of `f`. -/
lemma left_of_comp (hfg : is_fixed_pt (f ∘ g) x) (hg : is_fixed_pt g x) : is_fixed_pt f x :=
calc f x = f (g x) : congr_arg f hg.symm
     ... = x       : hfg

/-- If `x` is a fixed point of `f` and `g` is a left inverse of `f`, then `x` is a fixed
point of `g`. -/
lemma to_left_inverse (hf : is_fixed_pt f x) (h : left_inverse g f) : is_fixed_pt g x :=
calc g x = g (f x) : congr_arg g hf.symm
     ... = x       : h x

/-- If `g` (semi)conjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`. -/
protected lemma map {x : α} (hx : is_fixed_pt fa x) {g : α → β} (h : semiconj g fa fb) :
  is_fixed_pt fb (g x) :=
calc fb (g x) = g (fa x) : (h.eq x).symm
          ... = g x      : congr_arg g hx

protected lemma apply {x : α} (hx : is_fixed_pt f x) : is_fixed_pt f (f x) :=
by convert hx

end is_fixed_pt

@[simp] lemma injective.is_fixed_pt_apply_iff (hf : injective f) {x : α} :
  is_fixed_pt f (f x) ↔ is_fixed_pt f x :=
⟨λ h, hf h.eq, is_fixed_pt.apply⟩

/-- The set of fixed points of a map `f : α → α`. -/
def fixed_points (f : α → α) : set α := {x : α | is_fixed_pt f x}

instance fixed_points.decidable [decidable_eq α] (f : α → α) (x : α) :
  decidable (x ∈ fixed_points f) :=
is_fixed_pt.decidable

@[simp] lemma mem_fixed_points : x ∈ fixed_points f ↔ is_fixed_pt f x := iff.rfl

lemma mem_fixed_points_iff {α : Type*} {f : α → α} {x : α} :
  x ∈ fixed_points f ↔ f x = x :=
by refl

@[simp] lemma fixed_points_id : fixed_points (@id α) = set.univ :=
set.ext $ λ _, by simpa using is_fixed_pt_id _

lemma fixed_points_subset_range : fixed_points f ⊆ set.range f :=
λ x hx, ⟨x, hx⟩

/-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`. -/
lemma semiconj.maps_to_fixed_pts {g : α → β} (h : semiconj g fa fb) :
  set.maps_to g (fixed_points fa) (fixed_points fb) :=
λ x hx, hx.map h

/-- Any two maps `f : α → β` and `g : β → α` are inverse of each other on the sets of fixed points
of `f ∘ g` and `g ∘ f`, respectively. -/
lemma inv_on_fixed_pts_comp (f : α → β) (g : β → α) :
  set.inv_on f g (fixed_points $ f ∘ g) (fixed_points $ g ∘ f) :=
⟨λ x, id, λ x, id⟩

/-- Any map `f` sends fixed points of `g ∘ f` to fixed points of `f ∘ g`. -/
lemma maps_to_fixed_pts_comp (f : α → β) (g : β → α) :
  set.maps_to f (fixed_points $ g ∘ f) (fixed_points $ f ∘ g) :=
λ x hx, hx.map $ λ x, rfl

/-- Given two maps `f : α → β` and `g : β → α`, `g` is a bijective map between the fixed points
of `f ∘ g` and the fixed points of `g ∘ f`. The inverse map is `f`, see `inv_on_fixed_pts_comp`. -/
lemma bij_on_fixed_pts_comp (f : α → β) (g : β → α) :
  set.bij_on g (fixed_points $ f ∘ g) (fixed_points $ g ∘ f) :=
(inv_on_fixed_pts_comp f g).bij_on (maps_to_fixed_pts_comp g f) (maps_to_fixed_pts_comp f g)

/-- If self-maps `f` and `g` commute, then they are inverse of each other on the set of fixed points
of `f ∘ g`. This is a particular case of `function.inv_on_fixed_pts_comp`. -/
lemma commute.inv_on_fixed_pts_comp (h : commute f g) :
  set.inv_on f g (fixed_points $ f ∘ g) (fixed_points $ f ∘ g) :=
by simpa only [h.comp_eq] using inv_on_fixed_pts_comp f g

/-- If self-maps `f` and `g` commute, then `f` is bijective on the set of fixed points of `f ∘ g`.
This is a particular case of `function.bij_on_fixed_pts_comp`. -/
lemma commute.left_bij_on_fixed_pts_comp (h : commute f g) :
  set.bij_on f (fixed_points $ f ∘ g) (fixed_points $ f ∘ g) :=
by simpa only [h.comp_eq] using bij_on_fixed_pts_comp g f

/-- If self-maps `f` and `g` commute, then `g` is bijective on the set of fixed points of `f ∘ g`.
This is a particular case of `function.bij_on_fixed_pts_comp`. -/
lemma commute.right_bij_on_fixed_pts_comp (h : commute f g) :
  set.bij_on g (fixed_points $ f ∘ g) (fixed_points $ f ∘ g) :=
by simpa only [h.comp_eq] using bij_on_fixed_pts_comp f g

end function

author: Parinya-Siri

repo: lean-machine-learning


text:
/-
Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Yury G. Kudryashov
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.order.filter.basic
import Mathlib.data.set.countable
import Mathlib.PostPort

universes u_2 l u_1

namespace Mathlib

/-!
# Filters with countable intersection property

In this file we define `countable_Inter_filter` to be the class of filters with the following
property: for any countable collection of sets `s ∈ l` their intersection belongs to `l` as well.

Two main examples are the `residual` filter defined in `topology.metric_space.baire` and
the `measure.ae` filter defined in `measure_theory.measure_space`.
-/

/-- A filter `l` has the countable intersection property if for any countable collection
of sets `s ∈ l` their intersection belongs to `l` as well. -/
class countable_Inter_filter {α : Type u_2} (l : filter α)
where
  countable_sInter_mem_sets' : ∀ {S : set (set α)}, set.countable S → (∀ (s : set α), s ∈ S → s ∈ l) → ⋂₀S ∈ l

theorem countable_sInter_mem_sets {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set (set α)} (hSc : set.countable S) : ⋂₀S ∈ l ↔ ∀ (s : set α), s ∈ S → s ∈ l :=
  { mp := fun (hS : ⋂₀S ∈ l) (s : set α) (hs : s ∈ S) => filter.mem_sets_of_superset hS (set.sInter_subset_of_mem hs),
    mpr := countable_Inter_filter.countable_sInter_mem_sets' hSc }

theorem countable_Inter_mem_sets {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s : ι → set α} : (set.Inter fun (i : ι) => s i) ∈ l ↔ ∀ (i : ι), s i ∈ l :=
  set.sInter_range s ▸ iff.trans (countable_sInter_mem_sets (set.countable_range s)) set.forall_range_iff

theorem countable_bInter_mem_sets {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : set.countable S) {s : (i : ι) → i ∈ S → set α} : (set.Inter fun (i : ι) => set.Inter fun (H : i ∈ S) => s i H) ∈ l ↔ ∀ (i : ι) (H : i ∈ S), s i H ∈ l := sorry

theorem eventually_countable_forall {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {p : α → ι → Prop} : filter.eventually (fun (x : α) => ∀ (i : ι), p x i) l ↔ ∀ (i : ι), filter.eventually (fun (x : α) => p x i) l := sorry

theorem eventually_countable_ball {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : set.countable S) {p : α → (i : ι) → i ∈ S → Prop} : filter.eventually (fun (x : α) => ∀ (i : ι) (H : i ∈ S), p x i H) l ↔
  ∀ (i : ι) (H : i ∈ S), filter.eventually (fun (x : α) => p x i H) l := sorry

theorem eventually_le.countable_Union {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s : ι → set α} {t : ι → set α} (h : ∀ (i : ι), filter.eventually_le l (s i) (t i)) : filter.eventually_le l (set.Union fun (i : ι) => s i) (set.Union fun (i : ι) => t i) :=
  filter.eventually.mono (iff.mpr eventually_countable_forall h)
    fun (x : α) (hst : ∀ (i : ι), s i x ≤ t i x) (hs : set.Union (fun (i : ι) => s i) x) =>
      iff.mpr set.mem_Union (Exists.imp hst (iff.mp set.mem_Union hs))

theorem eventually_eq.countable_Union {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s : ι → set α} {t : ι → set α} (h : ∀ (i : ι), filter.eventually_eq l (s i) (t i)) : filter.eventually_eq l (set.Union fun (i : ι) => s i) (set.Union fun (i : ι) => t i) :=
  filter.eventually_le.antisymm (eventually_le.countable_Union fun (i : ι) => filter.eventually_eq.le (h i))
    (eventually_le.countable_Union fun (i : ι) => filter.eventually_eq.le (filter.eventually_eq.symm (h i)))

theorem eventually_le.countable_bUnion {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : set.countable S) {s : (i : ι) → i ∈ S → set α} {t : (i : ι) → i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), filter.eventually_le l (s i H) (t i H)) : filter.eventually_le l (set.Union fun (i : ι) => set.Union fun (H : i ∈ S) => s i H)
  (set.Union fun (i : ι) => set.Union fun (H : i ∈ S) => t i H) := sorry

theorem eventually_eq.countable_bUnion {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : set.countable S) {s : (i : ι) → i ∈ S → set α} {t : (i : ι) → i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), filter.eventually_eq l (s i H) (t i H)) : filter.eventually_eq l (set.Union fun (i : ι) => set.Union fun (H : i ∈ S) => s i H)
  (set.Union fun (i : ι) => set.Union fun (H : i ∈ S) => t i H) := sorry

theorem eventually_le.countable_Inter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s : ι → set α} {t : ι → set α} (h : ∀ (i : ι), filter.eventually_le l (s i) (t i)) : filter.eventually_le l (set.Inter fun (i : ι) => s i) (set.Inter fun (i : ι) => t i) :=
  filter.eventually.mono (iff.mpr eventually_countable_forall h)
    fun (x : α) (hst : ∀ (i : ι), s i x ≤ t i x) (hs : set.Inter (fun (i : ι) => s i) x) =>
      iff.mpr set.mem_Inter fun (i : ι) => hst i (iff.mp set.mem_Inter hs i)

theorem eventually_eq.countable_Inter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [encodable ι] {s : ι → set α} {t : ι → set α} (h : ∀ (i : ι), filter.eventually_eq l (s i) (t i)) : filter.eventually_eq l (set.Inter fun (i : ι) => s i) (set.Inter fun (i : ι) => t i) :=
  filter.eventually_le.antisymm (eventually_le.countable_Inter fun (i : ι) => filter.eventually_eq.le (h i))
    (eventually_le.countable_Inter fun (i : ι) => filter.eventually_eq.le (filter.eventually_eq.symm (h i)))

theorem eventually_le.countable_bInter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : set.countable S) {s : (i : ι) → i ∈ S → set α} {t : (i : ι) → i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), filter.eventually_le l (s i H) (t i H)) : filter.eventually_le l (set.Inter fun (i : ι) => set.Inter fun (H : i ∈ S) => s i H)
  (set.Inter fun (i : ι) => set.Inter fun (H : i ∈ S) => t i H) := sorry

theorem eventually_eq.countable_bInter {ι : Type u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set ι} (hS : set.countable S) {s : (i : ι) → i ∈ S → set α} {t : (i : ι) → i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), filter.eventually_eq l (s i H) (t i H)) : filter.eventually_eq l (set.Inter fun (i : ι) => set.Inter fun (H : i ∈ S) => s i H)
  (set.Inter fun (i : ι) => set.Inter fun (H : i ∈ S) => t i H) := sorry

protected instance countable_Inter_filter_principal {α : Type u_2} (s : set α) : countable_Inter_filter (filter.principal s) :=
  countable_Inter_filter.mk
    fun (S : set (set α)) (hSc : set.countable S) (hS : ∀ (s_1 : set α), s_1 ∈ S → s_1 ∈ filter.principal s) =>
      set.subset_sInter hS

protected instance countable_Inter_filter_bot {α : Type u_2} : countable_Inter_filter ⊥ :=
  eq.mpr (id (Eq._oldrec (Eq.refl (countable_Inter_filter ⊥)) (Eq.symm filter.principal_empty)))
    (Mathlib.countable_Inter_filter_principal ∅)

protected instance countable_Inter_filter_top {α : Type u_2} : countable_Inter_filter ⊤ :=
  eq.mpr (id (Eq._oldrec (Eq.refl (countable_Inter_filter ⊤)) (Eq.symm filter.principal_univ)))
    (Mathlib.countable_Inter_filter_principal set.univ)

/-- Infimum of two `countable_Inter_filter`s is a `countable_Inter_filter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
protected instance countable_Inter_filter_inf {α : Type u_2} (l₁ : filter α) (l₂ : filter α) [countable_Inter_filter l₁] [countable_Inter_filter l₂] : countable_Inter_filter (l₁ ⊓ l₂) := sorry

/-- Supremum of two `countable_Inter_filter`s is a `countable_Inter_filter`. -/
protected instance countable_Inter_filter_sup {α : Type u_2} (l₁ : filter α) (l₂ : filter α) [countable_Inter_filter l₁] [countable_Inter_filter l₂] : countable_Inter_filter (l₁ ⊔ l₂) :=
  countable_Inter_filter.mk
    fun (S : set (set α)) (hSc : set.countable S) (hS : ∀ (s : set α), s ∈ S → s ∈ l₁ ⊔ l₂) =>
      { left := iff.mpr (countable_sInter_mem_sets hSc) fun (s : set α) (hs : s ∈ S) => and.left (hS s hs),
        right := iff.mpr (countable_sInter_mem_sets hSc) fun (s : set α) (hs : s ∈ S) => and.right (hS s hs) }

author: AurelienSaue


import lambda_calculus.utlc.basic
import lambda_calculus.utlc.reduction
import lambda_calculus.utlc.beta.church_rosser
import lambda_calculus.utlc.beta.basic

namespace lambda_calculus
namespace utlc
namespace β

local notation a `[` b `:=` c  `]` : 70 := has_substitution.substitution a b c

inductive reduction_strategy: Type
| normal: reduction_strategy
| applicative: reduction_strategy
| left: reduction_strategy → reduction_strategy
| right: reduction_strategy → reduction_strategy

def reduction_strategy_next: reduction_strategy → reduction_strategy
| (reduction_strategy.left s) := s
| (reduction_strategy.right s) := s
| s := s

def maybe_head_reduction_step: utlc → utlc
| (↓n) := ↓n
| (Λ f) := Λ f
| (f·g) := match f with
  | (↓n) := ↓n·g
  | (Λ f) := f[0:=g]
  | (f·f') := f·f'·g
  end

theorem maybe_head_reduction_step_is_eq_or_reduction_step (f: utlc):
  f = maybe_head_reduction_step f ∨ f →β (maybe_head_reduction_step f)  :=
begin
  cases f;
  simp[maybe_head_reduction_step],
  cases f_f;
  simp[maybe_head_reduction_step],
  right,
  apply lambda_dot_step_substitution
end

def strategic_head_reduction (head head' left left' right right': utlc): reduction_strategy → utlc
| reduction_strategy.normal := if ¬ head_reduced head then head' else if ¬ reduced left then left'·right else left·right'
| reduction_strategy.applicative := if ¬ reduced left then left'·right else if ¬ reduced right then left·right' else head'
| (reduction_strategy.left _) := left'·right
| (reduction_strategy.right _) := left·right'

theorem strategic_head_reduction_cases (head' left' right': utlc) (head left right: utlc) (s: reduction_strategy):
  strategic_head_reduction head head' left left' right right' s = head'
  ∨ strategic_head_reduction head head' left left' right right' s = left'·right
  ∨ strategic_head_reduction head head' left left' right right' s = left·right' :=
begin
  cases s,
  all_goals { simp[strategic_head_reduction] },
  all_goals { split_ifs },
  any_goals { simp[*] }
end

def strategic_reduction_step: utlc → reduction_strategy → utlc
| (↓n) := λ s, ↓n
| (Λ f) := λ s, Λ strategic_reduction_step f s
| (f·g) := λ s,
  strategic_head_reduction
    (f·g) (maybe_head_reduction_step (f·g))
    f (strategic_reduction_step f (reduction_strategy_next s))
    g (strategic_reduction_step g (reduction_strategy_next s))
    s

def normal_reduction_step: utlc → utlc := λf, strategic_reduction_step f reduction_strategy.normal

def applicative_reduction_step: utlc → utlc := λf, strategic_reduction_step f reduction_strategy.normal

theorem strategic_reduction_step_eq_or_reduction_step (f: utlc): ∀ strategy, f = strategic_reduction_step f strategy ∨ f →β (strategic_reduction_step f strategy) :=
begin
  intro s,
  induction f generalizing s,
  any_goals { simp [strategic_reduction_step] },
  { apply f_ih },
  obtain h|h|h := strategic_head_reduction_cases _ _ _ _ _ _ s,
  all_goals { rw[h] },
  { apply maybe_head_reduction_step_is_eq_or_reduction_step (f_f·f_g) },
  { cases f_ih_f _,
    left,
    simp,
    apply h_1,
    right,
    apply dot_step_dot_left h_1 },
  { cases f_ih_g _,
    left,
    simp,
    apply h_1,
    right,
    apply dot_step_dot_right h_1 },
end

attribute [simp] normal_reduction_step applicative_reduction_step strategic_reduction_step strategic_head_reduction maybe_head_reduction_step reduction_strategy_next

theorem reduction_of_strategic_reduction (f: utlc) (s: reduction_strategy): f ↠β strategic_reduction_step f s :=
begin
  cases strategic_reduction_step_eq_or_reduction_step f s,
  { rw [← h] },
  { exact relation.refl_trans_gen.single h}
end

theorem equiv_of_strategic_reduction (f: utlc) (s: reduction_strategy): f ≡β strategic_reduction_step f s :=
begin
  use strategic_reduction_step f s,
  refine ⟨reduction_of_strategic_reduction _ _, by refl⟩,
end

theorem equiv_of_strategic_reduction' (f: utlc) (s: reduction_strategy): strategic_reduction_step f s ≡β f :=
  equiv_symm (equiv_of_strategic_reduction _ _)

theorem trans_equiv_of_strategic_reduction {f g: utlc} {s: reduction_strategy}: strategic_reduction_step f s ≡β g → f ≡β g :=
  equiv_trans (equiv_of_strategic_reduction _ _)

theorem trans_equiv_of_strategic_reduction' {f g: utlc} {s: reduction_strategy}: f ≡β strategic_reduction_step g s → f ≡β g :=
  λ p, equiv_trans p (equiv_of_strategic_reduction' _ _)

def normal_iteration : ℕ → utlc → utlc
| 0 := λ f, f
| (n+1) := λ f, (normal_iteration n (normal_reduction_step f))

def reduction_of_normal_iterator (n: ℕ) {f : utlc}: f ↠β normal_iteration n f :=
begin
  induction n generalizing f,
  { simp [normal_iteration] },
  { simp [normal_iteration],
    apply trans _ n_ih,
    apply reduction_of_strategic_reduction }
end

theorem trans_equiv_of_normal_iteration (n: ℕ) {f g: utlc}: normal_iteration n f ≡β g → f ≡β g :=
begin
  intro p,
  cases p with x p,
  exact ⟨x, trans (reduction_of_normal_iterator _) p.left, p.right⟩
end

theorem trans_equiv_of_normal_iteration' (n: ℕ) {f g: utlc}: f ≡β normal_iteration n g → f ≡β g :=
  λ p, equiv_symm (trans_equiv_of_normal_iteration _ (equiv_symm p))

def normal_form (f g : utlc) := reduced g ∧ ∃ n, normal_iteration n f = g

end β
end utlc
end lambda_calculus


text:
import MyNat.Definition
namespace MyNat
open MyNat

/--
This theorem proves that if you add zero to a MyNat you get back the same number.
-/

theorem add_zero (a : MyNat) : a + 0 = a := by rfl

/--
This theorem proves that (a + (d + 1)) = ((a + d) + 1) for a,d in MyNat.
-/
theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl

author: leanprover


text:
variable (C : Type) [Inhabited C]

example : C := default

variable {C}

example : C := default


import data.nat.basic

theorem USAMO_Problem_2_2014 (f : ℤ -> ℤ):
(∀ x y : ℤ, (x≠0) → (x*f(2*f(y)-x) + (y^2)*f(2*x-f(y)) = f(x)^2 / x + f(y*f(y))) ) →

((∀ x : ℤ, f(x)= x^2) ∨ (∀ x : ℤ, f(x) = 0))

 := sorry


text:
import tactic
import data.vector
import data.nat.basic
--import category_theory.types

--------------------- Vector Stuff ----------------------
namespace vector
variables {A : Type*} {B : Type*} {C : Type*}

def of : A → vector A 1 := λ a, ⟨[a],rfl⟩
def of₂ : A → A → vector A 2 := λ a b, ⟨[a,b],rfl⟩
def of₃ : A → A → A → vector A 3 := λ a b c, ⟨[a,b,c],rfl⟩
def to_fn {n} : vector A n →  (fin n → A) := λ as, as.nth
def proj {m n} : (fin m → fin n) → vector A n → vector A m :=
  λ f as, of_fn (λ i, as.to_fn $ f i)
def cast {m n : ℕ} : m = n → vector A m → vector A n := λ h, eq.rec_on h
def init {m n : ℕ} : vector A (m+n) → vector A m := λ as, cast (by simp) (take m as)
def last {m n : ℕ} : vector A (m+n) → vector A n := λ as, cast (by simp) (drop m as)
def liftl {a b c : ℕ} : (vector A a → vector A b) → vector A (a + c) → vector A (b + c) :=
  λ f as, append (f as.init) as.last
def liftr {a b c : ℕ} : (vector A a → vector A b) → vector A (c + a) → vector A (c + b) :=
  λ f as, append as.init (f as.last)
def curry {n} : (vector A (n+1) → B) → (A → (vector A n → B)) :=
  λ f a as, f $ a :: as
def uncurry {n} : (A → (vector A n → B)) → (vector A (n+1) → B) :=
  λ f as, f as.head as.tail

-- Any vector can be considered as a function
instance {n} : has_coe_to_fun (vector A n) := ⟨_,λ as, as.to_fn⟩

-- lemmas around the "of" things
theorem of_0th (a : A) : (of a) 0 = a := rfl

theorem of_eq_iff (a b : A) : of a = of b ↔ a = b :=
begin
  refine ⟨λ h, _,λ h, by rw h⟩,
  rw [←of_0th a, ←of_0th b, h],
end

-- Some other useful lemmas
theorem one_eq_of (as : vector A 1) : as = of (as 0) :=
begin
  rcases as with ⟨as,h⟩,
  induction as,
  { contradiction, },
  { congr, simp only [list.length] at h,
    have : as_tl.length = 0, by exact nat.succ.inj h,
    exact list.eq_nil_of_length_eq_zero this }
end

theorem one_eq_iff (as bs : vector A 1) : as = bs ↔ as 0 = bs 0 :=
begin
  rw one_eq_of as, rw one_eq_of bs,
  unfold of,
  finish,
end

-- Map lemmas
theorem map_of (f : A → B) (a : A) : (of a).map f = of (f a) := sorry
theorem map_to_fn {m} (f : A → B) (as : vector A m) : ⇑(as.map f) = f ∘ as := sorry
theorem map_of_fn {m} (f : A → B) (as : fin m → A) : (of_fn as).map f = of_fn (f ∘ as) := sorry
theorem map_ith {m} (f : A → B) (as : vector A m) (i : fin m) : (as.map f) i = f (as i) := sorry
theorem map_proj {m n} (f : A → B) (g : fin m → fin n) (as : vector A n) :
  (as.map f).proj g = (as.proj g).map f := sorry
theorem map_init {m n} (f : A → B) (as : vector A (m+n)) :
  as.init.map f = (as.map f).init := sorry
theorem map_last {m n} (f : A → B) (as : vector A (m+n)) :
  as.last.map f = (as.map f).last := sorry
theorem map_append {m n} (f : A → B) (as : vector A m) (bs : vector A n) :
  (as.append bs).map f = (as.map f).append (bs.map f) := sorry
theorem to_fn_zero_eq_head {n} (a : A) (as : vector A n) : (a :: as) 0 = a := sorry

theorem map_map {n} (f : A → B) (g : B → C) (as : vector A n) :
  (as.map f).map g = as.map (g ∘ f) := by {cases as, unfold map, finish}

@[simp]
theorem map_id {n} (as : vector A n) : as.map id = as :=
  by {cases as, unfold map, finish}

@[simp]
theorem map_id' {n} (as : vector A n) : as.map (λ x, x) = as := by apply map_id

theorem map_to_fn_eq {n} {f g : A → B} {as : vector A n} :
  (∀ i, f (as i) = g (as i)) → as.map f = as.map g := sorry

theorem exists_rep {n} (f : A → B) (bs : vector B n) :
  function.surjective f → (∃ as : vector A n, as.map f = bs) := sorry

-- of/to_fn lemmas
theorem of_fn_to_fn {m} (as : vector A m) : vector.of_fn as = as := sorry
theorem to_fn_of_fn {m} (as : fin m → A) : (vector.of_fn as).to_fn = as := sorry
theorem eq_iff_to_fn_eq_to_fn {m} (as bs : vector A m) : as = bs ↔ ⇑as = bs := sorry

-- Stuff involving quotients and a setoid
section quotient_stuff
variable [S : setoid A]
include S

theorem rel_head {n} (a b : A) (as : vector A n) :
  (∀ i, ((a :: as) i) ≈ ((b :: as) i)) ↔ a ≈ b :=
begin
  refine ⟨λ h, _, λ h i, _⟩,
  { specialize h 0, repeat{rw to_fn_zero_eq_head at h}, assumption },
  { by_cases i = 0,
    { simpa only [h, to_fn_zero_eq_head], },
    { sorry, } }
end

theorem rel_tail {n} (a : A) (as bs : vector A n) :
  (∀ i, ((a :: as) i) ≈ ((a :: bs) i)) ↔ (∀ i, (as i) ≈ (bs i)) := sorry

def quotient_lift : Π {n} (f : vector A n → B),
  (∀ as bs : vector A n, (∀ i, as i ≈ bs i) → f as = f bs) → vector (quotient S) n → B := λ n,
  nat.rec_on n
  (λ f h _, f nil) $
  λ m ind f h, uncurry $
  λ x, quotient.lift_on x
  (λ a, ind (curry f a)
  begin
    intros as bs cond,
    change f _ = f _,
    apply h,
    rw rel_tail,
    assumption,
  end)
  begin
    intros a b cond,
    dsimp only [],
    suffices : curry f a = curry f b, by simp_rw this,
    funext,
    change f _ = f _,
    apply h,
    rw rel_head,
    assumption,
  end

theorem quotient_lift_eq : Π {n} (f : vector A n → B)
  (h : ∀ as bs : vector A n, (∀ i, as i ≈ bs i) → f as = f bs) (as : vector A n),
  quotient_lift f h (as.map quotient.mk) = f as := sorry

end quotient_stuff

end vector

namespace function

theorem epi_of_surj {X Y Z : Type*} (f : X → Y) (g1 g2 : Y → Z) :
  surjective f → g1 ∘ f = g2 ∘ f → g1 = g2 := sorry

end function

author: adamtopaz

repo: UnivAlg

save_path: github-repos/lean/adamtopaz-UnivAlg


text:
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Chris Hughes
-/
import data.polynomial.field_division
import linear_algebra.finite_dimensional
import ring_theory.adjoin.basic
import ring_theory.power_basis
import ring_theory.principal_ideal_domain

/-!
# Adjoining roots of polynomials

This file defines the commutative ring `adjoin_root f`, the ring R[X]/(f) obtained from a
commutative ring `R` and a polynomial `f : R[X]`. If furthermore `R` is a field and `f` is
irreducible, the field structure on `adjoin_root f` is constructed.

## Main definitions and results

The main definitions are in the `adjoin_root` namespace.

*  `mk f : R[X] →+* adjoin_root f`, the natural ring homomorphism.

*  `of f : R →+* adjoin_root f`, the natural ring homomorphism.

* `root f : adjoin_root f`, the image of X in R[X]/(f).

* `lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : (adjoin_root f) →+* S`, the ring
  homomorphism from R[X]/(f) to S extending `i : R →+* S` and sending `X` to `x`.

* `lift_hom (x : S) (hfx : aeval x f = 0) : adjoin_root f →ₐ[R] S`, the algebra
  homomorphism from R[X]/(f) to S extending `algebra_map R S` and sending `X` to `x`

* `equiv : (adjoin_root f →ₐ[F] E) ≃ {x // x ∈ (f.map (algebra_map F E)).roots}` a
  bijection between algebra homomorphisms from `adjoin_root` and roots of `f` in `S`

-/
noncomputable theory
open_locale classical
open_locale big_operators polynomial

universes u v w

variables {R : Type u} {S : Type v} {K : Type w}

open polynomial ideal

/-- Adjoin a root of a polynomial `f` to a commutative ring `R`. We define the new ring
as the quotient of `polynomial R` by the principal ideal generated by `f`. -/
def adjoin_root [comm_ring R] (f : R[X]) : Type u :=
polynomial R ⧸ (span {f} : ideal R[X])

namespace adjoin_root

section comm_ring
variables [comm_ring R] (f : R[X])

instance : comm_ring (adjoin_root f) := ideal.quotient.comm_ring _

instance : inhabited (adjoin_root f) := ⟨0⟩

instance : decidable_eq (adjoin_root f) := classical.dec_eq _

/-- Ring homomorphism from `R[x]` to `adjoin_root f` sending `X` to the `root`. -/
def mk : R[X] →+* adjoin_root f := ideal.quotient.mk _

@[elab_as_eliminator]
theorem induction_on {C : adjoin_root f → Prop} (x : adjoin_root f)
  (ih : ∀ p : R[X], C (mk f p)) : C x :=
quotient.induction_on' x ih

/-- Embedding of the original ring `R` into `adjoin_root f`. -/
def of : R →+* adjoin_root f := (mk f).comp C

instance [comm_semiring S] [algebra S R] : algebra S (adjoin_root f) :=
ideal.quotient.algebra S

instance [comm_semiring S] [comm_semiring K] [has_scalar S K] [algebra S R] [algebra K R]
  [is_scalar_tower S K R] :
  is_scalar_tower S K (adjoin_root f) :=
submodule.quotient.is_scalar_tower _ _

instance [comm_semiring S] [comm_semiring K] [algebra S R] [algebra K R] [smul_comm_class S K R] :
  smul_comm_class S K (adjoin_root f) :=
submodule.quotient.smul_comm_class _ _

@[simp]

variables (S)

lemma algebra_map_eq' [comm_semiring S] [algebra S R] :
  algebra_map S (adjoin_root f) = (of f).comp (algebra_map S R) := rfl

variables {S}

/-- The adjoined root. -/
def root : adjoin_root f := mk f X

variables {f}

instance adjoin_root.has_coe_t : has_coe_t R (adjoin_root f) := ⟨of f⟩

@[simp] lemma mk_eq_mk {g h : R[X]} : mk f g = mk f h ↔ f ∣ g - h :=
ideal.quotient.eq.trans ideal.mem_span_singleton

@[simp] lemma mk_self : mk f f = 0 :=
quotient.sound' (mem_span_singleton.2 $ by simp)

@[simp] lemma mk_C (x : R) : mk f (C x) = x := rfl

@[simp] lemma mk_X : mk f X = root f := rfl

@[simp] lemma aeval_eq (p : R[X]) : aeval (root f) p = mk f p :=
polynomial.induction_on p (λ x, by { rw aeval_C, refl })
  (λ p q ihp ihq, by rw [alg_hom.map_add, ring_hom.map_add, ihp, ihq])
  (λ n x ih, by { rw [alg_hom.map_mul, aeval_C, alg_hom.map_pow, aeval_X,
    ring_hom.map_mul, mk_C, ring_hom.map_pow, mk_X], refl })

theorem adjoin_root_eq_top : algebra.adjoin R ({root f} : set (adjoin_root f)) = ⊤ :=
algebra.eq_top_iff.2 $ λ x, induction_on f x $ λ p,
(algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

@[simp] lemma eval₂_root (f : R[X]) : f.eval₂ (of f) (root f) = 0 :=
by rw [← algebra_map_eq, ← aeval_def, aeval_eq, mk_self]

lemma is_root_root (f : R[X]) : is_root (f.map (of f)) (root f) :=
by rw [is_root, eval_map, eval₂_root]

lemma is_algebraic_root (hf : f ≠ 0) : is_algebraic R (root f) :=
⟨f, hf, eval₂_root f⟩

variables [comm_ring S]

/-- Lift a ring homomorphism `i : R →+* S` to `adjoin_root f →+* S`. -/
def lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : (adjoin_root f) →+* S :=
begin
  apply ideal.quotient.lift _ (eval₂_ring_hom i x),
  intros g H,
  rcases mem_span_singleton.1 H with ⟨y, hy⟩,
  rw [hy, ring_hom.map_mul, coe_eval₂_ring_hom, h, zero_mul]
end

variables {i : R →+* S} {a : S} (h : f.eval₂ i a = 0)

@[simp] lemma lift_mk (g : R[X]) : lift i a h (mk f g) = g.eval₂ i a :=
ideal.quotient.lift_mk _ _ _

@[simp] lemma lift_root : lift i a h (root f) = a := by rw [root, lift_mk, eval₂_X]

@[simp] lemma lift_of {x : R} : lift i a h x = i x :=
by rw [← mk_C x, lift_mk, eval₂_C]

@[simp] lemma lift_comp_of : (lift i a h).comp (of f) = i :=
ring_hom.ext $ λ _, @lift_of _ _ _ _ _ _ _ h _

variables (f) [algebra R S]

/-- Produce an algebra homomorphism `adjoin_root f →ₐ[R] S` sending `root f` to
a root of `f` in `S`. -/
def lift_hom (x : S) (hfx : aeval x f = 0) : adjoin_root f →ₐ[R] S :=
{ commutes' := λ r, show lift _ _ hfx r = _, from lift_of hfx,
  .. lift (algebra_map R S) x hfx }

@[simp] lemma coe_lift_hom (x : S) (hfx : aeval x f = 0) :
  (lift_hom f x hfx : adjoin_root f →+* S) = lift (algebra_map R S) x hfx := rfl

@[simp] lemma aeval_alg_hom_eq_zero (ϕ : adjoin_root f →ₐ[R] S) : aeval (ϕ (root f)) f = 0 :=
begin
  have h : ϕ.to_ring_hom.comp (of f) = algebra_map R S := ring_hom.ext_iff.mpr (ϕ.commutes),
  rw [aeval_def, ←h, ←ring_hom.map_zero ϕ.to_ring_hom, ←eval₂_root f, hom_eval₂],
  refl,
end

@[simp] lemma lift_hom_eq_alg_hom (f : R[X]) (ϕ : adjoin_root f →ₐ[R] S) :
  lift_hom f (ϕ (root f)) (aeval_alg_hom_eq_zero f ϕ) = ϕ :=
begin
  suffices : ϕ.equalizer (lift_hom f (ϕ (root f)) (aeval_alg_hom_eq_zero f ϕ)) = ⊤,
  { exact (alg_hom.ext (λ x, (set_like.ext_iff.mp (this) x).mpr algebra.mem_top)).symm },
  rw [eq_top_iff, ←adjoin_root_eq_top, algebra.adjoin_le_iff, set.singleton_subset_iff],
  exact (@lift_root _ _ _ _ _ _ _ (aeval_alg_hom_eq_zero f ϕ)).symm,
end

variables (hfx : aeval a f = 0)

@[simp] lemma lift_hom_mk {g : R[X]} : lift_hom f a hfx (mk f g) = aeval a g :=
lift_mk hfx g

@[simp] lemma lift_hom_root : lift_hom f a hfx (root f) = a :=
lift_root hfx

@[simp] lemma lift_hom_of {x : R} : lift_hom f a hfx (of f x) = algebra_map _ _ x :=
lift_of hfx

end comm_ring

section irreducible

variables [field K] {f : K[X]} [irreducible f]

instance is_maximal_span : is_maximal (span {f} : ideal K[X]) :=
principal_ideal_ring.is_maximal_of_irreducible ‹irreducible f›

noncomputable instance field : field (adjoin_root f) :=
{ ..adjoin_root.comm_ring f,
  ..ideal.quotient.field (span {f} : ideal K[X]) }

lemma coe_injective : function.injective (coe : K → adjoin_root f) :=
(of f).injective

variable (f)

lemma mul_div_root_cancel :
  ((X - C (root f)) * (f.map (of f) / (X - C (root f))) : polynomial (adjoin_root f)) =
    f.map (of f) :=
mul_div_eq_iff_is_root.2 $ is_root_root _

end irreducible

section power_basis

variables [comm_ring R] {g : R[X]}

lemma is_integral_root' (hg : g.monic) : is_integral R (root g) :=
⟨g, hg, eval₂_root g⟩

/-- `adjoin_root.mod_by_monic_hom` sends the equivalence class of `f` mod `g` to `f %ₘ g`.

This is a well-defined right inverse to `adjoin_root.mk`, see `adjoin_root.mk_left_inverse`. -/
def mod_by_monic_hom (hg : g.monic) :
  adjoin_root g →ₗ[R] R[X] :=
(submodule.liftq _ (polynomial.mod_by_monic_hom g)
  (λ f (hf : f ∈ (ideal.span {g}).restrict_scalars R),
    (mem_ker_mod_by_monic hg).mpr (ideal.mem_span_singleton.mp hf))).comp $
(submodule.quotient.restrict_scalars_equiv R (ideal.span {g} : ideal R[X]))
  .symm.to_linear_map

@[simp] lemma mod_by_monic_hom_mk (hg : g.monic) (f : R[X]) :
  mod_by_monic_hom hg (mk g f) = f %ₘ g := rfl

lemma mk_left_inverse (hg : g.monic) :
  function.left_inverse (mk g) (mod_by_monic_hom hg) :=
λ f, induction_on g f $ λ f, begin
  rw [mod_by_monic_hom_mk hg, mk_eq_mk, mod_by_monic_eq_sub_mul_div _ hg,
      sub_sub_cancel_left, dvd_neg],
  apply dvd_mul_right
end

lemma mk_surjective (hg : g.monic) : function.surjective (mk g) :=
(mk_left_inverse hg).surjective

/-- The elements `1, root g, ..., root g ^ (d - 1)` form a basis for `adjoin_root g`,
where `g` is a monic polynomial of degree `d`. -/
@[simps] def power_basis_aux' (hg : g.monic) :
  basis (fin g.nat_degree) R (adjoin_root g) :=
basis.of_equiv_fun
{ to_fun := λ f i, (mod_by_monic_hom hg f).coeff i,
  inv_fun := λ c, mk g $ ∑ (i : fin g.nat_degree), monomial i (c i),
  map_add' := λ f₁ f₂, funext $ λ i,
    by simp only [(mod_by_monic_hom hg).map_add, coeff_add, pi.add_apply],
  map_smul' := λ f₁ f₂, funext $ λ i,
    by simp only [(mod_by_monic_hom hg).map_smul, coeff_smul, pi.smul_apply, ring_hom.id_apply],
  left_inv := λ f, induction_on g f (λ f, eq.symm $ mk_eq_mk.mpr $
    by { simp only [mod_by_monic_hom_mk, sum_mod_by_monic_coeff hg degree_le_nat_degree],
         rw [mod_by_monic_eq_sub_mul_div _ hg, sub_sub_cancel],
         exact dvd_mul_right _ _ }),
  right_inv := λ x, funext $ λ i, begin
    nontriviality R,
    simp only [mod_by_monic_hom_mk],
    rw [(mod_by_monic_eq_self_iff hg).mpr, finset_sum_coeff, finset.sum_eq_single i];
      try { simp only [coeff_monomial, eq_self_iff_true, if_true] },
    { intros j _ hj, exact if_neg (fin.coe_injective.ne hj) },
    { intros, have := finset.mem_univ i, contradiction },
    { refine (degree_sum_le _ _).trans_lt ((finset.sup_lt_iff _).mpr (λ j _, _)),
      { exact bot_lt_iff_ne_bot.mpr (mt degree_eq_bot.mp hg.ne_zero) },
      { refine (degree_monomial_le _ _).trans_lt _,
        rw [degree_eq_nat_degree hg.ne_zero, with_bot.coe_lt_coe],
        exact j.2 } },
  end}

/-- The power basis `1, root g, ..., root g ^ (d - 1)` for `adjoin_root g`,
where `g` is a monic polynomial of degree `d`. -/
@[simps] def power_basis' (hg : g.monic) : power_basis R (adjoin_root g) :=
{ gen := root g,
  dim := g.nat_degree,
  basis := power_basis_aux' hg,
  basis_eq_pow := λ i, begin
    simp only [power_basis_aux', basis.coe_of_equiv_fun, linear_equiv.coe_symm_mk],
    rw finset.sum_eq_single i,
    { rw [function.update_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X] },
    { intros j _ hj,
      rw ← monomial_zero_right _,
      convert congr_arg _ (function.update_noteq hj _ _) }, -- Fix `decidable_eq` mismatch
    { intros, have := finset.mem_univ i, contradiction },
  end}

variables [field K] {f : K[X]}

lemma is_integral_root (hf : f ≠ 0) : is_integral K (root f) :=
is_algebraic_iff_is_integral.mp (is_algebraic_root hf)

lemma minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C (f.leading_coeff⁻¹) :=
begin
  have f'_monic : monic _ := monic_mul_leading_coeff_inv hf,
  refine (minpoly.unique K _ f'_monic _ _).symm,
  { rw [alg_hom.map_mul, aeval_eq, mk_self, zero_mul] },
  intros q q_monic q_aeval,
  have commutes : (lift (algebra_map K (adjoin_root f)) (root f) q_aeval).comp (mk q) = mk f,
  { ext,
    { simp only [ring_hom.comp_apply, mk_C, lift_of], refl },
    { simp only [ring_hom.comp_apply, mk_X, lift_root] } },
  rw [degree_eq_nat_degree f'_monic.ne_zero, degree_eq_nat_degree q_monic.ne_zero,
      with_bot.coe_le_coe, nat_degree_mul hf, nat_degree_C, add_zero],
  apply nat_degree_le_of_dvd,
  { have : mk f q = 0, by rw [←commutes, ring_hom.comp_apply, mk_self, ring_hom.map_zero],
    rwa [←ideal.mem_span_singleton, ←ideal.quotient.eq_zero_iff_mem] },
  { exact q_monic.ne_zero },
  { rwa [ne.def, C_eq_zero, inv_eq_zero, leading_coeff_eq_zero] },
end

/-- The elements `1, root f, ..., root f ^ (d - 1)` form a basis for `adjoin_root f`,
where `f` is an irreducible polynomial over a field of degree `d`. -/
def power_basis_aux (hf : f ≠ 0) : basis (fin f.nat_degree) K (adjoin_root f) :=
begin
  set f' := f * C (f.leading_coeff⁻¹) with f'_def,
  have deg_f' : f'.nat_degree = f.nat_degree,
  { rw [nat_degree_mul hf, nat_degree_C, add_zero],
    { rwa [ne.def, C_eq_zero, inv_eq_zero, leading_coeff_eq_zero] } },
  have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf,
  apply @basis.mk _ _ _ (λ (i : fin f.nat_degree), (root f ^ i.val)),
  { rw [← deg_f', ← minpoly_eq],
    exact (is_integral_root hf).linear_independent_pow },
  { rw _root_.eq_top_iff,
    rintros y -,
    rw [← deg_f', ← minpoly_eq],
    apply (is_integral_root hf).mem_span_pow,
    obtain ⟨g⟩ := y,
    use g,
    rw aeval_eq,
    refl }
end

/-- The power basis `1, root f, ..., root f ^ (d - 1)` for `adjoin_root f`,
where `f` is an irreducible polynomial over a field of degree `d`. -/
@[simps] def power_basis (hf : f ≠ 0) :
  power_basis K (adjoin_root f) :=
{ gen := root f,
  dim := f.nat_degree,
  basis := power_basis_aux hf,
  basis_eq_pow := basis.mk_apply _ _ }

lemma minpoly_power_basis_gen (hf : f ≠ 0) :
  minpoly K (power_basis hf).gen = f * C (f.leading_coeff⁻¹) :=
by rw [power_basis_gen, minpoly_root hf]

lemma minpoly_power_basis_gen_of_monic (hf : f.monic) (hf' : f ≠ 0 := hf.ne_zero) :
  minpoly K (power_basis hf').gen = f :=
by rw [minpoly_power_basis_gen hf', hf.leading_coeff, inv_one, C.map_one, mul_one]

end power_basis

section equiv

section is_domain

variables [comm_ring R] [is_domain R] [comm_ring S] [is_domain S] [algebra R S]
variables (g : R[X]) (pb : _root_.power_basis R S)

/-- If `S` is an extension of `R` with power basis `pb` and `g` is a monic polynomial over `R`
such that `pb.gen` has a minimal polynomial `g`, then `S` is isomorphic to `adjoin_root g`.

Compare `power_basis.equiv_of_root`, which would require
`h₂ : aeval pb.gen (minpoly R (root g)) = 0`; that minimal polynomial is not
guaranteed to be identical to `g`. -/
@[simps {fully_applied := ff}]
def equiv' (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
  adjoin_root g ≃ₐ[R] S :=
{ to_fun := adjoin_root.lift_hom g pb.gen h₂,
  inv_fun := pb.lift (root g) h₁,
  left_inv := λ x, induction_on g x $ λ f, by rw [lift_hom_mk, pb.lift_aeval, aeval_eq],
  right_inv := λ x, begin
    obtain ⟨f, hf, rfl⟩ := pb.exists_eq_aeval x,
    rw [pb.lift_aeval, aeval_eq, lift_hom_mk]
  end,
  .. adjoin_root.lift_hom g pb.gen h₂ }

@[simp] lemma equiv'_to_alg_hom
  (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
  (equiv' g pb h₁ h₂).to_alg_hom = adjoin_root.lift_hom g pb.gen h₂ :=
rfl

@[simp] lemma equiv'_symm_to_alg_hom
  (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
  (equiv' g pb h₁ h₂).symm.to_alg_hom = pb.lift (root g) h₁ :=
rfl

end is_domain

section field

variables (K) (L F : Type*) [field F] [field K] [field L] [algebra F K] [algebra F L]
variables (pb : _root_.power_basis F K)

/-- If `L` is a field extension of `F` and `f` is a polynomial over `F` then the set
of maps from `F[x]/(f)` into `L` is in bijection with the set of roots of `f` in `L`. -/
def equiv (f : F[X]) (hf : f ≠ 0) :
  (adjoin_root f →ₐ[F] L) ≃ {x // x ∈ (f.map (algebra_map F L)).roots} :=
(power_basis hf).lift_equiv'.trans ((equiv.refl _).subtype_equiv (λ x,
  begin
    rw [power_basis_gen, minpoly_root hf, polynomial.map_mul, roots_mul,
        polynomial.map_C, roots_C, add_zero, equiv.refl_apply],
    { rw ← polynomial.map_mul, exact map_monic_ne_zero (monic_mul_leading_coeff_inv hf) }
  end))

end field

end equiv

section

open ideal double_quot polynomial

variables [comm_ring R] (I : ideal R) (f : polynomial R)

/-- The natural isomorphism `R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f))` for `α` a root of
`f : polynomial R` and `I : ideal R`.

See `adjoin_root.quot_map_of_equiv` for the isomorphism with `(R/I)[X] / (f mod I)`. -/
def quot_map_of_equiv_quot_map_C_map_span_mk :
  adjoin_root f ⧸ I.map (of f) ≃+* adjoin_root f ⧸ (I.map C).map (span {f})^.quotient.mk :=
ideal.quot_equiv_of_eq (by rw [of, adjoin_root.mk, ideal.map_map])

@[simp]
lemma quot_map_of_equiv_quot_map_C_map_span_mk_mk (x : adjoin_root f) :
  quot_map_of_equiv_quot_map_C_map_span_mk I f (ideal.quotient.mk (I.map (of f)) x) =
    ideal.quotient.mk _ x :=
rfl

/-- The natural isomorphism `R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x])`
  for `α` a root of `f : polynomial R` and `I : ideal R`-/
def quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk :
  (adjoin_root f) ⧸ ((I.map (C : R →+* R[X]))).map (span {f})^.quotient.mk ≃+*
    (R[X] ⧸ map C I) ⧸ (span {f}).map (I.map C)^.quotient.mk :=
quot_quot_equiv_comm (span ({f} : set (polynomial R))) (I.map (C : R →+* polynomial R))

@[simp]
lemma quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk_mk (p : R[X]) :
  quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f (ideal.quotient.mk _ (mk f p)) =
    quot_quot_mk (I.map C) (span {f}) p :=
rfl

/-- The natural isomorphism `(R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x])` where
  `f : polynomial R` and `I : ideal R`-/
def polynomial.quot_quot_equiv_comm :
  (R ⧸ I)[X] ⧸ span ({f.map (I^.quotient.mk)} : set (polynomial (R ⧸ I))) ≃+*
    (R[X] ⧸ map C I) ⧸ span ({(ideal.quotient.mk (I.map C)) f} : set (R[X] ⧸ map C I)) :=
quotient_equiv (span ({f.map (I^.quotient.mk)} : set (polynomial (R ⧸ I))))
  (span {ideal.quotient.mk (I.map polynomial.C) f})
  (polynomial_quotient_equiv_quotient_polynomial I)
  (by rw [map_span, set.image_singleton, ring_equiv.coe_to_ring_hom,
    polynomial_quotient_equiv_quotient_polynomial_map_mk I f])

@[simp]
lemma polynomial.quot_quot_equiv_comm_mk_mk (p : R[X]) :
  (polynomial.quot_quot_equiv_comm I f).symm (ideal.quotient.mk _ (ideal.quotient.mk _ p)) =
    (ideal.quotient.mk  _ (p.map I^.quotient.mk)) :=
by simp only [polynomial.quot_quot_equiv_comm, quotient_equiv_symm_mk,
  polynomial_quotient_equiv_quotient_polynomial_symm_mk]

/-- The natural isomorphism `R[α]/I[α] ≅ (R/I)[X]/(f mod I)` for `α` a root of `f : polynomial R`
  and `I : ideal R`-/
def quot_map_of_equiv : (adjoin_root f) ⧸ (I.map (of f)) ≃+*
  polynomial (R ⧸ I) ⧸ (span ({f.map (I^.quotient.mk)} : set (polynomial (R ⧸ I)))) :=
(quot_map_of_equiv_quot_map_C_map_span_mk I f).trans
  ((quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f).trans
  ((ideal.quot_equiv_of_eq
  (show (span ({f} : set (polynomial R))).map (I.map (C : R →+* polynomial R))^.quotient.mk =
    span ({(ideal.quotient.mk (I.map polynomial.C)) f} : set (polynomial R ⧸ map C I)),
    from by rw [map_span, set.image_singleton])).trans
  (polynomial.quot_quot_equiv_comm I f).symm))

@[simp]
lemma quot_adjoin_root_equiv_quot_polynomial_quot_mk_of (p : R[X]) :
  quot_map_of_equiv I f (ideal.quotient.mk (I.map (of f)) (mk f p)) =
    ideal.quotient.mk (span ({f.map (I^.quotient.mk)} : set (polynomial (R ⧸ I))))
    (p.map I^.quotient.mk) :=
by rw [quot_map_of_equiv, ring_equiv.trans_apply, ring_equiv.trans_apply, ring_equiv.trans_apply,
    quot_map_of_equiv_quot_map_C_map_span_mk_mk,
    quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk_mk,quot_quot_mk, ring_hom.comp_apply,
    quot_equiv_of_eq_mk, polynomial.quot_quot_equiv_comm_mk_mk]

end

end adjoin_root

author: saisurbehera

repo: mathProof


text:
/-
Copyright (c) 2017 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
-/
import category_theory.equivalence
import order.hom.basic

/-!

# Preorders as categories

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

We install a category instance on any preorder. This is not to be confused with the category _of_
preorders, defined in `order/category/Preorder`.

We show that monotone functions between preorders correspond to functors of the associated
categories.

## Main definitions

* `hom_of_le` and `le_of_hom` provide translations between inequalities in the preorder, and
  morphisms in the associated category.
* `monotone.functor` is the functor associated to a monotone function.

-/

universes u v

namespace preorder

open category_theory

/--
The category structure coming from a preorder. There is a morphism `X ⟶ Y` if and only if `X ≤ Y`.

Because we don't allow morphisms to live in `Prop`,
we have to define `X ⟶ Y` as `ulift (plift (X ≤ Y))`.
See `category_theory.hom_of_le` and `category_theory.le_of_hom`.

See <https://stacks.math.columbia.edu/tag/00D3>.
-/
@[priority 100] -- see Note [lower instance priority]
instance small_category (α : Type u) [preorder α] : small_category α :=
{ hom  := λ U V, ulift (plift (U ≤ V)),
  id   := λ X, ⟨ ⟨ le_refl X ⟩ ⟩,
  comp := λ X Y Z f g, ⟨ ⟨ le_trans _ _ _ f.down.down g.down.down ⟩ ⟩ }

end preorder

namespace category_theory

open opposite

variables {X : Type u} [preorder X]

/--
Express an inequality as a morphism in the corresponding preorder category.
-/
def hom_of_le {x y : X} (h : x ≤ y) : x ⟶ y := ulift.up (plift.up h)

alias hom_of_le ← _root_.has_le.le.hom

@[simp] lemma hom_of_le_refl {x : X} : (le_refl x).hom = 𝟙 x := rfl
@[simp] lemma hom_of_le_comp {x y z : X} (h : x ≤ y) (k : y ≤ z) :
  h.hom ≫ k.hom = (h.trans k).hom := rfl

/--
Extract the underlying inequality from a morphism in a preorder category.
-/
lemma le_of_hom {x y : X} (h : x ⟶ y) : x ≤ y := h.down.down

alias le_of_hom ← _root_.quiver.hom.le

@[simp] lemma le_of_hom_hom_of_le {x y : X} (h : x ≤ y) : h.hom.le = h := rfl
@[simp] lemma hom_of_le_le_of_hom {x y : X} (h : x ⟶ y) : h.le.hom = h :=
by { cases h, cases h, refl, }

/-- Construct a morphism in the opposite of a preorder category from an inequality. -/
def op_hom_of_le {x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x := h.hom.op

lemma le_of_op_hom {x y : Xᵒᵖ} (h : x ⟶ y) : unop y ≤ unop x := h.unop.le

instance unique_to_top [order_top X] {x : X} : unique (x ⟶ ⊤) := by tidy
instance unique_from_bot [order_bot X] {x : X} : unique (⊥ ⟶ x) := by tidy

end category_theory

section

variables {X : Type u} {Y : Type v} [preorder X] [preorder Y]

/--
A monotone function between preorders induces a functor between the associated categories.
-/
def monotone.functor {f : X → Y} (h : monotone f) : X ⥤ Y :=
{ obj := f,
  map := λ x₁ x₂ g, (h g.le).hom }

@[simp] lemma monotone.functor_obj {f : X → Y} (h : monotone f) : h.functor.obj = f := rfl

end

namespace category_theory

section preorder

variables {X : Type u} {Y : Type v} [preorder X] [preorder Y]

/--
A functor between preorder categories is monotone.
-/
@[mono] lemma functor.monotone (f : X ⥤ Y) : monotone f.obj :=
λ x y hxy, (f.map hxy.hom).le

end preorder

section partial_order

variables {X : Type u} {Y : Type v} [partial_order X] [partial_order Y]

lemma iso.to_eq {x y : X} (f : x ≅ y) : x = y := le_antisymm f.hom.le f.inv.le

/--
A categorical equivalence between partial orders is just an order isomorphism.
-/
def equivalence.to_order_iso (e : X ≌ Y) : X ≃o Y :=
{ to_fun := e.functor.obj,
  inv_fun := e.inverse.obj,
  left_inv := λ a, (e.unit_iso.app a).to_eq.symm,
  right_inv := λ b, (e.counit_iso.app b).to_eq,
  map_rel_iff' := λ a a',
    ⟨λ h, ((equivalence.unit e).app a ≫ e.inverse.map h.hom ≫ (equivalence.unit_inv e).app a').le,
     λ (h : a ≤ a'), (e.functor.map h.hom).le⟩, }

-- `@[simps]` on `equivalence.to_order_iso` produces lemmas that fail the `simp_nf` linter,
-- so we provide them by hand:
@[simp]

@[simp]
lemma equivalence.to_order_iso_symm_apply (e : X ≌ Y) (y : Y) :
  e.to_order_iso.symm y = e.inverse.obj y := rfl

end partial_order

end category_theory

author: leanprover-community

repo: mathlib