Theorems · Definition · geometry

AffineMap.pi

{k : Type u_2} →
  {V1 : Type u_3} →
    {P1 : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V1] →
          [inst_2 : AddTorsor V1 P1] →
            [inst_3 : Module k V1] →
              {ι : Type u_9} →
                {φv : ι → Type u_10} →
                  {φp : ι → Type u_11} →
                    [inst_4 : (i : ι) → AddCommGroup (φv i)] →
                      [inst_5 : (i : ι) → Module k (φv i)] →
                        [inst_6 : (i : ι) → AddTorsor (φv i) (φp i)] →
                          ((i : ι) → P1 →ᵃ[k] φp i) → P1 →ᵃ[k] (i : ι) → φp i

pi construction for affine maps. From a family of affine maps it produces an affine map into a family of affine spaces. This is the affine version of LinearMap.pi.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Cited by

6 results in Mathlib

Foundations

Depth 29 from the axioms · uses Classical.choice, Quot.sound

Assumes

RingAddCommGroupAddTorsorModuleAddCommGroupModuleAddTorsor