Counting a module along the range and the kernel of a linear map

For a linear map f : M →ₗ[R] N the first isomorphism theorem identifies M ⧸ ker f with range f, so the cardinality of M is the product of the cardinalities of the range and of the kernel. Both sides are Nat.card, which is 0 on an infinite type, so no finiteness hypothesis is needed: the statement also says that M is infinite exactly when the range or the kernel is.

The second result records that the range of a linear map depends only on the map up to an isomorphism of arrows: two linear maps intertwined by linear equivalences on the source and on the target have ranges of the same cardinality.

Both are the counting steps of an exact-sequence argument, where a term is compared with the image of the map leaving it and the image of the map entering it.

theorem LinearMap.card_eq_card_range_mul_card_ker {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) : Nat.card M = Nat.card ↥f.range * Nat.card ↥f.ker

The cardinality of the source of a linear map is the product of the cardinalities of its range and of its kernel.

theorem LinearMap.card_range_eq_card_range_of_comp_eq {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_4} {N' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] (f : M →ₗ[R] N) (f' : M' →ₗ[R] N') (e : M ≃ₗ[R] M') (e' : N ≃ₗ[R] N') (h : ↑e' ∘ₗ f = f' ∘ₗ ↑e) : Nat.card ↥f.range = Nat.card ↥f'.range

Linear maps intertwined by linear equivalences on the source and on the target have ranges of the same cardinality.