The coefficient-dual annihilator lemma

Only the annihilator calculation required by the stable Hom--Ext argument is retained here. For an injective coefficient module, the image of dual precomposition by t consists precisely of the functionals vanishing on ker t.

def MagnitudeConjecture.CoefficientDual.annihilator {k : Type uk} {M : Type uM} {E : Type uE} [CommRing k] [AddCommGroup M] [Module k M] [AddCommGroup E] [Module k E] (N : Submodule k M) : Submodule k (M →ₗ[k] E)

The submodule of coefficient-valued functionals vanishing on N.

@[simp]

theorem MagnitudeConjecture.CoefficientDual.mem_annihilator_iff {k : Type uk} {M : Type uM} {E : Type uE} [CommRing k] [AddCommGroup M] [Module k M] [AddCommGroup E] [Module k E] (N : Submodule k M) (phi : M →ₗ[k] E) : phi ∈ annihilator N ↔ ∀ n ∈ N, phi n = 0

theorem MagnitudeConjecture.CoefficientDual.range_lcomp_eq_annihilator_ker {k : Type uk} {M : Type uM} {E : Type uE} [CommRing k] [AddCommGroup M] [Module k M] [AddCommGroup E] [Module k E] {N : Type uN} [AddCommGroup N] [Module k N] [Small.{uE, uk} k] [Module.Injective k E] (t : M →ₗ[k] N) : (LinearMap.lcomp k E t).range = annihilator t.ker

Dual precomposition by t has image the annihilator of ker t.