Documentation

TauCeti.LinearAlgebra.End.Split

Extending endomorphisms along a split surjection #

For linear maps π : F →ₗ[R] M and σ : M →ₗ[R] F with π ∘ₗ σ = id, LinearMap.splitEnd π σ h extends an endomorphism of M to F by the identity on ker π. This is a monoid homomorphism, and an extended endomorphism is invertible exactly when the original one is. The construction requires no freeness, finiteness or projectivity assumptions.

The evaluation and intertwining lemmas describe the extension without unfolding it. The affine formula LinearMap.splitEnd_one_sub is useful for characteristic polynomials, while the construction and its unit criterion also underlie determinants on finite projective modules. LinearMap.kerSplitEndEquiv identifies the kernel of an extension with the original kernel; in particular, extending by the identity does not add generalized spectral vectors at zero.

source
def LinearMap.splitEnd {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommMonoid M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) :
Module.End R M →* Module.End R F

Extend an endomorphism of a retract M of F by the identity on ker π.

Instances For
    source
    theorem LinearMap.splitEnd_apply {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommMonoid M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) :
    (π.splitEnd σ h) f = σ ∘ₗ f ∘ₗ π + (1 - σ ∘ₗ π)

    The extension acts by f on σ(M) and by the identity on ker π.

    source
    @[simp]
    theorem LinearMap.splitEnd_comp {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommMonoid M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) :
    (π.splitEnd σ h) f ∘ₗ σ = σ ∘ₗ f

    The section intertwines the original endomorphism and its extension.

    source
    @[simp]
    theorem LinearMap.comp_splitEnd {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) :
    π ∘ₗ (π.splitEnd σ h) f = f ∘ₗ π

    The retraction intertwines the extension and the original endomorphism.

    source
    def LinearMap.kerSplitEndEquiv {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) :
    ↥(ker ((π.splitEnd σ h) f)) ≃ₗ[R] ↥(ker f)

    The retraction and section identify the kernel of an extension by the identity with its original kernel. No freeness or finiteness hypothesis is needed.

    Instances For
      source
      @[simp]
      theorem LinearMap.coe_kerSplitEndEquiv_apply {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) (x : ↥(ker ((π.splitEnd σ h) f))) :
      ↑((π.kerSplitEndEquiv σ h f) x) = π ↑x

      The kernel equivalence for an extension applies the retraction.

      source
      @[simp]
      theorem LinearMap.coe_kerSplitEndEquiv_symm_apply {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) (x : ↥(ker f)) :
      ↑((π.kerSplitEndEquiv σ h f).symm x) = σ ↑x

      The inverse kernel equivalence for an extension applies the section.

      source
      theorem LinearMap.splitEnd_eq_one_add {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) :
      (π.splitEnd σ h) f = 1 + σ ∘ₗ (f - 1) ∘ₗ π

      Extending an endomorphism is an affine operation around the identity.

      source
      @[simp]
      theorem LinearMap.splitEnd_one_sub {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) :
      (π.splitEnd σ h) (1 - f) = 1 - σ ∘ₗ f ∘ₗ π

      Extending 1 - f gives 1 - σ ∘ₗ f ∘ₗ π.

      source
      @[simp]
      theorem LinearMap.isUnit_splitEnd_iff {R : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) :
      IsUnit ((π.splitEnd σ h) f) ↔ IsUnit f

      Extending by the identity preserves and reflects invertibility.