Unimodular elements and a free rank-one summand

This file contains the unconditional module-theoretic splitting associated to a unimodular element. It uses no rank, Ore, simplicity, or finiteness hypothesis.

def AlgebraicAnalysis.Unimodular.IsUnimodular {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (x : N) : Prop

An element of a left module is unimodular if a left-linear functional takes it to 1.

Equations

• AlgebraicAnalysis.Unimodular.IsUnimodular x = ∃ (φ : N →ₗ[R] R), φ x = 1

theorem AlgebraicAnalysis.Unimodular.exists_unimodular_iff_surjective {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] : (∃ (x : N), IsUnimodular x) ↔ ∃ (φ : N →ₗ[R] R), Function.Surjective ⇑φ

def AlgebraicAnalysis.Unimodular.unimodularKernelProjection {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (φ : N →ₗ[R] R) (x : N) (hx : φ x = 1) : N →ₗ[R] ↥φ.ker

The projection onto the kernel of a functional which is normalized at x.

Equations

• AlgebraicAnalysis.Unimodular.unimodularKernelProjection φ x hx = LinearMap.codRestrict φ.ker (LinearMap.id - LinearMap.toSpanSingleton R N x ∘ₗ φ) ⋯

def AlgebraicAnalysis.Unimodular.unimodularSplitMap {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (φ : N →ₗ[R] R) (x : N) (hx : φ x = 1) : N →ₗ[R] ↥φ.ker × R

The canonical splitting map associated to a normalized functional.

Equations

• AlgebraicAnalysis.Unimodular.unimodularSplitMap φ x hx = (AlgebraicAnalysis.Unimodular.unimodularKernelProjection φ x hx).prod φ

def AlgebraicAnalysis.Unimodular.unimodularSplitMapInv {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (φ : N →ₗ[R] R) (x : N) : ↥φ.ker × R →ₗ[R] N

The inverse map to unimodularSplitMap.

Equations

• AlgebraicAnalysis.Unimodular.unimodularSplitMapInv φ x = { toFun := fun (y : ↥φ.ker × R) => ↑y.1 + y.2 • x, map_add' := ⋯, map_smul' := ⋯ }

theorem AlgebraicAnalysis.Unimodular.unimodularSplitMap_left_inverse {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (φ : N →ₗ[R] R) (x : N) (hx : φ x = 1) : unimodularSplitMapInv φ x ∘ₗ unimodularSplitMap φ x hx = LinearMap.id

theorem AlgebraicAnalysis.Unimodular.unimodularSplitMap_right_inverse {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (φ : N →ₗ[R] R) (x : N) (hx : φ x = 1) : unimodularSplitMap φ x hx ∘ₗ unimodularSplitMapInv φ x = LinearMap.id

def AlgebraicAnalysis.Unimodular.unimodularSplitEquiv {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (φ : N →ₗ[R] R) (x : N) (hx : φ x = 1) : N ≃ₗ[R] ↥φ.ker × R

A unimodular element splits off a free rank-one factor.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicAnalysis.Unimodular.unimodular_split {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (x : N) (hx : IsUnimodular x) : ∃ (φ : N →ₗ[R] R) (_ : φ x = 1), Nonempty (N ≃ₗ[R] ↥φ.ker × R)

theorem AlgebraicAnalysis.Unimodular.unimodular_span_singleton_free {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] (x : N) (hx : IsUnimodular x) : Module.Free R ↥(LinearMap.toSpanSingleton R N x).range

The cyclic submodule generated by a unimodular element is a free rank-one module. The target is the actual range, so no commutativity or centrality assumption on R is hidden in the statement.

theorem AlgebraicAnalysis.Unimodular.projective_ker_of_unimodular {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] [Module.Projective R N] (φ : N →ₗ[R] R) (x : N) (hx : φ x = 1) : Module.Projective R ↥φ.ker

The kernel of a split functional is a direct summand of its domain. In particular, if the domain is projective then this kernel is projective.