Documentation

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Affine maps #

This file defines affine maps.

Main definitions #

Notations #

Implementation notes #

outParam is used in the definition of [AddTorsor V P] to make V an implicit argument (deduced from P) in most cases. As for modules, k is an explicit argument rather than implied by P or V.

This file only provides purely algebraic definitions and results. Those depending on analysis or topology are defined elsewhere; see Analysis.NormedSpace.AddTorsor and Topology.Algebra.Affine.

References #

structure AffineMap (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
Type (max (max (max u_2 u_3) u_4) u_5)

An AffineMap k P1 P2 (notation: P1 →ᵃ[k] P2) is a map from P1 to P2 that induces a corresponding linear map from V1 to V2.

  • toFun : P1P2
  • linear : V1 →ₗ[k] V2
  • map_vadd' : ∀ (p : P1) (v : V1), self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p
Instances For
    theorem AffineMap.map_vadd' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (self : P1 →ᵃ[k] P2) (p : P1) (v : V1) :
    self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p

    An AffineMap k P1 P2 (notation: P1 →ᵃ[k] P2) is a map from P1 to P2 that induces a corresponding linear map from V1 to V2.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance AffineMap.instFunLike (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
      FunLike (P1 →ᵃ[k] P2) P1 P2
      Equations
      instance AffineMap.hasCoeToFun (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
      CoeFun (P1 →ᵃ[k] P2) fun (x : P1 →ᵃ[k] P2) => P1P2
      Equations
      def LinearMap.toAffineMap {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (f : V₁ →ₗ[k] V₂) :
      V₁ →ᵃ[k] V₂

      Reinterpret a linear map as an affine map.

      Equations
      • f.toAffineMap = { toFun := f, linear := f, map_vadd' := }
      Instances For
        @[simp]
        theorem LinearMap.coe_toAffineMap {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (f : V₁ →ₗ[k] V₂) :
        f.toAffineMap = f
        @[simp]
        theorem LinearMap.toAffineMap_linear {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (f : V₁ →ₗ[k] V₂) :
        f.toAffineMap.linear = f
        @[simp]
        theorem AffineMap.coe_mk {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (linear : V1 →ₗ[k] V2) (add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p) :
        { toFun := f, linear := linear, map_vadd' := add } = f

        Constructing an affine map and coercing back to a function produces the same map.

        @[simp]
        theorem AffineMap.toFun_eq_coe {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
        f.toFun = f

        toFun is the same as the result of coercing to a function.

        @[simp]
        theorem AffineMap.map_vadd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p : P1) (v : V1) :
        f (v +ᵥ p) = f.linear v +ᵥ f p

        An affine map on the result of adding a vector to a point produces the same result as the linear map applied to that vector, added to the affine map applied to that point.

        @[simp]
        theorem AffineMap.linearMap_vsub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p1 : P1) (p2 : P1) :
        f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2

        The linear map on the result of subtracting two points is the result of subtracting the result of the affine map on those two points.

        theorem AffineMap.ext {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} (h : ∀ (p : P1), f p = g p) :
        f = g

        Two affine maps are equal if they coerce to the same function.

        theorem AffineMap.ext_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} :
        f = g ∀ (p : P1), f p = g p
        theorem AffineMap.coeFn_injective {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
        Function.Injective DFunLike.coe
        theorem AffineMap.congr_arg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) {x : P1} {y : P1} (h : x = y) :
        f x = f y
        theorem AffineMap.congr_fun {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} (h : f = g) (x : P1) :
        f x = g x
        theorem AffineMap.ext_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} (h₁ : f.linear = g.linear) {p : P1} (h₂ : f p = g p) :
        f = g

        Two affine maps are equal if they have equal linear maps and are equal at some point.

        theorem AffineMap.ext_linear_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} :
        f = g f.linear = g.linear ∃ (p : P1), f p = g p

        Two affine maps are equal if they have equal linear maps and are equal at some point.

        def AffineMap.const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) :
        P1 →ᵃ[k] P2

        The constant function as an AffineMap.

        Equations
        Instances For
          @[simp]
          theorem AffineMap.coe_const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) :
          @[simp]
          theorem AffineMap.const_apply (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) (q : P1) :
          (AffineMap.const k P1 p) q = p
          @[simp]
          theorem AffineMap.const_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) :
          (AffineMap.const k P1 p).linear = 0
          theorem AffineMap.linear_eq_zero_iff_exists_const {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
          f.linear = 0 ∃ (q : P2), f = AffineMap.const k P1 q
          instance AffineMap.nonempty {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
          Equations
          • =
          def AffineMap.mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
          P1 →ᵃ[k] P2

          Construct an affine map by verifying the relation between the map and its linear part at one base point. Namely, this function takes a map f : P₁ → P₂, a linear map f' : V₁ →ₗ[k] V₂, and a point p such that for any other point p' we have f p' = f' (p' -ᵥ p) +ᵥ f p.

          Equations
          • AffineMap.mk' f f' p h = { toFun := f, linear := f', map_vadd' := }
          Instances For
            @[simp]
            theorem AffineMap.coe_mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
            (AffineMap.mk' f f' p h) = f
            @[simp]
            theorem AffineMap.mk'_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
            (AffineMap.mk' f f' p h).linear = f'
            instance AffineMap.mulAction {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] :
            MulAction R (P1 →ᵃ[k] V2)

            The space of affine maps to a module inherits an R-action from the action on its codomain.

            Equations
            @[simp]
            theorem AffineMap.coe_smul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] (c : R) (f : P1 →ᵃ[k] V2) :
            (c f) = c f
            @[simp]
            theorem AffineMap.smul_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] (t : R) (f : P1 →ᵃ[k] V2) :
            (t f).linear = t f.linear
            instance AffineMap.isCentralScalar {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] [DistribMulAction Rᵐᵒᵖ V2] [IsCentralScalar R V2] :
            Equations
            • =
            instance AffineMap.instZero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] :
            Zero (P1 →ᵃ[k] V2)
            Equations
            • AffineMap.instZero = { zero := { toFun := 0, linear := 0, map_vadd' := } }
            instance AffineMap.instAdd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] :
            Add (P1 →ᵃ[k] V2)
            Equations
            • AffineMap.instAdd = { add := fun (f g : P1 →ᵃ[k] V2) => { toFun := f + g, linear := f.linear + g.linear, map_vadd' := } }
            instance AffineMap.instSub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] :
            Sub (P1 →ᵃ[k] V2)
            Equations
            • AffineMap.instSub = { sub := fun (f g : P1 →ᵃ[k] V2) => { toFun := f - g, linear := f.linear - g.linear, map_vadd' := } }
            instance AffineMap.instNeg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] :
            Neg (P1 →ᵃ[k] V2)
            Equations
            • AffineMap.instNeg = { neg := fun (f : P1 →ᵃ[k] V2) => { toFun := -f, linear := -f.linear, map_vadd' := } }
            @[simp]
            theorem AffineMap.coe_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] :
            0 = 0
            @[simp]
            theorem AffineMap.coe_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
            (f + g) = f + g
            @[simp]
            theorem AffineMap.coe_neg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) :
            (-f) = -f
            @[simp]
            theorem AffineMap.coe_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
            (f - g) = f - g
            @[simp]
            theorem AffineMap.zero_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] :
            @[simp]
            theorem AffineMap.add_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
            (f + g).linear = f.linear + g.linear
            @[simp]
            theorem AffineMap.sub_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
            (f - g).linear = f.linear - g.linear
            @[simp]
            theorem AffineMap.neg_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) :
            (-f).linear = -f.linear
            instance AffineMap.instAddCommGroup {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] :

            The set of affine maps to a vector space is an additive commutative group.

            Equations
            instance AffineMap.instAddTorsor {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
            AddTorsor (P1 →ᵃ[k] V2) (P1 →ᵃ[k] P2)

            The space of affine maps from P1 to P2 is an affine space over the space of affine maps from P1 to the vector space V2 corresponding to P2.

            Equations
            @[simp]
            theorem AffineMap.vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) :
            (f +ᵥ g) p = f p +ᵥ g p
            @[simp]
            theorem AffineMap.vsub_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P2) (p : P1) :
            (f -ᵥ g) p = f p -ᵥ g p
            def AffineMap.fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
            P1 × P2 →ᵃ[k] P1

            Prod.fst as an AffineMap.

            Equations
            • AffineMap.fst = { toFun := Prod.fst, linear := LinearMap.fst k V1 V2, map_vadd' := }
            Instances For
              @[simp]
              theorem AffineMap.coe_fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
              AffineMap.fst = Prod.fst
              @[simp]
              theorem AffineMap.fst_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
              AffineMap.fst.linear = LinearMap.fst k V1 V2
              def AffineMap.snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
              P1 × P2 →ᵃ[k] P2

              Prod.snd as an AffineMap.

              Equations
              • AffineMap.snd = { toFun := Prod.snd, linear := LinearMap.snd k V1 V2, map_vadd' := }
              Instances For
                @[simp]
                theorem AffineMap.coe_snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
                AffineMap.snd = Prod.snd
                @[simp]
                theorem AffineMap.snd_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] :
                AffineMap.snd.linear = LinearMap.snd k V1 V2
                def AffineMap.id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] :
                P1 →ᵃ[k] P1

                Identity map as an affine map.

                Equations
                • AffineMap.id k P1 = { toFun := id, linear := LinearMap.id, map_vadd' := }
                Instances For
                  @[simp]
                  theorem AffineMap.coe_id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] :
                  (AffineMap.id k P1) = id

                  The identity affine map acts as the identity.

                  @[simp]
                  theorem AffineMap.id_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] :
                  (AffineMap.id k P1).linear = LinearMap.id
                  theorem AffineMap.id_apply (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) :
                  (AffineMap.id k P1) p = p

                  The identity affine map acts as the identity.

                  instance AffineMap.instInhabited {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] :
                  Equations
                  def AffineMap.comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) :
                  P1 →ᵃ[k] P3

                  Composition of affine maps.

                  Equations
                  • f.comp g = { toFun := f g, linear := f.linear ∘ₗ g.linear, map_vadd' := }
                  Instances For
                    @[simp]
                    theorem AffineMap.coe_comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) :
                    (f.comp g) = f g

                    Composition of affine maps acts as applying the two functions.

                    theorem AffineMap.comp_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1) :
                    (f.comp g) p = f (g p)

                    Composition of affine maps acts as applying the two functions.

                    @[simp]
                    theorem AffineMap.comp_id {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
                    f.comp (AffineMap.id k P1) = f
                    @[simp]
                    theorem AffineMap.id_comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
                    (AffineMap.id k P2).comp f = f
                    theorem AffineMap.comp_assoc {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} {V4 : Type u_8} {P4 : Type u_9} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] [AddCommGroup V4] [Module k V4] [AddTorsor V4 P4] (f₃₄ : P3 →ᵃ[k] P4) (f₂₃ : P2 →ᵃ[k] P3) (f₁₂ : P1 →ᵃ[k] P2) :
                    (f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)
                    instance AffineMap.instMonoid {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] :
                    Monoid (P1 →ᵃ[k] P1)
                    Equations
                    • AffineMap.instMonoid = Monoid.mk npowRec
                    @[simp]
                    theorem AffineMap.coe_mul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (f : P1 →ᵃ[k] P1) (g : P1 →ᵃ[k] P1) :
                    (f * g) = f g
                    @[simp]
                    theorem AffineMap.coe_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] :
                    1 = id
                    @[simp]
                    theorem AffineMap.linearHom_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (self : P1 →ᵃ[k] P1) :
                    AffineMap.linearHom self = self.linear
                    def AffineMap.linearHom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] :
                    (P1 →ᵃ[k] P1) →* V1 →ₗ[k] V1

                    AffineMap.linear on endomorphisms is a MonoidHom.

                    Equations
                    • AffineMap.linearHom = { toFun := AffineMap.linear, map_one' := , map_mul' := }
                    Instances For
                      @[simp]
                      theorem AffineMap.linear_injective_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
                      @[simp]
                      theorem AffineMap.linear_surjective_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
                      @[simp]
                      theorem AffineMap.linear_bijective_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
                      theorem AffineMap.image_vsub_image {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {s : Set P1} {t : Set P1} (f : P1 →ᵃ[k] P2) :
                      f '' s -ᵥ f '' t = f.linear '' (s -ᵥ t)

                      Definition of AffineMap.lineMap and lemmas about it #

                      def AffineMap.lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
                      k →ᵃ[k] P1

                      The affine map from k to P1 sending 0 to p₀ and 1 to p₁.

                      Equations
                      Instances For
                        theorem AffineMap.coe_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
                        (AffineMap.lineMap p₀ p₁) = fun (c : k) => c (p₁ -ᵥ p₀) +ᵥ p₀
                        theorem AffineMap.lineMap_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
                        (AffineMap.lineMap p₀ p₁) c = c (p₁ -ᵥ p₀) +ᵥ p₀
                        theorem AffineMap.lineMap_apply_module' {k : Type u_1} {V1 : Type u_2} [Ring k] [AddCommGroup V1] [Module k V1] (p₀ : V1) (p₁ : V1) (c : k) :
                        (AffineMap.lineMap p₀ p₁) c = c (p₁ - p₀) + p₀
                        theorem AffineMap.lineMap_apply_module {k : Type u_1} {V1 : Type u_2} [Ring k] [AddCommGroup V1] [Module k V1] (p₀ : V1) (p₁ : V1) (c : k) :
                        (AffineMap.lineMap p₀ p₁) c = (1 - c) p₀ + c p₁
                        theorem AffineMap.lineMap_apply_ring' {k : Type u_1} [Ring k] (a : k) (b : k) (c : k) :
                        (AffineMap.lineMap a b) c = c * (b - a) + a
                        theorem AffineMap.lineMap_apply_ring {k : Type u_1} [Ring k] (a : k) (b : k) (c : k) :
                        (AffineMap.lineMap a b) c = (1 - c) * a + c * b
                        theorem AffineMap.lineMap_vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) (v : V1) (c : k) :
                        (AffineMap.lineMap p (v +ᵥ p)) c = c v +ᵥ p
                        @[simp]
                        theorem AffineMap.lineMap_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
                        (AffineMap.lineMap p₀ p₁).linear = LinearMap.id.smulRight (p₁ -ᵥ p₀)
                        theorem AffineMap.lineMap_same_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) (c : k) :
                        @[simp]
                        theorem AffineMap.lineMap_same {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) :
                        @[simp]
                        theorem AffineMap.lineMap_apply_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
                        (AffineMap.lineMap p₀ p₁) 0 = p₀
                        @[simp]
                        theorem AffineMap.lineMap_apply_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
                        (AffineMap.lineMap p₀ p₁) 1 = p₁
                        @[simp]
                        theorem AffineMap.lineMap_eq_lineMap_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ : P1} {p₁ : P1} {c₁ : k} {c₂ : k} :
                        (AffineMap.lineMap p₀ p₁) c₁ = (AffineMap.lineMap p₀ p₁) c₂ p₀ = p₁ c₁ = c₂
                        @[simp]
                        theorem AffineMap.lineMap_eq_left_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ : P1} {p₁ : P1} {c : k} :
                        (AffineMap.lineMap p₀ p₁) c = p₀ p₀ = p₁ c = 0
                        @[simp]
                        theorem AffineMap.lineMap_eq_right_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ : P1} {p₁ : P1} {c : k} :
                        (AffineMap.lineMap p₀ p₁) c = p₁ p₀ = p₁ c = 1
                        theorem AffineMap.lineMap_injective (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ : P1} {p₁ : P1} (h : p₀ p₁) :
                        @[simp]
                        theorem AffineMap.apply_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ : P1) (p₁ : P1) (c : k) :
                        f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c
                        @[simp]
                        theorem AffineMap.comp_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ : P1) (p₁ : P1) :
                        f.comp (AffineMap.lineMap p₀ p₁) = AffineMap.lineMap (f p₀) (f p₁)
                        @[simp]
                        theorem AffineMap.fst_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p₀ : P1 × P2) (p₁ : P1 × P2) (c : k) :
                        ((AffineMap.lineMap p₀ p₁) c).1 = (AffineMap.lineMap p₀.1 p₁.1) c
                        @[simp]
                        theorem AffineMap.snd_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p₀ : P1 × P2) (p₁ : P1 × P2) (c : k) :
                        ((AffineMap.lineMap p₀ p₁) c).2 = (AffineMap.lineMap p₀.2 p₁.2) c
                        theorem AffineMap.lineMap_symm {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
                        AffineMap.lineMap p₀ p₁ = (AffineMap.lineMap p₁ p₀).comp (AffineMap.lineMap 1 0)
                        theorem AffineMap.lineMap_apply_one_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
                        (AffineMap.lineMap p₀ p₁) (1 - c) = (AffineMap.lineMap p₁ p₀) c
                        @[simp]
                        theorem AffineMap.lineMap_vsub_left {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
                        (AffineMap.lineMap p₀ p₁) c -ᵥ p₀ = c (p₁ -ᵥ p₀)
                        @[simp]
                        theorem AffineMap.left_vsub_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
                        p₀ -ᵥ (AffineMap.lineMap p₀ p₁) c = c (p₀ -ᵥ p₁)
                        @[simp]
                        theorem AffineMap.lineMap_vsub_right {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
                        (AffineMap.lineMap p₀ p₁) c -ᵥ p₁ = (1 - c) (p₀ -ᵥ p₁)
                        @[simp]
                        theorem AffineMap.right_vsub_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
                        p₁ -ᵥ (AffineMap.lineMap p₀ p₁) c = (1 - c) (p₁ -ᵥ p₀)
                        theorem AffineMap.lineMap_vadd_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (v₁ : V1) (v₂ : V1) (p₁ : P1) (p₂ : P1) (c : k) :
                        (AffineMap.lineMap v₁ v₂) c +ᵥ (AffineMap.lineMap p₁ p₂) c = (AffineMap.lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂)) c
                        theorem AffineMap.lineMap_vsub_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₁ : P1) (p₂ : P1) (p₃ : P1) (p₄ : P1) (c : k) :
                        (AffineMap.lineMap p₁ p₂) c -ᵥ (AffineMap.lineMap p₃ p₄) c = (AffineMap.lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)) c
                        theorem AffineMap.decomp {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddCommGroup V2] [Module k V2] (f : V1 →ᵃ[k] V2) :
                        f = f.linear + fun (x : V1) => f 0

                        Decomposition of an affine map in the special case when the point space and vector space are the same.

                        theorem AffineMap.decomp' {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddCommGroup V2] [Module k V2] (f : V1 →ᵃ[k] V2) :
                        f.linear = f - fun (x : V1) => f 0

                        Decomposition of an affine map in the special case when the point space and vector space are the same.

                        theorem AffineMap.image_uIcc {k : Type u_10} [LinearOrderedField k] (f : k →ᵃ[k] k) (a : k) (b : k) :
                        f '' Set.uIcc a b = Set.uIcc (f a) (f b)
                        def AffineMap.proj {k : Type u_1} [Ring k] {ι : Type u_10} {V : ιType u_11} {P : ιType u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (i : ι) :
                        ((i : ι) → P i) →ᵃ[k] P i

                        Evaluation at a point as an affine map.

                        Equations
                        Instances For
                          @[simp]
                          theorem AffineMap.proj_apply {k : Type u_1} [Ring k] {ι : Type u_10} {V : ιType u_11} {P : ιType u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (i : ι) (f : (i : ι) → P i) :
                          (AffineMap.proj i) f = f i
                          @[simp]
                          theorem AffineMap.proj_linear {k : Type u_1} [Ring k] {ι : Type u_10} {V : ιType u_11} {P : ιType u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (i : ι) :
                          theorem AffineMap.pi_lineMap_apply {k : Type u_1} [Ring k] {ι : Type u_10} {V : ιType u_11} {P : ιType u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (f : (i : ι) → P i) (g : (i : ι) → P i) (c : k) (i : ι) :
                          (AffineMap.lineMap f g) c i = (AffineMap.lineMap (f i) (g i)) c
                          instance AffineMap.distribMulAction {R : Type u_1} {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V1] [Module k V2] [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] :

                          The space of affine maps to a module inherits an R-action from the action on its codomain.

                          Equations
                          instance AffineMap.instModule {R : Type u_1} {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [SMulCommClass k R V2] :
                          Module R (P1 →ᵃ[k] V2)

                          The space of affine maps taking values in an R-module is an R-module.

                          Equations
                          • AffineMap.instModule = let __src := AffineMap.distribMulAction; Module.mk
                          @[simp]
                          theorem AffineMap.toConstProdLinearMap_apply (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [SMulCommClass k R V2] (f : V1 →ᵃ[k] V2) :
                          (AffineMap.toConstProdLinearMap R) f = (f 0, f.linear)
                          @[simp]
                          theorem AffineMap.toConstProdLinearMap_symm_apply (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [SMulCommClass k R V2] (p : V2 × (V1 →ₗ[k] V2)) :
                          (AffineMap.toConstProdLinearMap R).symm p = p.2.toAffineMap + AffineMap.const k V1 p.1
                          def AffineMap.toConstProdLinearMap (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [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]

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def AffineMap.pi {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ιType u_10} {φp : ιType u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (f : (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.

                            Equations
                            • AffineMap.pi f = { toFun := fun (m : P1) (a : ι) => (f a) m, linear := LinearMap.pi fun (a : ι) => (f a).linear, map_vadd' := }
                            Instances For
                              @[simp]
                              theorem AffineMap.pi_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ιType u_10} {φp : ιType u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (c : P1) (i : ι) :
                              (AffineMap.pi fp) c i = (fp i) c
                              theorem AffineMap.pi_comp {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V3 : Type u_7} {P3 : Type u_8} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [AddCommGroup V3] [AddTorsor V3 P3] [Module k V1] [Module k V3] {ι : Type u_9} {φv : ιType u_10} {φp : ιType u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (g : P3 →ᵃ[k] P1) :
                              (AffineMap.pi fp).comp g = AffineMap.pi fun (i : ι) => (fp i).comp g
                              theorem AffineMap.pi_eq_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] (fv : (i : ι) → P1 →ᵃ[k] φv i) :
                              AffineMap.pi fv = 0 ∀ (i : ι), fv i = 0
                              theorem AffineMap.pi_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] :
                              (AffineMap.pi fun (x : ι) => 0) = 0
                              theorem AffineMap.proj_pi {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ιType u_10} {φp : ιType u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (i : ι) :
                              (AffineMap.proj i).comp (AffineMap.pi fp) = fp i
                              theorem AffineMap.pi_ext_zero {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [AddCommGroup V2] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [Finite ι] [DecidableEq ι] {f : ((i : ι) → φv i) →ᵃ[k] P2} {g : ((i : ι) → φv i) →ᵃ[k] P2} (h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)) (h₂ : f 0 = g 0) :
                              f = g

                              Two affine maps from a Pi-tyoe of modules (i : ι) → φv i are equal if they are equal in their operation on Pi.single and at zero. Analogous to LinearMap.pi_ext. See also pi_ext_nonempty, which instead of agrement at zero requires Nonempty ι.

                              theorem AffineMap.pi_ext_nonempty {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [AddCommGroup V2] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [Finite ι] [DecidableEq ι] {f : ((i : ι) → φv i) →ᵃ[k] P2} {g : ((i : ι) → φv i) →ᵃ[k] P2} [Nonempty ι] (h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)) :
                              f = g

                              Two affine maps from a Pi-tyoe of modules (i : ι) → φv i are equal if they are equal in their operation on Pi.single and ι is nonempty. Analogous to LinearMap.pi_ext. See also pi_ext_zero, which instead Nonempty ι requires agreement at 0.

                              theorem AffineMap.pi_ext_nonempty' {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [AddCommGroup V2] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [Finite ι] [DecidableEq ι] {f : ((i : ι) → φv i) →ᵃ[k] P2} {g : ((i : ι) → φv i) →ᵃ[k] P2} [Nonempty ι] (h : ∀ (i : ι), f.comp (LinearMap.single i).toAffineMap = g.comp (LinearMap.single i).toAffineMap) :
                              f = g

                              This is used as the ext lemma instead of AffineMap.pi_ext_nonempty for reasons explained in note [partially-applied ext lemmas]. Analogous to LinearMap.pi_ext'

                              def AffineMap.homothety {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) :
                              P1 →ᵃ[k] P1

                              homothety c r is the homothety (also known as dilation) about c with scale factor r.

                              Equations
                              Instances For
                                theorem AffineMap.homothety_def {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) :
                                theorem AffineMap.homothety_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) (p : P1) :
                                (AffineMap.homothety c r) p = r (p -ᵥ c) +ᵥ c
                                theorem AffineMap.homothety_eq_lineMap {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) (p : P1) :
                                @[simp]
                                theorem AffineMap.homothety_one {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) :
                                @[simp]
                                theorem AffineMap.homothety_apply_same {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) :
                                theorem AffineMap.homothety_mul_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ : k) (r₂ : k) (p : P1) :
                                (AffineMap.homothety c (r₁ * r₂)) p = (AffineMap.homothety c r₁) ((AffineMap.homothety c r₂) p)
                                theorem AffineMap.homothety_mul {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ : k) (r₂ : k) :
                                AffineMap.homothety c (r₁ * r₂) = (AffineMap.homothety c r₁).comp (AffineMap.homothety c r₂)
                                @[simp]
                                theorem AffineMap.homothety_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) :
                                @[simp]
                                theorem AffineMap.homothety_add {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ : k) (r₂ : k) :
                                def AffineMap.homothetyHom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) :
                                k →* P1 →ᵃ[k] P1

                                homothety as a multiplicative monoid homomorphism.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem AffineMap.coe_homothetyHom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) :
                                  def AffineMap.homothetyAffine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) :
                                  k →ᵃ[k] P1 →ᵃ[k] P1

                                  homothety as an affine map.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem AffineMap.coe_homothetyAffine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) :
                                    theorem Convex.combo_affine_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] {x : E} {y : E} {a : 𝕜} {b : 𝕜} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :
                                    f (a x + b y) = a f x + b f y

                                    Applying an affine map to an affine combination of two points yields an affine combination of the images.