import algebra.group.inj_surj

import algebra.group.commute

import algebra.hom.equiv.basic

import algebra.opposites

import data.int.cast.defs

universes u v

variables (α : Type u)

namespace mul_opposite

@[to_additive] instance [has_nat_cast α] : has_nat_cast αᵐᵒᵖ := ⟨λ n, op n⟩

@[to_additive] instance [has_int_cast α] : has_int_cast αᵐᵒᵖ := ⟨λ n, op n⟩

instance [add_semigroup α] : add_semigroup (αᵐᵒᵖ) :=

unop_injective.add_semigroup _ (λ x y, rfl)

instance [add_left_cancel_semigroup α] : add_left_cancel_semigroup αᵐᵒᵖ :=

unop_injective.add_left_cancel_semigroup _ (λ x y, rfl)

instance [add_right_cancel_semigroup α] : add_right_cancel_semigroup αᵐᵒᵖ :=

unop_injective.add_right_cancel_semigroup _ (λ x y, rfl)

instance [add_comm_semigroup α] : add_comm_semigroup αᵐᵒᵖ :=

unop_injective.add_comm_semigroup _ (λ x y, rfl)

instance [add_zero_class α] : add_zero_class αᵐᵒᵖ :=

unop_injective.add_zero_class _ rfl (λ x y, rfl)

instance [add_monoid α] : add_monoid αᵐᵒᵖ :=

unop_injective.add_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance [add_comm_monoid α] : add_comm_monoid αᵐᵒᵖ :=

unop_injective.add_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance [add_monoid_with_one α] : add_monoid_with_one αᵐᵒᵖ :=

{ nat_cast_zero := show op ((0 : ℕ) : α) = 0, by rw [nat.cast_zero, op_zero],

nat_cast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op (n : ℕ) + 1, by simp,

.. mul_opposite.add_monoid α, .. mul_opposite.has_one α, ..mul_opposite.has_nat_cast _ }

instance [add_comm_monoid_with_one α] : add_comm_monoid_with_one αᵐᵒᵖ :=

{ .. mul_opposite.add_monoid_with_one α, ..mul_opposite.add_comm_monoid α }

instance [sub_neg_monoid α] : sub_neg_monoid αᵐᵒᵖ :=

unop_injective.sub_neg_monoid _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance [add_group α] : add_group αᵐᵒᵖ :=

unop_injective.add_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance [add_comm_group α] : add_comm_group αᵐᵒᵖ :=

unop_injective.add_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance [add_group_with_one α] : add_group_with_one αᵐᵒᵖ :=

{ int_cast := λ n, op n,

int_cast_of_nat := λ n, show op ((n : ℤ) : α) = op n, by rw int.cast_coe_nat,

int_cast_neg_succ_of_nat := λ n, show op _ = op (- unop (op ((n + 1 : ℕ) : α))),

by erw [unop_op, int.cast_neg_succ_of_nat]; refl,

.. mul_opposite.add_monoid_with_one α, .. mul_opposite.add_group α }

instance [add_comm_group_with_one α] : add_comm_group_with_one αᵐᵒᵖ :=

{ .. mul_opposite.add_group_with_one α, ..mul_opposite.add_comm_group α }

@[to_additive] instance [semigroup α] : semigroup αᵐᵒᵖ :=

{ mul_assoc := λ x y z, unop_injective $ eq.symm $ mul_assoc (unop z) (unop y) (unop x),

.. mul_opposite.has_mul α }

@[to_additive] instance [right_cancel_semigroup α] : left_cancel_semigroup αᵐᵒᵖ :=

{ mul_left_cancel := λ x y z H, unop_injective $ mul_right_cancel $ op_injective H,

.. mul_opposite.semigroup α }

@[to_additive] instance [left_cancel_semigroup α] : right_cancel_semigroup αᵐᵒᵖ :=

{ mul_right_cancel := λ x y z H, unop_injective $ mul_left_cancel $ op_injective H,

.. mul_opposite.semigroup α }

@[to_additive] instance [comm_semigroup α] : comm_semigroup αᵐᵒᵖ :=

{ mul_comm := λ x y, unop_injective $ mul_comm (unop y) (unop x),

.. mul_opposite.semigroup α }

@[to_additive] instance [mul_one_class α] : mul_one_class αᵐᵒᵖ :=

{ one_mul := λ x, unop_injective $ mul_one $ unop x,

mul_one := λ x, unop_injective $ one_mul $ unop x,

.. mul_opposite.has_mul α, .. mul_opposite.has_one α }

