Finite algebras of operators detected by a pairing

Suppose a module embeds into functionals on a Noetherian module, and a family of operators is adjoint to operators on that Noetherian module. Then the algebra generated by the first family is finite over the base ring. In particular, a finite module over a Noetherian ring suffices. This transfers an integral structure on cycles to an algebra of operators on functions, without choosing a lattice in the function space.

The symbol-side evaluation takes values in the opposite endomorphism ring. Precomposition reverses products, so this convention extends generator equivariance to the free algebra without any commutativity assumption on the operators.

The pairing need only be bilinear over the base ring, even when the first family is linear over a scalar algebra.

theorem LinearMap.pairing_freeAlgebra_lift {R : Type u_1} {K : Type u_2} {M : Type u_3} {V : Type u_4} {ι : Type u_5} [CommSemiring R] [Semiring K] [Algebra R K] [AddCommMonoid M] [Module R M] [AddCommMonoid V] [Module K V] [Module R V] [IsScalarTower R K V] (P : V →ₗ[R] M →ₗ[R] K) (t : ι → Module.End K V) (u : ι → Module.End R M) (h : ∀ (i : ι) (v : V) (x : M), (P ((t i) v)) x = (P v) ((u i) x)) (a : FreeAlgebra R ι) (v : V) (x : M) : (P ((((FreeAlgebra.lift R) t) a) v)) x = (P v) ((MulOpposite.unop (((FreeAlgebra.lift R) fun (i : ι) => MulOpposite.op (u i)) a)) x)

An adjointness identity on generators extends to the free algebra, with the adjoint operators evaluated in the opposite endomorphism ring.

theorem LinearMap.finite_adjoin_of_injective_pairing {R : Type u_1} {K : Type u_2} {M : Type u_3} {V : Type u_4} {ι : Type u_5} [CommRing R] [Semiring K] [Algebra R K] [AddCommGroup M] [Module R M] [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] [IsNoetherian R M] (P : V →ₗ[R] M →ₗ[R] K) (hP : Function.Injective ⇑P) (t : ι → Module.End K V) (u : ι → Module.End R M) (h : ∀ (i : ι) (v : V) (x : M), (P ((t i) v)) x = (P v) ((u i) x)) : Module.Finite R ↥(Algebra.adjoin R (Set.range t))

If an injective pairing detects a family of operators by adjoint operators on a Noetherian module, its generated algebra is finite over the base ring. The operators need not commute, and the module carrying the first family need not be finite.