Evaluation into the opposite double dual

For a left module P over a possibly noncommutative ring A, its dual Hom_A(P, A) is a right A-module. Dualizing on that side, with values in the right regular module A, returns a left module. Evaluation identifies a finitely generated projective module with this double dual.

opDualCodomainEquiv transports right-linear functionals from the regular codomain A to Aᵐᵒᵖ, semilinearly along A ≃+* Aᵐᵒᵖᵐᵒᵖ. It commutes with precomposition and carries its range onto the range computed using the opposite codomain. This compares evaluation with constructions that use the opposite ring itself as the second dual's codomain.

unopDualEvalEquiv gives the right-module version with both duals taking values in A, so that its scalars stay in Aᵐᵒᵖ rather than passing to a triple opposite.

This is the reflexivity used when dualizing a projective presentation twice in the Auslander--Bridger transpose construction. Unlike Module.evalEquiv, the evaluation here changes sides and does not require commutativity of the coefficient ring.

def TauCeti.opDualCodomainEquiv (A : Type u_1) (N : Type u_2) [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] : (N →ₗ[Aᵐᵒᵖ] A) ≃ₛₗ[↑(RingEquiv.opOp A)] Module.Dual Aᵐᵒᵖ N

Changing the codomain of a right-linear functional from A to Aᵐᵒᵖ identifies the two dual conventions. Scalars change from A to its double opposite.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.opDualCodomainEquiv_apply (A : Type u_1) (N : Type u_2) [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] (F : N →ₗ[Aᵐᵒᵖ] A) (x : N) : ((opDualCodomainEquiv A N) F) x = MulOpposite.op (F x)

Codomain transport applies op to the value of a functional.

@[simp]

theorem TauCeti.opDualCodomainEquiv_symm_apply (A : Type u_1) (N : Type u_2) [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] (F : Module.Dual Aᵐᵒᵖ N) (x : N) : ((opDualCodomainEquiv A N).symm F) x = MulOpposite.unop (F x)

Inverse codomain transport applies unop to the value of a functional.

@[simp]

theorem TauCeti.opDualCodomainEquiv_lcomp (A : Type u_1) {N : Type u_2} [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] {N' : Type u_3} [AddCommMonoid N'] [Module Aᵐᵒᵖ N'] (f : N →ₗ[Aᵐᵒᵖ] N') (F : N' →ₗ[Aᵐᵒᵖ] A) : (opDualCodomainEquiv A N) ((LinearMap.lcomp A A f) F) = (LinearMap.lcomp Aᵐᵒᵖᵐᵒᵖ Aᵐᵒᵖ f) ((opDualCodomainEquiv A N') F)

Codomain transport commutes with precomposition.

theorem TauCeti.map_range_opDualCodomainEquiv (A : Type u_1) {N : Type u_2} [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] {N' : Type u_3} [AddCommMonoid N'] [Module Aᵐᵒᵖ N'] (f : N →ₗ[Aᵐᵒᵖ] N') : Submodule.map (↑(opDualCodomainEquiv A N)) (LinearMap.lcomp A A f).range = (LinearMap.lcomp Aᵐᵒᵖᵐᵒᵖ Aᵐᵒᵖ f).range

Codomain transport carries the image of precomposition onto the image of precomposition with the opposite regular codomain.

def TauCeti.opDualEval (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] : P →ₗ[A] Module.Dual A P →ₗ[Aᵐᵒᵖ] A

Evaluation into the double dual, changing from left to right modules between the two dualizations. The second dual takes values in the right regular module A.

Equations

• TauCeti.opDualEval A P = LinearMap.id.flip

@[simp]

theorem TauCeti.opDualEval_apply (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] (x : P) (φ : Module.Dual A P) : ((opDualEval A P) x) φ = φ x

Evaluation is application of a functional to a vector.

theorem TauCeti.opDualEval_naturality (A : Type u_1) {P : Type u_2} [Semiring A] [AddCommMonoid P] [Module A P] {Q : Type u_3} [AddCommMonoid Q] [Module A Q] (f : P →ₗ[A] Q) (x : P) : (opDualEval A Q) (f x) = (LinearMap.lcomp A A (LinearMap.lcomp Aᵐᵒᵖ A f)) ((opDualEval A P) x)

Evaluation commutes with applying a linear map and dualizing it twice.

theorem TauCeti.opDualEval_bijective (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] [Module.Finite A P] [Module.Projective A P] : Function.Bijective ⇑(opDualEval A P)

A finitely generated projective module is its opposite double dual. Evaluation is bijective, with no commutativity hypothesis on the semiring.

