import algebra.smul_with_zero

import group_theory.group_action.group

import tactic.abel

open function

universes u v

variables {α R k S M M₂ M₃ ι : Type*}

@[ext, protect_proj] class module (R : Type u) (M : Type v) [semiring R]

[add_comm_monoid M] extends distrib_mul_action R M :=

(add_smul : ∀(r s : R) (x : M), (r + s) • x = r • x + s • x)

(zero_smul : ∀x : M, (0 : R) • x = 0)

section add_comm_monoid

variables [semiring R] [add_comm_monoid M] [module R M] (r s : R) (x y : M)

@[priority 100] -- see Note [lower instance priority]

instance module.to_mul_action_with_zero :

mul_action_with_zero R M :=

{ smul_zero := smul_zero,

zero_smul := module.zero_smul,

..(infer_instance : mul_action R M) }

instance add_comm_monoid.nat_module : module ℕ M :=

{ one_smul := one_nsmul,

mul_smul := λ m n a, mul_nsmul a m n,

smul_add := λ n a b, nsmul_add a b n,

smul_zero := nsmul_zero,

zero_smul := zero_nsmul,

add_smul := λ r s x, add_nsmul x r s }

lemma add_monoid.End.nat_cast_def (n : ℕ) :

(↑n : add_monoid.End M) = distrib_mul_action.to_add_monoid_End ℕ M n := rfl

theorem add_smul : (r + s) • x = r • x + s • x := module.add_smul r s x