@[to_additive] instance [monoid α] : monoid αᵐᵒᵖ :=

{ npow := λ n x, op $ x.unop ^ n,

npow_zero' := λ x, unop_injective $ monoid.npow_zero' x.unop,

npow_succ' := λ n x, unop_injective $ pow_succ' x.unop n,

.. mul_opposite.semigroup α, .. mul_opposite.mul_one_class α }

@[to_additive] instance [right_cancel_monoid α] : left_cancel_monoid αᵐᵒᵖ :=

{ .. mul_opposite.left_cancel_semigroup α, .. mul_opposite.monoid α }

@[to_additive] instance [left_cancel_monoid α] : right_cancel_monoid αᵐᵒᵖ :=

{ .. mul_opposite.right_cancel_semigroup α, .. mul_opposite.monoid α }

@[to_additive] instance [cancel_monoid α] : cancel_monoid αᵐᵒᵖ :=

{ .. mul_opposite.right_cancel_monoid α, .. mul_opposite.left_cancel_monoid α }

@[to_additive] instance [comm_monoid α] : comm_monoid αᵐᵒᵖ :=

{ .. mul_opposite.monoid α, .. mul_opposite.comm_semigroup α }

@[to_additive] instance [cancel_comm_monoid α] : cancel_comm_monoid αᵐᵒᵖ :=

{ .. mul_opposite.cancel_monoid α, .. mul_opposite.comm_monoid α }

@[to_additive add_opposite.sub_neg_monoid] instance [div_inv_monoid α] : div_inv_monoid αᵐᵒᵖ :=