noncomputable def TauCeti.opDualEvalEquiv (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] [Module.Finite A P] [Module.Projective A P] : P ≃ₗ[A] Module.Dual A P →ₗ[Aᵐᵒᵖ] A

The canonical equivalence of a finitely generated projective left module with the dual of its right dual.

Equations

• TauCeti.opDualEvalEquiv A P = LinearEquiv.ofBijective (TauCeti.opDualEval A P) ⋯

@[simp]

theorem TauCeti.opDualEvalEquiv_toLinearMap (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] [Module.Finite A P] [Module.Projective A P] : ↑(opDualEvalEquiv A P) = opDualEval A P

The underlying map of the double-dual equivalence is evaluation.

@[simp]

theorem TauCeti.opDualEvalEquiv_apply (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] [Module.Finite A P] [Module.Projective A P] (x : P) (φ : Module.Dual A P) : ((opDualEvalEquiv A P) x) φ = φ x

The double-dual equivalence is evaluation.

@[simp]

theorem TauCeti.apply_opDualEvalEquiv_symm (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] [Module.Finite A P] [Module.Projective A P] (F : Module.Dual A P →ₗ[Aᵐᵒᵖ] A) (φ : Module.Dual A P) : φ ((opDualEvalEquiv A P).symm F) = F φ

The inverse double-dual equivalence recovers the vector represented by a functional.

theorem TauCeti.opDual_lcomp_bijective (A : Type u_1) (P : Type u_2) [Semiring A] [AddCommMonoid P] [Module A P] {Q : Type u_3} [AddCommMonoid Q] [Module A Q] [Module.Finite A P] [Module.Projective A P] : Function.Bijective fun (f : Q →ₗ[A] P) => LinearMap.lcomp Aᵐᵒᵖ A f

Taking opposite duals identifies maps into a finite projective module with maps out of its opposite dual. The source module need not be finite or projective.

theorem TauCeti.map_range_opDualEval (A : Type u_1) {P : Type u_2} [Semiring A] [AddCommMonoid P] [Module A P] {Q : Type u_3} [AddCommMonoid Q] [Module A Q] [Module.Finite A P] [Module.Projective A P] (f : P →ₗ[A] Q) : Submodule.map (opDualEval A Q) f.range = (LinearMap.lcomp A A (LinearMap.lcomp Aᵐᵒᵖ A f)).range

Evaluation carries the image of a map onto the image of its opposite double dual when the source is finitely generated and projective. No hypothesis on the target is needed.

noncomputable def TauCeti.unopDualEvalEquiv (A : Type u_4) (N : Type u_5) [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module.Finite Aᵐᵒᵖ N] [Module.Projective Aᵐᵒᵖ N] : N ≃ₗ[Aᵐᵒᵖ] Module.Dual A (N →ₗ[Aᵐᵒᵖ] A)

Evaluation identifies a finite projective right module with the left dual of its right-linear dual taking values in A. Both sides have their original right A-action.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.unopDualEvalEquiv_apply (A : Type u_4) (N : Type u_5) [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module.Finite Aᵐᵒᵖ N] [Module.Projective Aᵐᵒᵖ N] (x : N) (φ : N →ₗ[Aᵐᵒᵖ] A) : ((unopDualEvalEquiv A N) x) φ = φ x

Right-module bidual evaluation applies a functional to the vector.

@[simp]

theorem TauCeti.apply_unopDualEvalEquiv_symm (A : Type u_4) (N : Type u_5) [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module.Finite Aᵐᵒᵖ N] [Module.Projective Aᵐᵒᵖ N] (F : Module.Dual A (N →ₗ[Aᵐᵒᵖ] A)) (φ : N →ₗ[Aᵐᵒᵖ] A) : φ ((unopDualEvalEquiv A N).symm F) = F φ

A functional applied to inverse right-module bidual evaluation recovers its value.

theorem TauCeti.unopDualEvalEquiv_naturality (A : Type u_4) {N : Type u_5} [Semiring A] [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module.Finite Aᵐᵒᵖ N] [Module.Projective Aᵐᵒᵖ N] {N' : Type u_6} [AddCommMonoid N'] [Module Aᵐᵒᵖ N'] [Module.Finite Aᵐᵒᵖ N'] [Module.Projective Aᵐᵒᵖ N'] (f : N →ₗ[Aᵐᵒᵖ] N') (x : N) : (unopDualEvalEquiv A N') (f x) = (LinearMap.lcomp Aᵐᵒᵖ A (LinearMap.lcomp A A f)) ((unopDualEvalEquiv A N) x)

Right-module bidual evaluation commutes with a linear map and its double dual.