Evaluation from the balanced tensor product of an opposite dual

For a left module P over a possibly noncommutative k-algebra A, evaluation gives Hom_A(P,A) ⊗_A N → Hom_A(P,N), sending φ ⊗ n to x ↦ φ(x) • n. This map is an isomorphism when P is finitely generated projective. It is natural contravariantly in P and covariantly in N. If P is merely finitely generated, every map from P factoring through a projective module belongs to its image, even when that intermediate projective is not finitely generated.

The right action on Hom_A(P,A) is Mathlib's opposite-scalar action on the codomain. The tensor product is the existing balanced quotient over k; neither A nor its modules need to be finite-dimensional. These identifications allow a projective presentation's Hom complex to be computed by tensoring its opposite-dual complex, as in the tensor description of the transpose and Auslander–Reiten duality.

Mathlib's dualTensorHom treats commutative scalars. Here the balancing relations replace commutativity.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.2.

def TauCeti.balancedDualTensorHom (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] : BalancedTensorProduct k A (Module.Dual A P) N →ₗ[k] P →ₗ[A] N

Evaluation on the opposite dual tensored over a possibly noncommutative algebra: φ ⊗ n gives the linear map x ↦ φ(x) • n.

@[simp]

theorem TauCeti.balancedDualTensorHom_tmul (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] (φ : Module.Dual A P) (n : N) (x : P) : ((balancedDualTensorHom k A P N) (BalancedTensorProduct.tmul k A φ n)) x = φ x • n

theorem TauCeti.balancedDualTensorHom_bijective (k : Type u_1) (A : Type u_2) {P : Type u_3} {N : Type u_4} [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] : Function.Bijective ⇑(balancedDualTensorHom k A P N)

Evaluation is an isomorphism for finitely generated projective source modules, over a possibly noncommutative algebra.

theorem TauCeti.balancedDualTensorHom_map (k : Type u_1) (A : Type u_2) {P : Type u_3} {N : Type u_4} [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] {P' : Type u_5} {N' : Type u_6} [AddCommMonoid P'] [Module A P'] [AddCommGroup N'] [Module A N'] [Module k N'] [IsScalarTower k A N'] (f : P' →ₗ[A] P) (g : N →ₗ[A] N') : balancedDualTensorHom k A P' N' ∘ₗ BalancedTensorProduct.map (LinearMap.lcomp k A f) (↑k g) ⋯ ⋯ = LinearMap.compRight k g ∘ₗ LinearMap.lcomp k N f ∘ₗ balancedDualTensorHom k A P N

Evaluation is contravariantly natural in the dualized module and covariantly natural in the target. In particular, a map of projective presentations gives a commuting square between the corresponding tensor and Hom maps.

noncomputable def TauCeti.balancedDualTensorHomEquiv (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] : BalancedTensorProduct k A (Module.Dual A P) N ≃ₗ[k] P →ₗ[A] N

The canonical tensor–Hom equivalence for a finite projective left module. The tensor product uses the opposite dual and is balanced over A.

@[simp]

theorem TauCeti.balancedDualTensorHomEquiv_toLinearMap (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] : ↑(balancedDualTensorHomEquiv k A P N) = balancedDualTensorHom k A P N

@[simp]

theorem TauCeti.balancedDualTensorHomEquiv_apply (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] (z : BalancedTensorProduct k A (Module.Dual A P) N) : (balancedDualTensorHomEquiv k A P N) z = (balancedDualTensorHom k A P N) z

@[simp]

theorem TauCeti.balancedDualTensorHomEquiv_symm_balancedDualTensorHom (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] (z : BalancedTensorProduct k A (Module.Dual A P) N) : (balancedDualTensorHomEquiv k A P N).symm ((balancedDualTensorHom k A P N) z) = z

@[simp]

theorem TauCeti.balancedDualTensorHom_balancedDualTensorHomEquiv_symm (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] (F : P →ₗ[A] N) : (balancedDualTensorHom k A P N) ((balancedDualTensorHomEquiv k A P N).symm F) = F

theorem LinearMap.comp_mem_range_balancedDualTensorHom {k : Type u_1} {A : Type u_2} {M : Type u_3} {P : Type u_4} {N : Type u_5} [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid M] [Module A M] [Module.Finite A M] [AddCommGroup P] [Module A P] [Module.Projective A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] (f : M →ₗ[A] P) (g : P →ₗ[A] N) : g ∘ₗ f ∈ (TauCeti.balancedDualTensorHom k A M N).range

A map from a finitely generated module that factors through a projective module lies in the image of balanced tensor evaluation. The projective intermediate module need not be finitely generated.