lean-ga / for_mathlib.algebra.algebra.opposite

source

def alg_hom.from_opposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

Aᵐᵒᵖ →ₐ[R] B

An algebra homomorphism f : A →ₐ[R] B such that f x commutes with f y for all x, y defines an algebra homomorphism from Aᵐᵒᵖ.

Equations

f.from_opposite hf = {to_fun := ⇑f ∘ mul_opposite.unop, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem alg_hom.from_opposite_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

⇑(f.from_opposite hf) = ⇑f ∘ mul_opposite.unop

source

@[simp]

theorem alg_hom.to_linear_map_from_opposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

(f.from_opposite hf).to_linear_map = f.to_linear_map.comp (mul_opposite.op_linear_equiv R).symm.to_linear_map

source

@[simp]

theorem alg_hom.to_ring_hom_from_opposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

(f.from_opposite hf).to_ring_hom = f.to_ring_hom.from_opposite hf

source

@[simp]

theorem alg_hom.to_opposite_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

⇑(f.to_opposite hf) = mul_opposite.op ∘ ⇑f

source

def alg_hom.to_opposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

A →ₐ[R] Bᵐᵒᵖ

An algebra homomorphism f : A →ₐ[R] B such that f x commutes with f y for all x, y defines an algebra homomorphism to Bᵐᵒᵖ.

Equations

f.to_opposite hf = {to_fun := mul_opposite.op ∘ ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem alg_hom.to_linear_map_to_opposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

(f.to_opposite hf).to_linear_map = (mul_opposite.op_linear_equiv R).to_linear_map.comp f.to_linear_map

source

@[simp]

theorem alg_hom.to_ring_hom_to_opposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), commute (⇑f x) (⇑f y)) :

(f.to_opposite hf).to_ring_hom = f.to_ring_hom.to_opposite hf

source

@[protected]

def alg_hom.op {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

(A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ)

An algebra hom A →ₐ[R] B can equivalently be viewed as an algebra hom αᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

alg_hom.op = {to_fun := λ (f : A →ₐ[R] B), {to_fun := (⇑ring_hom.op f.to_ring_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, inv_fun := λ (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ), {to_fun := (⇑ring_hom.unop f.to_ring_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem alg_hom.op_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) (ᾰ : A) :

⇑(⇑(alg_hom.op.symm) f) ᾰ = (⇑ring_hom.unop f.to_ring_hom).to_fun ᾰ

source

@[simp]

theorem alg_hom.op_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (ᾰ : Aᵐᵒᵖ) :

⇑(⇑alg_hom.op f) ᾰ = (⇑ring_hom.op f.to_ring_hom).to_fun ᾰ

source

@[protected, simp]

def alg_hom.unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

(Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B)

The 'unopposite' of an algebra hom αᵐᵒᵖ →+* Bᵐᵒᵖ. Inverse to ring_hom.op.

Equations

alg_hom.unop = alg_hom.op.symm

source

@[simp]

theorem alg_equiv.alg_equiv.op_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A ≃ₐ[R] B) (ᾰ : Aᵐᵒᵖ) :

⇑(⇑alg_equiv.alg_equiv.op f) ᾰ = (⇑ring_equiv.op f.to_ring_equiv).to_fun ᾰ

source

@[simp]

theorem alg_equiv.alg_equiv.op_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) (ᾰ : A) :

⇑(⇑(alg_equiv.alg_equiv.op.symm) f) ᾰ = (⇑ring_equiv.unop f.to_ring_equiv).to_fun ᾰ

source

@[simp]

theorem alg_equiv.alg_equiv.op_symm_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) (ᾰ : B) :

⇑((⇑(alg_equiv.alg_equiv.op.symm) f).symm) ᾰ = (⇑ring_equiv.unop f.to_ring_equiv).inv_fun ᾰ

source

def alg_equiv.alg_equiv.op {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

(A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ

An algebra iso A ≃ₐ[R] B can equivalently be viewed as an algebra iso αᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

alg_equiv.alg_equiv.op = {to_fun := λ (f : A ≃ₐ[R] B), {to_fun := (⇑ring_equiv.op f.to_ring_equiv).to_fun, inv_fun := (⇑ring_equiv.op f.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}, inv_fun := λ (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ), {to_fun := (⇑ring_equiv.unop f.to_ring_equiv).to_fun, inv_fun := (⇑ring_equiv.unop f.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem alg_equiv.alg_equiv.op_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A ≃ₐ[R] B) (ᾰ : Bᵐᵒᵖ) :

⇑((⇑alg_equiv.alg_equiv.op f).symm) ᾰ = (⇑ring_equiv.op f.to_ring_equiv).inv_fun ᾰ

source

@[protected, simp]

def alg_equiv.unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

(Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ A ≃ₐ[R] B

The 'unopposite' of an algebra iso Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ. Inverse to alg_equiv.op.

Equations

alg_equiv.unop = alg_equiv.alg_equiv.op.symm

source

@[simp]

theorem mul_opposite.op_op_alg_equiv_symm_apply {R : Type u_1} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] (ᾰ : A) :

⇑(mul_opposite.op_op_alg_equiv.symm) ᾰ = mul_opposite.op (mul_opposite.op ᾰ)

source

def mul_opposite.op_op_alg_equiv {R : Type u_1} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] :

Aᵐᵒᵖ ᵐᵒᵖ ≃ₐ[R] A

The double opposite is isomorphic as an algebra to the original type.

Equations

mul_opposite.op_op_alg_equiv = alg_equiv.of_linear_equiv ((mul_opposite.op_linear_equiv R).trans (mul_opposite.op_linear_equiv R)).symm mul_opposite.op_op_alg_equiv._proof_7 mul_opposite.op_op_alg_equiv._proof_8

source

@[simp]

theorem mul_opposite.op_op_alg_equiv_apply {R : Type u_1} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] (ᾰ : Aᵐᵒᵖ ᵐᵒᵖ) :

⇑mul_opposite.op_op_alg_equiv ᾰ = mul_opposite.unop (mul_opposite.unop ᾰ)

source

@[simp]

theorem alg_hom.op_comm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (ᾰ : A →ₐ[R] Bᵐᵒᵖ) (ᾰ_1 : Aᵐᵒᵖ) :

⇑(⇑alg_hom.op_comm ᾰ) ᾰ_1 = mul_opposite.unop (⇑(⇑(mul_opposite.op_op_alg_equiv.symm.arrow_congr alg_equiv.refl) ᾰ) (mul_opposite.op ᾰ_1))

source

@[simp]

theorem alg_hom.op_comm_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (ᾰ : Aᵐᵒᵖ →ₐ[R] B) (ᾰ_1 : A) :

⇑(⇑(alg_hom.op_comm.symm) ᾰ) ᾰ_1 = mul_opposite.op (⇑ᾰ (mul_opposite.op ᾰ_1))

source

def alg_hom.op_comm {R : Type u_1} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :

(A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B)

Equations

alg_hom.op_comm = (mul_opposite.op_op_alg_equiv.symm.arrow_congr alg_equiv.refl).trans alg_hom.op.symm

mathlib3 documentation

Algebra structures on the multiplicative opposite #