Linear maps with range in a finitely generated submodule

A linear map f : M →ₗ[R] N is of finite rank (LinearMap.IsFiniteRank) if its range is contained in a finitely generated submodule of N. This is the notion of finite image used for operators on Banach modules over a coefficient ring: the completely continuous operators (ContinuousLinearMap.IsCompletelyContinuous) are those that, for every ε > 0, are uniformly within ε * ‖x‖ of a continuous map of finite rank; over Tate scalars this is approximation in the operator norm.

Mathlib's LinearMap.HasFiniteRange asks the range itself to be finitely generated. Over a general ring a submodule of a finitely generated module need not be finitely generated, so that predicate is not stable under addition or under precomposition. Asking only for a finitely generated submodule containing the range repairs this: maps of finite rank are closed under addition, negation, scalar multiplication and composition on either side by arbitrary linear maps, over any ring. Over a Noetherian ring the two notions coincide (LinearMap.isFiniteRank_iff_hasFiniteRange).

Over a division ring, a finite-rank perturbation of the identity, or more generally of a linear equivalence, is injective if and only if it is surjective: it restricts to an endomorphism of the finite-dimensional range of the perturbation. This algebraic Fredholm alternative gives the equivalence of injectivity, surjectivity and invertibility for 1 - u with u completely continuous (ContinuousLinearMap.IsCompletelyContinuous.injective_one_sub_iff_surjective).

Main definitions

• LinearMap.IsFiniteRank: the range of f is contained in a finitely generated submodule.

Main results

• LinearMap.HasFiniteRange.isFiniteRank: a map with finitely generated range has finite rank.
• LinearMap.isFiniteRank_iff_hasFiniteRange: over a Noetherian ring, finite rank is equivalent to finitely generated range.
• LinearMap.IsFiniteRank.add, LinearMap.IsFiniteRank.smul, LinearMap.IsFiniteRank.comp_left, LinearMap.IsFiniteRank.comp_right: the closure properties, with no Noetherian hypothesis.
• LinearMap.HasFiniteRange.injective_one_add_iff_surjective: over a division ring, 1 + F is injective if and only if it is surjective when F has finitely generated range.
• LinearMap.HasFiniteRange.injective_equiv_add_iff_surjective: the same for e + w with e a linear equivalence and w of finitely generated range.

References

• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.

def LinearMap.IsFiniteRank {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : Prop

A linear map is of finite rank if its range is contained in a finitely generated submodule of its codomain. Over a Noetherian ring this is LinearMap.HasFiniteRange (LinearMap.isFiniteRank_iff_hasFiniteRange); in general it is weaker.

theorem LinearMap.isFiniteRank_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} : f.IsFiniteRank ↔ ∃ (Q : Submodule R N), Q.FG ∧ f.range ≤ Q

theorem LinearMap.isFiniteRank_iff_forall_mem {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} : f.IsFiniteRank ↔ ∃ (Q : Submodule R N), Q.FG ∧ ∀ (x : M), f x ∈ Q

A linear map has finite rank if and only if all its values lie in a common finitely generated submodule.

theorem LinearMap.HasFiniteRange.isFiniteRank {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} (hf : f.HasFiniteRange) : f.IsFiniteRank

@[simp]

theorem LinearMap.IsFiniteRank.zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : IsFiniteRank 0

@[simp]

theorem LinearMap.IsFiniteRank.of_finite_rng {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R N] {f : M →ₗ[R] N} : f.IsFiniteRank

Every linear map into a finitely generated module has finite rank.

theorem LinearMap.IsFiniteRank.add {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : M →ₗ[R] N} (hf : f.IsFiniteRank) (hg : g.IsFiniteRank) : (f + g).IsFiniteRank

theorem LinearMap.IsFiniteRank.comp_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {f : M →ₗ[R] N} (hf : f.IsFiniteRank) (g : N →ₗ[R] P) : (g ∘ₗ f).IsFiniteRank

Postcomposing a map of finite rank with any linear map gives a map of finite rank.

theorem LinearMap.IsFiniteRank.comp_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {g : N →ₗ[R] P} (hg : g.IsFiniteRank) (f : M →ₗ[R] N) : (g ∘ₗ f).IsFiniteRank

Precomposing a map of finite rank with any linear map gives a map of finite rank. Unlike LinearMap.HasFiniteRange.comp_right, this needs no Noetherian hypothesis.

theorem LinearMap.IsFiniteRank.smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {S : Type u_5} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] {f : M →ₗ[R] N} (hf : f.IsFiniteRank) (c : S) : (c • f).IsFiniteRank

theorem LinearMap.IsFiniteRank.neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : f.IsFiniteRank) : (-f).IsFiniteRank

@[simp]

theorem LinearMap.IsFiniteRank.neg_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} : (-f).IsFiniteRank ↔ f.IsFiniteRank

Finite rank is invariant under negation.

theorem LinearMap.IsFiniteRank.sub {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {f g : M →ₗ[R] N} (hf : f.IsFiniteRank) (hg : g.IsFiniteRank) : (f - g).IsFiniteRank

theorem LinearMap.IsFiniteRank.hasFiniteRange {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherianRing R] {f : M →ₗ[R] N} (hf : f.IsFiniteRank) : f.HasFiniteRange

Over a Noetherian ring, a map of finite rank has finitely generated range.

theorem LinearMap.isFiniteRank_iff_hasFiniteRange {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherianRing R] {f : M →ₗ[R] N} : f.IsFiniteRank ↔ f.HasFiniteRange

Over a Noetherian ring, a linear map has finite rank if and only if its range is finitely generated.

theorem LinearMap.HasFiniteRange.injective_one_add_iff_surjective {K : Type u_5} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {F : V →ₗ[K] V} (hF : F.HasFiniteRange) : Function.Injective ⇑(1 + F) ↔ Function.Surjective ⇑(1 + F)

For a linear map F with finitely generated range, 1 + F is injective if and only if it is surjective (the Fredholm alternative for finite-rank perturbations of the identity).

theorem LinearMap.HasFiniteRange.injective_equiv_add_iff_surjective {K : Type u_5} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Type u_7} [AddCommGroup W] [Module K W] {e : V ≃ₗ[K] W} {w : V →ₗ[K] W} (hw : w.HasFiniteRange) : Function.Injective ⇑(↑e + w) ↔ Function.Surjective ⇑(↑e + w)

For a linear equivalence e and a linear map w with finitely generated range, e + w is injective if and only if it is surjective.