Generators of a module isomorphic to the base ring

A generator of a module N, that is an element x with span K {x} = ⊤, is carried by a linear isomorphism N ≃ₗ[K] K to a generator of the ideal ⊤, that is to a unit of K (Submodule.span_image_linearEquiv, Ideal.span_singleton_eq_top). So when 1 is the only unit of the commutative semiring K, as for ZMod 2, a module isomorphic to K has exactly one generator. This is what makes Thom classes with such coefficients unique on every fibre, without any orientation.

Conversely, a linear functional Ψ on a module N ≃ₗ[K] K taking the value 1 on x makes x a generator: Ψ factors through the isomorphism as multiplication by Ψ (e⁻¹ 1), so e x is a unit of K and a ↦ a • x is bijective.

Main results

• LinearEquiv.span_singleton_apply_eq_top_iff: a linear equivalence carries generators to generators.
• LinearEquiv.eq_of_span_singleton_eq_top: a module isomorphic to a commutative semiring whose only unit is 1 has a single generator.
• LinearEquiv.isUnit_apply_of_apply_eq_one, LinearEquiv.bijective_smul_of_apply_eq_one: an element on which a linear functional takes the value 1 is carried to a unit, and generates freely.

theorem LinearEquiv.span_singleton_apply_eq_top_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] (e : M ≃ₗ[R] N) {x : M} : R ∙ e x = ⊤ ↔ R ∙ x = ⊤

A linear equivalence carries generators to generators: e x spans the codomain if and only if x spans the domain.

theorem LinearEquiv.eq_of_span_singleton_eq_top {K : Type u_1} {N : Type u_2} [CommSemiring K] [Subsingleton Kˣ] [AddCommMonoid N] [Module K N] (φ : N ≃ₗ[K] K) {x y : N} (hx : K ∙ x = ⊤) (hy : K ∙ y = ⊤) : x = y

A module isomorphic to K has a single generator when 1 is the only unit of K: two elements x and y of a module N ≃ₗ[K] K with span K {x} = ⊤ and span K {y} = ⊤ are equal.

theorem LinearEquiv.isUnit_apply_of_apply_eq_one {K : Type u_1} {N : Type u_2} [CommSemiring K] [AddCommMonoid N] [Module K N] (e : N ≃ₗ[K] K) (Ψ : N →ₗ[K] K) {x : N} (hx : Ψ x = 1) : IsUnit (e x)

If a linear functional Ψ on a module N ≃ₗ[K] K takes the value 1 on x, then e x is a unit of K, with inverse Ψ (e⁻¹ 1).

theorem LinearEquiv.bijective_smul_of_apply_eq_one {K : Type u_1} {N : Type u_2} [CommSemiring K] [AddCommMonoid N] [Module K N] (e : N ≃ₗ[K] K) (Ψ : N →ₗ[K] K) {x : N} (hx : Ψ x = 1) : Function.Bijective fun (a : K) => a • x

If a linear functional Ψ on a module N ≃ₗ[K] K takes the value 1 on x, then a ↦ a • x is bijective.