lemma convex.combo_self {a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x :=

by rw [←add_smul, h, one_smul]

variables (R)

theorem two_smul : (2 : R) • x = x + x := by rw [bit0, add_smul, one_smul]

theorem two_smul' : (2 : R) • x = bit0 x := two_smul R x

@[simp] lemma inv_of_two_smul_add_inv_of_two_smul [invertible (2 : R)] (x : M) :

(⅟2 : R) • x + (⅟2 : R) • x = x :=

convex.combo_self inv_of_two_add_inv_of_two _

protected def function.injective.module [add_comm_monoid M₂] [has_smul R M₂] (f : M₂ →+ M)

(hf : injective f) (smul : ∀ (c : R) x, f (c • x) = c • f x) :

module R M₂ :=

{ smul := (•),

add_smul := λ c₁ c₂ x, hf $ by simp only [smul, f.map_add, add_smul],

zero_smul := λ x, hf $ by simp only [smul, zero_smul, f.map_zero],

.. hf.distrib_mul_action f smul }

protected def function.surjective.module [add_comm_monoid M₂] [has_smul R M₂] (f : M →+ M₂)

(hf : surjective f) (smul : ∀ (c : R) x, f (c • x) = c • f x) :

module R M₂ :=

{ smul := (•),

add_smul := λ c₁ c₂ x, by { rcases hf x with ⟨x, rfl⟩,

simp only [add_smul, ← smul, ← f.map_add] },

zero_smul := λ x, by { rcases hf x with ⟨x, rfl⟩, simp only [← f.map_zero, ← smul, zero_smul] },

.. hf.distrib_mul_action f smul }

def function.surjective.module_left {R S M : Type*} [semiring R] [add_comm_monoid M]

[module R M] [semiring S] [has_smul S M]

(f : R →+* S) (hf : function.surjective f) (hsmul : ∀ c (x : M), f c • x = c • x) :

module S M :=

{ smul := (•),

zero_smul := λ x, by rw [← f.map_zero, hsmul, zero_smul],

add_smul := hf.forall₂.mpr (λ a b x, by simp only [← f.map_add, hsmul, add_smul]),

.. hf.distrib_mul_action_left f.to_monoid_hom hsmul }

variables {R} (M)

@[reducible] def module.comp_hom [semiring S] (f : S →+* R) :

module S M :=

{ smul := has_smul.comp.smul f,

add_smul := λ r s x, by simp [add_smul],

.. mul_action_with_zero.comp_hom M f.to_monoid_with_zero_hom,

.. distrib_mul_action.comp_hom M (f : S →* R) }

variables (R) (M)

def module.to_add_monoid_End : R →+* add_monoid.End M :=

{ map_zero' := add_monoid_hom.ext $ λ r, by simp,

map_add' := λ x y, add_monoid_hom.ext $ λ r, by simp [add_smul],

..distrib_mul_action.to_add_monoid_End R M }

def smul_add_hom : R →+ M →+ M :=

(module.to_add_monoid_End R M).to_add_monoid_hom

variables {R M}

@[simp] lemma smul_add_hom_apply (r : R) (x : M) :

smul_add_hom R M r x = r • x := rfl

lemma module.eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0 :=

by rw [←one_smul R x, ←zero_eq_one, zero_smul]

@[simp] lemma smul_add_one_sub_smul {R : Type*} [ring R] [module R M]

{r : R} {m : M} : r • m + (1 - r) • m = m :=

by rw [← add_smul, add_sub_cancel'_right, one_smul]

end add_comm_monoid

variables (R)

def module.add_comm_monoid_to_add_comm_group [ring R] [add_comm_monoid M] [module R M] :

add_comm_group M :=

{ neg := λ a, (-1 : R) • a,

add_left_neg := λ a, show (-1 : R) • a + a = 0, by

{ nth_rewrite 1 ← one_smul _ a,

rw [← add_smul, add_left_neg, zero_smul] },

..(infer_instance : add_comm_monoid M), }

variables {R}

section add_comm_group

variables (R M) [semiring R] [add_comm_group M]

instance add_comm_group.int_module : module ℤ M :=

{ one_smul := one_zsmul,

mul_smul := λ m n a, mul_zsmul a m n,

smul_add := λ n a b, zsmul_add a b n,

smul_zero := zsmul_zero,

zero_smul := zero_zsmul,

add_smul := λ r s x, add_zsmul x r s }

lemma add_monoid.End.int_cast_def (z : ℤ) :

(↑z : add_monoid.End M) = distrib_mul_action.to_add_monoid_End ℤ M z := rfl

structure module.core extends has_smul R M :=

(smul_add : ∀(r : R) (x y : M), r • (x + y) = r • x + r • y)

(add_smul : ∀(r s : R) (x : M), (r + s) • x = r • x + s • x)

(mul_smul : ∀(r s : R) (x : M), (r * s) • x = r • s • x)

(one_smul : ∀x : M, (1 : R) • x = x)

variables {R M}

def module.of_core (H : module.core R M) : module R M :=

by letI := H.to_has_smul; exact

{ zero_smul := λ x, (add_monoid_hom.mk' (λ r : R, r • x) (λ r s, H.add_smul r s x)).map_zero,

smul_zero := λ r, (add_monoid_hom.mk' ((•) r) (H.smul_add r)).map_zero,

..H }

lemma convex.combo_eq_smul_sub_add [module R M] {x y : M} {a b : R} (h : a + b = 1) :

a • x + b • y = b • (y - x) + x :=

a • x + b • y = (b • y - b • x) + (a • x + b • x) : by abel

... = b • (y - x) + x : by rw [smul_sub, convex.combo_self h]

end add_comm_group

lemma module.ext' {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M] (P Q : module R M)

(w : ∀ (r : R) (m : M), by { haveI := P, exact r • m } = by { haveI := Q, exact r • m }) :

P = Q :=

ext,

exact w _ _

section module

variables [ring R] [add_comm_group M] [module R M] (r s : R) (x y : M)

@[simp] theorem neg_smul : -r • x = - (r • x) :=

eq_neg_of_add_eq_zero_left $ by rw [← add_smul, add_left_neg, zero_smul]

@[simp] lemma neg_smul_neg : -r • -x = r • x :=

by rw [neg_smul, smul_neg, neg_neg]

@[simp] theorem units.neg_smul (u : Rˣ) (x : M) : -u • x = - (u • x) :=

by rw [units.smul_def, units.coe_neg, neg_smul, units.smul_def]

variables (R)

theorem neg_one_smul (x : M) : (-1 : R) • x = -x := by simp

variables {R}

theorem sub_smul (r s : R) (y : M) : (r - s) • y = r • y - s • y :=

by simp [add_smul, sub_eq_add_neg]

end module

protected theorem module.subsingleton (R M : Type*) [semiring R] [subsingleton R]

[add_comm_monoid M] [module R M] :

subsingleton M :=

mul_action_with_zero.subsingleton R M

protected theorem module.nontrivial (R M : Type*) [semiring R] [nontrivial M] [add_comm_monoid M]

[module R M] :

nontrivial R :=

mul_action_with_zero.nontrivial R M

@[priority 910] -- see Note [lower instance priority]

instance semiring.to_module [semiring R] : module R R :=

{ smul_add := mul_add,

add_smul := add_mul,

zero_smul := zero_mul,

smul_zero := mul_zero }

@[priority 910] -- see Note [lower instance priority]

instance semiring.to_opposite_module [semiring R] : module Rᵐᵒᵖ R :=

{ smul_add := λ r x y, add_mul _ _ _,

add_smul := λ r x y, mul_add _ _ _,

..monoid_with_zero.to_opposite_mul_action_with_zero R}

def ring_hom.to_module [semiring R] [semiring S] (f : R →+* S) : module R S :=

module.comp_hom S f

instance ring_hom.apply_distrib_mul_action [semiring R] : distrib_mul_action (R →+* R) R :=

{ smul := ($),

smul_zero := ring_hom.map_zero,

smul_add := ring_hom.map_add,

one_smul := λ _, rfl,

mul_smul := λ _ _ _, rfl }

@[simp] protected lemma ring_hom.smul_def [semiring R] (f : R →+* R) (a : R) :

f • a = f a := rfl

instance ring_hom.apply_has_faithful_smul [semiring R] : has_faithful_smul (R →+* R) R :=

⟨ring_hom.ext⟩

section add_comm_monoid

variables [semiring R] [add_comm_monoid M] [module R M]

variables (R)

lemma nsmul_eq_smul_cast (n : ℕ) (b : M) :

n • b = (n : R) • b :=

induction n with n ih,

{ rw [nat.cast_zero, zero_smul, zero_smul] },

{ rw [nat.succ_eq_add_one, nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul], }

lemma nat_smul_eq_nsmul (h : module ℕ M) (n : ℕ) (x : M) :

@has_smul.smul ℕ M h.to_has_smul n x = n • x :=

by rw [nsmul_eq_smul_cast ℕ n x, nat.cast_id]

def add_comm_monoid.nat_module.unique : unique (module ℕ M) :=

{ default := by apply_instance,

uniq := λ P, module.ext' P _ $ λ n, nat_smul_eq_nsmul P n }

instance add_comm_monoid.nat_is_scalar_tower :

is_scalar_tower ℕ R M :=

{ smul_assoc := λ n x y, nat.rec_on n

(by simp only [zero_smul])

(λ n ih, by simp only [nat.succ_eq_add_one, add_smul, one_smul, ih]) }

end add_comm_monoid

section add_comm_group

variables [semiring S] [ring R] [add_comm_group M] [module S M] [module R M]

variables (R)

lemma zsmul_eq_smul_cast (n : ℤ) (b : M) : n • b = (n : R) • b :=

have (smul_add_hom ℤ M).flip b = ((smul_add_hom R M).flip b).comp (int.cast_add_hom R),

by { ext, simp },

add_monoid_hom.congr_fun this n

lemma int_smul_eq_zsmul (h : module ℤ M) (n : ℤ) (x : M) :

@has_smul.smul ℤ M h.to_has_smul n x = n • x :=

by rw [zsmul_eq_smul_cast ℤ n x, int.cast_id]

def add_comm_group.int_module.unique : unique (module ℤ M) :=

{ default := by apply_instance,

uniq := λ P, module.ext' P _ $ λ n, int_smul_eq_zsmul P n }

end add_comm_group

lemma map_int_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}

[add_monoid_hom_class F M M₂] (f : F) (R S : Type*) [ring R] [ring S] [module R M] [module S M₂]

(x : ℤ) (a : M) : f ((x : R) • a) = (x : S) • f a :=

by simp only [←zsmul_eq_smul_cast, map_zsmul]

lemma map_nat_cast_smul [add_comm_monoid M] [add_comm_monoid M₂] {F : Type*}

[add_monoid_hom_class F M M₂] (f : F)

(R S : Type*) [semiring R] [semiring S] [module R M] [module S M₂] (x : ℕ) (a : M) :

f ((x : R) • a) = (x : S) • f a :=

by simp only [←nsmul_eq_smul_cast, map_nsmul]

lemma map_inv_nat_cast_smul [add_comm_monoid M] [add_comm_monoid M₂] {F : Type*}

[add_monoid_hom_class F M M₂] (f : F)

(R S : Type*) [division_semiring R] [division_semiring S] [module R M] [module S M₂]

(n : ℕ) (x : M) :

f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x :=

by_cases hR : (n : R) = 0; by_cases hS : (n : S) = 0,

{ simp [hR, hS] },

{ suffices : ∀ y, f y = 0, by simp [this], clear x, intro x,

rw [← inv_smul_smul₀ hS (f x), ← map_nat_cast_smul f R S], simp [hR] },

{ suffices : ∀ y, f y = 0, by simp [this], clear x, intro x,

rw [← smul_inv_smul₀ hR x, map_nat_cast_smul f R S, hS, zero_smul] },

{ rw [← inv_smul_smul₀ hS (f _), ← map_nat_cast_smul f R S, smul_inv_smul₀ hR] }

lemma map_inv_int_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}

[add_monoid_hom_class F M M₂] (f : F)

(R S : Type*) [division_ring R] [division_ring S] [module R M] [module S M₂]

(z : ℤ) (x : M) :

f ((z⁻¹ : R) • x) = (z⁻¹ : S) • f x :=

obtain ⟨n, rfl | rfl⟩ := z.eq_coe_or_neg,

{ rw [int.cast_coe_nat, int.cast_coe_nat, map_inv_nat_cast_smul _ R S] },

{ simp_rw [int.cast_neg, int.cast_coe_nat, inv_neg, neg_smul, map_neg,

map_inv_nat_cast_smul _ R S] },

lemma map_rat_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}

[add_monoid_hom_class F M M₂] (f : F)

(R S : Type*) [division_ring R] [division_ring S] [module R M] [module S M₂]

(c : ℚ) (x : M) :

f ((c : R) • x) = (c : S) • f x :=

by rw [rat.cast_def, rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,

map_int_cast_smul f R S, map_inv_nat_cast_smul f R S]

lemma map_rat_smul [add_comm_group M] [add_comm_group M₂] [module ℚ M] [module ℚ M₂] {F : Type*}

[add_monoid_hom_class F M M₂] (f : F) (c : ℚ) (x : M) :

f (c • x) = c • f x :=

rat.cast_id c ▸ map_rat_cast_smul f ℚ ℚ c x

instance subsingleton_rat_module (E : Type*) [add_comm_group E] : subsingleton (module ℚ E) :=

⟨λ P Q, module.ext' P Q $ λ r x,

@map_rat_smul _ _ _ _ P Q _ _ (add_monoid_hom.id E) r x⟩

lemma inv_nat_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_monoid E] [division_semiring R]

[division_semiring S] [module R E] [module S E] (n : ℕ) (x : E) :

(n⁻¹ : R) • x = (n⁻¹ : S) • x :=

map_inv_nat_cast_smul (add_monoid_hom.id E) R S n x

lemma inv_int_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]

[division_ring S] [module R E] [module S E] (n : ℤ) (x : E) :

(n⁻¹ : R) • x = (n⁻¹ : S) • x :=

map_inv_int_cast_smul (add_monoid_hom.id E) R S n x

lemma inv_nat_cast_smul_comm {α E : Type*} (R : Type*) [add_comm_monoid E] [division_semiring R]

[monoid α] [module R E] [distrib_mul_action α E] (n : ℕ) (s : α) (x : E) :

(n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=

(map_inv_nat_cast_smul (distrib_mul_action.to_add_monoid_hom E s) R R n x).symm

lemma inv_int_cast_smul_comm {α E : Type*} (R : Type*) [add_comm_group E] [division_ring R]

[monoid α] [module R E] [distrib_mul_action α E] (n : ℤ) (s : α) (x : E) :

(n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=

(map_inv_int_cast_smul (distrib_mul_action.to_add_monoid_hom E s) R R n x).symm

lemma rat_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]

[division_ring S] [module R E] [module S E] (r : ℚ) (x : E) :

(r : R) • x = (r : S) • x :=

map_rat_cast_smul (add_monoid_hom.id E) R S r x

instance add_comm_group.int_is_scalar_tower {R : Type u} {M : Type v} [ring R] [add_comm_group M]

[module R M]: is_scalar_tower ℤ R M :=

{ smul_assoc := λ n x y, ((smul_add_hom R M).flip y).map_zsmul x n }

instance is_scalar_tower.rat {R : Type u} {M : Type v} [ring R] [add_comm_group M]

[module R M] [module ℚ R] [module ℚ M] : is_scalar_tower ℚ R M :=

{ smul_assoc := λ r x y, map_rat_smul ((smul_add_hom R M).flip y) r x }

instance smul_comm_class.rat {R : Type u} {M : Type v} [semiring R] [add_comm_group M]

[module R M] [module ℚ M] : smul_comm_class ℚ R M :=

{ smul_comm := λ r x y, (map_rat_smul (smul_add_hom R M x) r y).symm }

instance smul_comm_class.rat' {R : Type u} {M : Type v} [semiring R] [add_comm_group M]

[module R M] [module ℚ M] : smul_comm_class R ℚ M :=

smul_comm_class.symm _ _ _

section no_zero_smul_divisors

class no_zero_smul_divisors (R M : Type*) [has_zero R] [has_zero M] [has_smul R M] : Prop :=

(eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0)

export no_zero_smul_divisors (eq_zero_or_eq_zero_of_smul_eq_zero)

lemma function.injective.no_zero_smul_divisors {R M N : Type*} [has_zero R] [has_zero M]

[has_zero N] [has_smul R M] [has_smul R N] [no_zero_smul_divisors R N] (f : M → N)

(hf : function.injective f) (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) :

no_zero_smul_divisors R M :=

⟨λ c m h,

or.imp_right (@hf _ _) $ h0.symm ▸ eq_zero_or_eq_zero_of_smul_eq_zero (by rw [←hs, h, h0])⟩

@[priority 100] -- See note [lower instance priority]

instance no_zero_divisors.to_no_zero_smul_divisors [has_zero R] [has_mul R] [no_zero_divisors R] :

no_zero_smul_divisors R R :=

⟨λ c x, eq_zero_or_eq_zero_of_mul_eq_zero⟩

lemma smul_ne_zero [has_zero R] [has_zero M] [has_smul R M] [no_zero_smul_divisors R M] {c : R}

{x : M} (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0 :=

λ h, (eq_zero_or_eq_zero_of_smul_eq_zero h).elim hc hx

section smul_with_zero

variables [has_zero R] [has_zero M] [smul_with_zero R M] [no_zero_smul_divisors R M] {c : R} {x : M}

@[simp] lemma smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=

⟨eq_zero_or_eq_zero_of_smul_eq_zero,

λ h, h.elim (λ h, h.symm ▸ zero_smul R x) (λ h, h.symm ▸ smul_zero c)⟩

lemma smul_ne_zero_iff : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 := by rw [ne.def, smul_eq_zero, not_or_distrib]

end smul_with_zero

section module

variables [semiring R] [add_comm_monoid M] [module R M]

section nat

variables (R) (M) [no_zero_smul_divisors R M] [char_zero R]

include R

lemma nat.no_zero_smul_divisors : no_zero_smul_divisors ℕ M :=

⟨by { intros c x, rw [nsmul_eq_smul_cast R, smul_eq_zero], simp }⟩

@[simp] lemma two_nsmul_eq_zero {v : M} : 2 • v = 0 ↔ v = 0 :=

by { haveI := nat.no_zero_smul_divisors R M, simp [smul_eq_zero] }

end nat

variables (R M)

lemma char_zero.of_module (M) [add_comm_monoid_with_one M] [char_zero M] [module R M] :

char_zero R :=

refine ⟨λ m n h, @nat.cast_injective M _ _ _ _ _⟩,

rw [← nsmul_one, ← nsmul_one, nsmul_eq_smul_cast R m (1 : M), nsmul_eq_smul_cast R n (1 : M), h]

end module

section add_comm_group -- `R` can still be a semiring here

variables [semiring R] [add_comm_group M] [module R M]

section smul_injective

variables (M)

lemma smul_right_injective [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) :

function.injective ((•) c : M → M) :=

(injective_iff_map_eq_zero (smul_add_hom R M c)).2 $ λ a ha, (smul_eq_zero.mp ha).resolve_left hc

variables {M}

lemma smul_right_inj [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) {x y : M} :

c • x = c • y ↔ x = y :=

(smul_right_injective M hc).eq_iff

end smul_injective

section nat

variables (R M) [no_zero_smul_divisors R M] [char_zero R]

include R

lemma self_eq_neg {v : M} : v = - v ↔ v = 0 :=

by rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]

lemma neg_eq_self {v : M} : - v = v ↔ v = 0 :=

by rw [eq_comm, self_eq_neg R M]

lemma self_ne_neg {v : M} : v ≠ -v ↔ v ≠ 0 :=

(self_eq_neg R M).not

lemma neg_ne_self {v : M} : -v ≠ v ↔ v ≠ 0 :=

(neg_eq_self R M).not

end nat

end add_comm_group

section module

variables [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M]

section smul_injective

variables (R)

lemma smul_left_injective {x : M} (hx : x ≠ 0) :

function.injective (λ (c : R), c • x) :=

λ c d h, sub_eq_zero.mp ((smul_eq_zero.mp

(calc (c - d) • x = c • x - d • x : sub_smul c d x

... = 0 : sub_eq_zero.mpr h)).resolve_right hx)

end smul_injective

end module

section group_with_zero

variables [group_with_zero R] [add_monoid M] [distrib_mul_action R M]

@[priority 100] -- see note [lower instance priority]

instance group_with_zero.to_no_zero_smul_divisors : no_zero_smul_divisors R M :=

⟨λ c x h, or_iff_not_imp_left.2 $ λ hc, (smul_eq_zero_iff_eq' hc).1 h⟩

end group_with_zero

@[priority 100] -- see note [lower instance priority]

instance rat_module.no_zero_smul_divisors [add_comm_group M] [module ℚ M] :

no_zero_smul_divisors ℤ M :=

⟨λ k x h, by simpa [zsmul_eq_smul_cast ℚ k x] using h⟩

end no_zero_smul_divisors

@[simp] lemma nat.smul_one_eq_coe {R : Type*} [semiring R] (m : ℕ) :

m • (1 : R) = ↑m :=

by rw [nsmul_eq_mul, mul_one]

@[simp] lemma int.smul_one_eq_coe {R : Type*} [ring R] (m : ℤ) :

m • (1 : R) = ↑m :=

by rw [zsmul_eq_mul, mul_one]

assert_not_exists multiset