Representation-finiteness of the opposite algebra

The k-dual D = Hom_k(-, k) sends finite-dimensional left B-modules to right B-modules, reverses endomorphism rings and is involutive up to the evaluation isomorphism. Hence a finite-dimensional algebra is representation-finite if and only if its opposite is (isRepresentationFinite_op). This is used for the dual halves of the local arguments of Part III ("the dual assertion holds", "passing to the opposite algebra").

def MultiplicativeBasisDeformations.KDual.lact {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) (b : B) : ↑M →ₗ[k] ↑M

The action of an element as a k-linear map.

theorem MultiplicativeBasisDeformations.KDual.lact_apply {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) (b : B) (m : ↑M) : (lact M b) m = b • m

def MultiplicativeBasisDeformations.KDual.ρD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : Bᵐᵒᵖ →+* Module.End k (Module.Dual k ↑M)

The right action on the dual.

def MultiplicativeBasisDeformations.KDual.DT (k : Type u) [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : Type u

The dual space, with the right action of B.

@[instance_reducible]

instance MultiplicativeBasisDeformations.KDual.instAddCommGroupDT {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : AddCommGroup (DT k M)

@[instance_reducible]

instance MultiplicativeBasisDeformations.KDual.instModuleMulOppositeDT {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : Module Bᵐᵒᵖ (DT k M)

def MultiplicativeBasisDeformations.KDual.D {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : ModuleCat Bᵐᵒᵖ

The dual module.

def MultiplicativeBasisDeformations.KDual.ofD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M : ModuleCat B} (φ : ↑(D M)) : Module.Dual k ↑M

An element of the dual module as a functional.

def MultiplicativeBasisDeformations.KDual.toD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M : ModuleCat B} (φ : Module.Dual k ↑M) : ↑(D M)

A functional as an element of the dual module.

@[simp]

theorem MultiplicativeBasisDeformations.KDual.ofD_toD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M : ModuleCat B} (φ : Module.Dual k ↑M) : ofD (toD φ) = φ

@[simp]

theorem MultiplicativeBasisDeformations.KDual.toD_ofD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M : ModuleCat B} (φ : ↑(D M)) : toD (ofD φ) = φ

theorem MultiplicativeBasisDeformations.KDual.D_smul {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) (b : Bᵐᵒᵖ) (φ : ↑(D M)) (m : ↑M) : (ofD (b • φ)) m = (ofD φ) (MulOpposite.unop b • m)

theorem MultiplicativeBasisDeformations.KDual.ofD_add {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M : ModuleCat B} (φ ψ : ↑(D M)) : ofD (φ + ψ) = ofD φ + ofD ψ

theorem MultiplicativeBasisDeformations.KDual.ofD_zero {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M : ModuleCat B} : ofD 0 = 0

theorem MultiplicativeBasisDeformations.KDual.ofD_smul_k {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M : ModuleCat B} (c : k) (φ : ↑(D M)) : ofD (c • φ) = c • ofD φ

The scalar action of k on the dual module is the usual one.

def MultiplicativeBasisDeformations.KDual.ofDL {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : ↑(D M) ≃ₗ[k] Module.Dual k ↑M

The dual module is the dual space, k-linearly.

instance MultiplicativeBasisDeformations.KDual.instFiniteCarrierMulOppositeD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) [Module.Finite k ↑M] : Module.Finite k ↑(D M)

def MultiplicativeBasisDeformations.KDual.fk {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} (f : M ⟶ N) : ↑M →ₗ[k] ↑N

A module map as a k-linear map.

theorem MultiplicativeBasisDeformations.KDual.fk_apply {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} (f : M ⟶ N) (m : ↑M) : (fk f) m = (CategoryTheory.ConcreteCategory.hom f) m

def MultiplicativeBasisDeformations.KDual.dualHom {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} (f : M ⟶ N) : DT k N →ₗ[Bᵐᵒᵖ] DT k M

The transpose of a module map.

def MultiplicativeBasisDeformations.KDual.Dmap {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} (f : M ⟶ N) : D N ⟶ D M

The dual of a module map.

theorem MultiplicativeBasisDeformations.KDual.Dmap_apply {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} (f : M ⟶ N) (φ : ↑(D N)) (m : ↑M) : (ofD ((CategoryTheory.ConcreteCategory.hom (Dmap f)) φ)) m = (ofD φ) ((CategoryTheory.ConcreteCategory.hom f) m)

theorem MultiplicativeBasisDeformations.KDual.Dmap_comp {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N P : ModuleCat B} (f : M ⟶ N) (g : N ⟶ P) : Dmap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Dmap g) (Dmap f)