{ zpow := λ n x, op $ x.unop ^ n,

zpow_zero' := λ x, unop_injective $ div_inv_monoid.zpow_zero' x.unop,

zpow_succ' := λ n x, unop_injective $

by rw [unop_op, zpow_of_nat, zpow_of_nat, pow_succ', unop_mul, unop_op],

zpow_neg' := λ z x, unop_injective $ div_inv_monoid.zpow_neg' z x.unop,

.. mul_opposite.monoid α, .. mul_opposite.has_inv α }

@[to_additive add_opposite.subtraction_monoid] instance [division_monoid α] :

division_monoid αᵐᵒᵖ :=

{ mul_inv_rev := λ a b, unop_injective $ mul_inv_rev _ _,

inv_eq_of_mul := λ a b h, unop_injective $ inv_eq_of_mul_eq_one_left $ congr_arg unop h,

.. mul_opposite.div_inv_monoid α, .. mul_opposite.has_involutive_inv α }

@[to_additive add_opposite.subtraction_comm_monoid] instance [division_comm_monoid α] :

division_comm_monoid αᵐᵒᵖ :=

{ ..mul_opposite.division_monoid α, ..mul_opposite.comm_semigroup α }

@[to_additive] instance [group α] : group αᵐᵒᵖ :=

{ mul_left_inv := λ x, unop_injective $ mul_inv_self $ unop x,

.. mul_opposite.div_inv_monoid α, }

@[to_additive] instance [comm_group α] : comm_group αᵐᵒᵖ :=

{ .. mul_opposite.group α, .. mul_opposite.comm_monoid α }

variable {α}

@[simp, norm_cast, to_additive] lemma op_nat_cast [has_nat_cast α] (n : ℕ) : op (n : α) = n := rfl

@[simp, norm_cast, to_additive] lemma op_int_cast [has_int_cast α] (n : ℤ) : op (n : α) = n := rfl

lemma unop_nat_cast [has_nat_cast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n := rfl

lemma unop_int_cast [has_int_cast α] (n : ℤ) : unop (n : αᵐᵒᵖ) = n := rfl

@[simp, to_additive] lemma unop_div [div_inv_monoid α] (x y : αᵐᵒᵖ) :

unop (x / y) = (unop y)⁻¹ * unop x :=

rfl

@[simp, to_additive] lemma op_div [div_inv_monoid α] (x y : α) :

op (x / y) = (op y)⁻¹ * op x :=

by simp [div_eq_mul_inv]

@[simp, to_additive] lemma semiconj_by_op [has_mul α] {a x y : α} :

semiconj_by (op a) (op y) (op x) ↔ semiconj_by a x y :=

by simp only [semiconj_by, ← op_mul, op_inj, eq_comm]

@[simp, to_additive] lemma semiconj_by_unop [has_mul α] {a x y : αᵐᵒᵖ} :

semiconj_by (unop a) (unop y) (unop x) ↔ semiconj_by a x y :=

by conv_rhs { rw [← op_unop a, ← op_unop x, ← op_unop y, semiconj_by_op] }

@[to_additive] lemma _root_.semiconj_by.op [has_mul α] {a x y : α} (h : semiconj_by a x y) :

semiconj_by (op a) (op y) (op x) :=

semiconj_by_op.2 h

@[to_additive] lemma _root_.semiconj_by.unop [has_mul α] {a x y : αᵐᵒᵖ} (h : semiconj_by a x y) :

semiconj_by (unop a) (unop y) (unop x) :=

semiconj_by_unop.2 h

@[to_additive] lemma _root_.commute.op [has_mul α] {x y : α} (h : commute x y) :

commute (op x) (op y) := h.op

@[to_additive] lemma commute.unop [has_mul α] {x y : αᵐᵒᵖ} (h : commute x y) :

commute (unop x) (unop y) := h.unop

@[simp, to_additive] lemma commute_op [has_mul α] {x y : α} :

commute (op x) (op y) ↔ commute x y :=

semiconj_by_op

@[simp, to_additive] lemma commute_unop [has_mul α] {x y : αᵐᵒᵖ} :

commute (unop x) (unop y) ↔ commute x y :=

semiconj_by_unop

def op_add_equiv [has_add α] : α ≃+ αᵐᵒᵖ :=

{ map_add' := λ a b, rfl, .. op_equiv }

@[simp] lemma op_add_equiv_to_equiv [has_add α] :

(op_add_equiv : α ≃+ αᵐᵒᵖ).to_equiv = op_equiv :=

rfl

end mul_opposite

namespace add_opposite

instance [semigroup α] : semigroup (αᵃᵒᵖ) :=

unop_injective.semigroup _ (λ x y, rfl)

instance [left_cancel_semigroup α] : left_cancel_semigroup αᵃᵒᵖ :=

unop_injective.left_cancel_semigroup _ (λ x y, rfl)

instance [right_cancel_semigroup α] : right_cancel_semigroup αᵃᵒᵖ :=

unop_injective.right_cancel_semigroup _ (λ x y, rfl)

instance [comm_semigroup α] : comm_semigroup αᵃᵒᵖ :=

unop_injective.comm_semigroup _ (λ x y, rfl)

instance [mul_one_class α] : mul_one_class αᵃᵒᵖ :=

unop_injective.mul_one_class _ rfl (λ x y, rfl)

instance {β} [has_pow α β] : has_pow αᵃᵒᵖ β := { pow := λ a b, op (unop a ^ b) }

@[simp] lemma op_pow {β} [has_pow α β] (a : α) (b : β) : op (a ^ b) = op a ^ b := rfl

@[simp] lemma unop_pow {β} [has_pow α β] (a : αᵃᵒᵖ) (b : β) : unop (a ^ b) = unop a ^ b := rfl

instance [monoid α] : monoid αᵃᵒᵖ :=

unop_injective.monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance [comm_monoid α] : comm_monoid αᵃᵒᵖ :=

unop_injective.comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

instance [div_inv_monoid α] : div_inv_monoid αᵃᵒᵖ :=

unop_injective.div_inv_monoid _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance [group α] : group αᵃᵒᵖ :=

unop_injective.group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance [comm_group α] : comm_group αᵃᵒᵖ :=

unop_injective.comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance [add_comm_monoid_with_one α] : add_comm_monoid_with_one αᵃᵒᵖ :=

{ nat_cast_zero := show op ((0 : ℕ) : α) = 0, by rw [nat.cast_zero, op_zero],

nat_cast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op (n : ℕ) + 1, by simp [add_comm],

..add_opposite.add_comm_monoid α, ..add_opposite.has_one, ..add_opposite.has_nat_cast _ }

instance [add_comm_group_with_one α] : add_comm_group_with_one αᵃᵒᵖ :=

{ int_cast_of_nat := λ n, congr_arg op $ int.cast_of_nat n,

int_cast_neg_succ_of_nat := λ _, congr_arg op $ int.cast_neg_succ_of_nat _,

..add_opposite.add_comm_monoid_with_one _, ..add_opposite.add_comm_group α,

..add_opposite.has_int_cast α }

variable {α}

def op_mul_equiv [has_mul α] : α ≃* αᵃᵒᵖ :=

{ map_mul' := λ a b, rfl, .. op_equiv }

@[simp] lemma op_mul_equiv_to_equiv [has_mul α] :

(op_mul_equiv : α ≃* αᵃᵒᵖ).to_equiv = op_equiv :=

rfl

end add_opposite

open mul_opposite

def mul_equiv.inv' (G : Type*) [division_monoid G] : G ≃* Gᵐᵒᵖ :=

{ map_mul' := λ x y, unop_injective $ mul_inv_rev x y,

.. (equiv.inv G).trans op_equiv }

def mul_hom.to_opposite {M N : Type*} [has_mul M] [has_mul N] (f : M →ₙ* N)

(hf : ∀ x y, commute (f x) (f y)) : M →ₙ* Nᵐᵒᵖ :=

{ to_fun := mul_opposite.op ∘ f,

map_mul' := λ x y, by simp [(hf x y).eq] }

def mul_hom.from_opposite {M N : Type*} [has_mul M] [has_mul N] (f : M →ₙ* N)

(hf : ∀ x y, commute (f x) (f y)) : Mᵐᵒᵖ →ₙ* N :=

{ to_fun := f ∘ mul_opposite.unop,

map_mul' := λ x y, (f.map_mul _ _).trans (hf _ _).eq }

def monoid_hom.to_opposite {M N : Type*} [mul_one_class M] [mul_one_class N] (f : M →* N)

(hf : ∀ x y, commute (f x) (f y)) : M →* Nᵐᵒᵖ :=

{ to_fun := mul_opposite.op ∘ f,

map_one' := congr_arg op f.map_one,

map_mul' := λ x y, by simp [(hf x y).eq] }

def monoid_hom.from_opposite {M N : Type*} [mul_one_class M] [mul_one_class N] (f : M →* N)

(hf : ∀ x y, commute (f x) (f y)) : Mᵐᵒᵖ →* N :=

{ to_fun := f ∘ mul_opposite.unop,

map_one' := f.map_one,

map_mul' := λ x y, (f.map_mul _ _).trans (hf _ _).eq }

def units.op_equiv {M} [monoid M] : (Mᵐᵒᵖ)ˣ ≃* (Mˣ)ᵐᵒᵖ :=

{ to_fun := λ u, op ⟨unop u, unop ↑(u⁻¹), op_injective u.4, op_injective u.3⟩,

inv_fun := mul_opposite.rec $ λ u, ⟨op ↑(u), op ↑(u⁻¹), unop_injective $ u.4, unop_injective u.3⟩,

map_mul' := λ x y, unop_injective $ units.ext $ rfl,

left_inv := λ x, units.ext $ by simp,

right_inv := λ x, unop_injective $ units.ext $ rfl }

lemma units.coe_unop_op_equiv {M} [monoid M] (u : (Mᵐᵒᵖ)ˣ) :

((units.op_equiv u).unop : M) = unop (u : Mᵐᵒᵖ) :=

rfl

lemma units.coe_op_equiv_symm {M} [monoid M] (u : (Mˣ)ᵐᵒᵖ) :

(units.op_equiv.symm u : Mᵐᵒᵖ) = op (u.unop : M) :=

rfl

lemma is_unit.op {M} [monoid M] {m : M} (h : is_unit m) : is_unit (op m) :=

let ⟨u, hu⟩ := h in hu ▸ ⟨units.op_equiv.symm (op u), rfl⟩

lemma is_unit.unop {M} [monoid M] {m : Mᵐᵒᵖ} (h : is_unit m) : is_unit (unop m) :=

let ⟨u, hu⟩ := h in hu ▸ ⟨unop (units.op_equiv u), rfl⟩

lemma is_unit_op {M} [monoid M] {m : M} : is_unit (op m) ↔ is_unit m := ⟨is_unit.unop, is_unit.op⟩

lemma is_unit_unop {M} [monoid M] {m : Mᵐᵒᵖ} : is_unit (unop m) ↔ is_unit m :=

⟨is_unit.op, is_unit.unop⟩

def mul_hom.op {M N} [has_mul M] [has_mul N] :

(M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) :=

{ to_fun := λ f, { to_fun := op ∘ f ∘ unop,

map_mul' := λ x y, unop_injective (f.map_mul y.unop x.unop) },

inv_fun := λ f, { to_fun := unop ∘ f ∘ op,

map_mul' := λ x y, congr_arg unop (f.map_mul (op y) (op x)) },

left_inv := λ f, by { ext, refl },

right_inv := λ f, by { ext x, simp } }

def mul_hom.unop {M N} [has_mul M] [has_mul N] :

(Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N) := mul_hom.op.symm

def add_hom.mul_op {M N} [has_add M] [has_add N] :

(add_hom M N) ≃ (add_hom Mᵐᵒᵖ Nᵐᵒᵖ) :=

{ to_fun := λ f, { to_fun := op ∘ f ∘ unop,

map_add' := λ x y, unop_injective (f.map_add x.unop y.unop) },

inv_fun := λ f, { to_fun := unop ∘ f ∘ op,

map_add' := λ x y, congr_arg unop (f.map_add (op x) (op y)) },

left_inv := λ f, by { ext, refl },

right_inv := λ f, by { ext, simp } }

@[simp] def add_hom.mul_unop {α β} [has_add α] [has_add β] :

(add_hom αᵐᵒᵖ βᵐᵒᵖ) ≃ (add_hom α β) := add_hom.mul_op.symm

def monoid_hom.op {M N} [mul_one_class M] [mul_one_class N] :

(M →* N) ≃ (Mᵐᵒᵖ →* Nᵐᵒᵖ) :=

{ to_fun := λ f, { to_fun := op ∘ f ∘ unop,

map_one' := congr_arg op f.map_one,

map_mul' := λ x y, unop_injective (f.map_mul y.unop x.unop) },

inv_fun := λ f, { to_fun := unop ∘ f ∘ op,

map_one' := congr_arg unop f.map_one,

map_mul' := λ x y, congr_arg unop (f.map_mul (op y) (op x)) },

left_inv := λ f, by { ext, refl },

right_inv := λ f, by { ext x, simp } }

def monoid_hom.unop {M N} [mul_one_class M] [mul_one_class N] :

(Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N) := monoid_hom.op.symm

def add_monoid_hom.mul_op {M N} [add_zero_class M] [add_zero_class N] :

(M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ) :=

{ to_fun := λ f, { to_fun := op ∘ f ∘ unop,

map_zero' := unop_injective f.map_zero,

map_add' := λ x y, unop_injective (f.map_add x.unop y.unop) },

inv_fun := λ f, { to_fun := unop ∘ f ∘ op,

map_zero' := congr_arg unop f.map_zero,

map_add' := λ x y, congr_arg unop (f.map_add (op x) (op y)) },

left_inv := λ f, by { ext, refl },

right_inv := λ f, by { ext, simp } }

@[simp] def add_monoid_hom.mul_unop {α β} [add_zero_class α] [add_zero_class β] :

(αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β) := add_monoid_hom.mul_op.symm

def add_equiv.mul_op {α β} [has_add α] [has_add β] :

(α ≃+ β) ≃ (αᵐᵒᵖ ≃+ βᵐᵒᵖ) :=

{ to_fun := λ f, op_add_equiv.symm.trans (f.trans op_add_equiv),

inv_fun := λ f, op_add_equiv.trans (f.trans op_add_equiv.symm),

left_inv := λ f, by { ext, refl },

right_inv := λ f, by { ext, simp } }

@[simp] def add_equiv.mul_unop {α β} [has_add α] [has_add β] :

(αᵐᵒᵖ ≃+ βᵐᵒᵖ) ≃ (α ≃+ β) := add_equiv.mul_op.symm

def mul_equiv.op {α β} [has_mul α] [has_mul β] :

(α ≃* β) ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ) :=

{ to_fun := λ f, { to_fun := op ∘ f ∘ unop,

inv_fun := op ∘ f.symm ∘ unop,

left_inv := λ x, unop_injective (f.symm_apply_apply x.unop),

right_inv := λ x, unop_injective (f.apply_symm_apply x.unop),

map_mul' := λ x y, unop_injective (f.map_mul y.unop x.unop) },

inv_fun := λ f, { to_fun := unop ∘ f ∘ op,

inv_fun := unop ∘ f.symm ∘ op,

left_inv := λ x, by simp,

right_inv := λ x, by simp,

map_mul' := λ x y, congr_arg unop (f.map_mul (op y) (op x)) },

left_inv := λ f, by { ext, refl },

right_inv := λ f, by { ext, simp } }

def mul_equiv.unop {α β} [has_mul α] [has_mul β] :

(αᵐᵒᵖ ≃* βᵐᵒᵖ) ≃ (α ≃* β) := mul_equiv.op.symm

section ext

lemma add_monoid_hom.mul_op_ext {α β} [add_zero_class α] [add_zero_class β]

(f g : αᵐᵒᵖ →+ β)

(h : f.comp (op_add_equiv : α ≃+ αᵐᵒᵖ).to_add_monoid_hom =

g.comp (op_add_equiv : α ≃+ αᵐᵒᵖ).to_add_monoid_hom) : f = g :=

add_monoid_hom.ext $ mul_opposite.rec $ λ x, (add_monoid_hom.congr_fun h : _) x

end ext