Linear maps and duality

Vector spaces and modules, linear maps and their invariants such as trace, dual spaces, dual bases and perfect pairings, and exactness of sequences of linear maps.

DefinitionEvaluation of an affine function at two points#✓fully proved

Evaluation of the affine function x ↦ slope * x + intercept at two distinct points.

def affineEvaluation (theta theta' : F) (h : theta ≠ theta') : (F × F) ≃ₗ[F] (F × F) where
  toFun p := (p.1 * theta + p.2, p.1 * theta' + p.2)
  invFun p := ((p.1 - p.2) / (theta - theta'),
    p.1 - (p.1 - p.2) / (theta - theta') * theta)
  map_add' p q := by
    ext <;> dsimp <;> ring
  map_smul' c p := by
    ext <;> dsimp <;> ring
  left_inv p := by
    ext <;> dsimp <;> field_simp [sub_ne_zero.mpr h] <;> ring
  right_inv p := by
    ext <;> dsimp <;> field_simp [sub_ne_zero.mpr h] <;> ring

TheoremHom detects exact sequences ending in a surjection#✓fully proved

Let \(R\) be a commutative ring, let \(M\), \(N\), \(P\) be \(R\)-modules, and let \(\varphi : M \to N\) and \(\psi : N \to P\) be \(R\)-linear maps. Then the image of \(\varphi\) equals the kernel of \(\psi\) and \(\psi\) is surjective if and only if, for every \(R\)-module \(D\) in the same universe as \(N\) and \(P\), precomposition with \(\psi\), \(g \mapsto g \circ \psi\), is an injective map \(\operatorname{Hom}_R(P, D) \to \operatorname{Hom}_R(N, D)\) whose image is the kernel of precomposition with \(\varphi\), \(h \mapsto h \circ \varphi\), as a map \(\operatorname{Hom}_R(N, D) \to \operatorname{Hom}_R(M, D)\).

theorem exact_and_surjective_iff_forall_lcomp
    (φ : M →ₗ[R] N) (ψ : N →ₗ[R] P) :
    (Function.Exact φ ψ ∧ Function.Surjective ψ) ↔
      ∀ (D : Type w) [AddCommGroup D] [Module R D],
        Function.Injective (lcomp R D ψ) ∧
        Function.Exact (lcomp R D ψ) (lcomp R D φ)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.