Theorems · Definition · geometry

AffineMap.toConstProdLinearMap

(R : Type u_1) →
  {k : Type u_2} →
    {V1 : Type u_3} →
      {V2 : Type u_5} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : AddCommGroup V2] →
              [inst_3 : Module k V1] →
                [inst_4 : Module k V2] →
                  [inst_5 : Semiring R] →
                    [inst_6 : Module R V2] → [inst_7 : SMulCommClass k R V2] → (V1 →ᵃ[k] V2) ≃ₗ[R] V2 × (V1 →ₗ[k] V2)

The space of affine maps between two modules is linearly equivalent to the product of the domain with the space of linear maps, by taking the value of the affine map at (0 : V1) and the linear part. See note [bundled maps over different rings]

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Cited by

4 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupAddCommGroupModuleModuleSemiringModuleSMulCommClass