theorem MultiplicativeBasisDeformations.KDual.Dmap_id {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : Dmap (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (D M)

theorem MultiplicativeBasisDeformations.KDual.Dmap_add {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} (f g : M ⟶ N) : Dmap (f + g) = Dmap f + Dmap g

theorem MultiplicativeBasisDeformations.KDual.Dmap_zero {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} : Dmap 0 = 0

def MultiplicativeBasisDeformations.KDual.endD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : (CategoryTheory.End M)ᵐᵒᵖ →+* CategoryTheory.End (D M)

Transposition reverses endomorphism rings.

theorem MultiplicativeBasisDeformations.KDual.endD_injective {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : Function.Injective ⇑(endD M)

def MultiplicativeBasisDeformations.KDual.psiE {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) (h : CategoryTheory.End (D M)) (m : ↑M) : Module.Dual k (Module.Dual k ↑M)

The functional on the dual given by an endomorphism of the dual module.

noncomputable def MultiplicativeBasisDeformations.KDual.preE {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) [Module.Finite k ↑M] (h : CategoryTheory.End (D M)) (m : ↑M) : ↑M

The preimage of an endomorphism of the dual module.

theorem MultiplicativeBasisDeformations.KDual.dual_preE {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) [Module.Finite k ↑M] (h : CategoryTheory.End (D M)) (m : ↑M) (φ : Module.Dual k ↑M) : φ (preE M h m) = (ofD ((ModuleCat.Hom.hom h) (toD φ))) m

theorem MultiplicativeBasisDeformations.KDual.eq_of_dual {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) [Module.Finite k ↑M] {x y : ↑M} (h : ∀ (φ : Module.Dual k ↑M), φ x = φ y) : x = y

noncomputable def MultiplicativeBasisDeformations.KDual.preHom {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) [Module.Finite k ↑M] (h : CategoryTheory.End (D M)) : ↑M →ₗ[B] ↑M

The preimage as a module map.

theorem MultiplicativeBasisDeformations.KDual.endD_surjective {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) [Module.Finite k ↑M] : Function.Surjective ⇑(endD M)

noncomputable def MultiplicativeBasisDeformations.KDual.endDEquiv {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) [Module.Finite k ↑M] : (CategoryTheory.End M)ᵐᵒᵖ ≃+* CategoryTheory.End (D M)

Transposition is an anti-isomorphism of endomorphism rings.

theorem MultiplicativeBasisDeformations.KDual.isLocalRing_mop {R : Type u_1} [Ring R] [IsLocalRing R] : IsLocalRing Rᵐᵒᵖ

The opposite of a local ring is local.

def MultiplicativeBasisDeformations.KDual.evD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) (m : ↑M) : DT k (D M)

Evaluation into the double dual.

theorem MultiplicativeBasisDeformations.KDual.ofD_evD {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (M : ModuleCat B) [Module.Finite k ↑M] (m : ↑M) (φ : ↑(D M)) : (ofD (evD M m)) φ = (ofD φ) m

def MultiplicativeBasisDeformations.KDual.toM {B : Type u} [Ring B] (M : ModuleCat B) (m : ↑(toOpOp.functor.obj M)) : ↑M

Elements of the restricted module.

theorem MultiplicativeBasisDeformations.KDual.toM_add {B : Type u} [Ring B] (M : ModuleCat B) (m m' : ↑(toOpOp.functor.obj M)) : toM M (m + m') = toM M m + toM M m'

def MultiplicativeBasisDeformations.KDual.ddMap {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (M : ModuleCat B) : ↑(toOpOp.functor.obj M) →ₗ[Bᵐᵒᵖᵐᵒᵖ] DT k (D M)

The double dual, as a map of right Bᵒᵖ-modules.

theorem MultiplicativeBasisDeformations.KDual.ddMap_bijective {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (M : ModuleCat B) [Module.Finite k ↑M] : Function.Bijective ⇑(ddMap M)

noncomputable def MultiplicativeBasisDeformations.KDual.ddIso {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (M : ModuleCat B) [Module.Finite k ↑M] : toOpOp.functor.obj M ≅ D (D M)

The double dual isomorphism.

def MultiplicativeBasisDeformations.KDual.Diso {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] {M N : ModuleCat B} (e : M ≅ N) : D N ≅ D M

The dual of an isomorphism.

theorem MultiplicativeBasisDeformations.isRepresentationFinite_op {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (hB : IsRepresentationFinite k B) : IsRepresentationFinite k Bᵐᵒᵖ

The opposite of a representation-finite algebra is representation-finite.