Documentation

Mathlib.Algebra.AddConstMap.Basic

Maps (semi)conjugating a shift to a shift #

Denote by $S^1$ the unit circle UnitAddCircle. A common way to study a self-map $f\colon S^1\to S^1$ of degree 1 is to lift it to a map $\tilde f\colon \mathbb R\to \mathbb R$ such that $\tilde f(x + 1) = \tilde f(x)+1$ for all x.

In this file we define a structure and a typeclass for bundled maps satisfying f (x + a) = f x + b.

We use parameters a and b instead of 1 to accommodate for two use cases:

structure AddConstMap (G : Type u_1) (H : Type u_2) [Add G] [Add H] (a : G) (b : H) :
Type (max u_1 u_2)

A bundled map f : G → H such that f (x + a) = f x + b for all x.

One can think about f as a lift to G of a map between two AddCircles.

  • toFun : GH

    The underlying function of an AddConstMap. Use automatic coercion to function instead.

  • map_add_const' : ∀ (x : G), self.toFun (x + a) = self.toFun x + b

    An AddConstMap satisfies f (x + a) = f x + b. Use map_add_const instead.

Instances For
    theorem AddConstMap.map_add_const' {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (self : AddConstMap G H a b) (x : G) :
    self.toFun (x + a) = self.toFun x + b

    An AddConstMap satisfies f (x + a) = f x + b. Use map_add_const instead.

    A bundled map f : G → H such that f (x + a) = f x + b for all x.

    One can think about f as a lift to G of a map between two AddCircles.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      class AddConstMapClass (F : Type u_1) (G : outParam (Type u_2)) (H : outParam (Type u_3)) [Add G] [Add H] (a : outParam G) (b : outParam H) [FunLike F G H] :

      Typeclass for maps satisfying f (x + a) = f x + b.

      Note that a and b are outParams, so one should not add instances like [AddConstMapClass F G H a b] : AddConstMapClass F G H (-a) (-b).

      • map_add_const : ∀ (f : F) (x : G), f (x + a) = f x + b

        A map of AddConstMapClass class semiconjugates shift by a to the shift by b: ∀ x, f (x + a) = f x + b.

      Instances
        theorem AddConstMapClass.map_add_const {F : Type u_1} {G : outParam (Type u_2)} {H : outParam (Type u_3)} [Add G] [Add H] {a : outParam G} {b : outParam H} [FunLike F G H] [self : AddConstMapClass F G H a b] (f : F) (x : G) :
        f (x + a) = f x + b

        A map of AddConstMapClass class semiconjugates shift by a to the shift by b: ∀ x, f (x + a) = f x + b.

        Properties of AddConstMapClass maps #

        In this section we prove properties like f (x + n • a) = f x + n • b.

        theorem AddConstMapClass.semiconj {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [Add G] [Add H] [AddConstMapClass F G H a b] (f : F) :
        Function.Semiconj (⇑f) (fun (x : G) => x + a) fun (x : H) => x + b
        theorem AddConstMapClass.map_add_nsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ) :
        f (x + n a) = f x + n b
        theorem AddConstMapClass.map_add_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ) :
        f (x + n) = f x + n b
        theorem AddConstMapClass.map_add_one {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :
        f (x + 1) = f x + b
        theorem AddConstMapClass.map_add_ofNat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ) [n.AtLeastTwo] :
        f (x + OfNat.ofNat n) = f x + OfNat.ofNat n b
        theorem AddConstMapClass.map_add_nat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ) :
        f (x + n) = f x + n
        theorem AddConstMapClass.map_add_ofNat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ) [n.AtLeastTwo] :
        f (x + OfNat.ofNat n) = f x + OfNat.ofNat n
        theorem AddConstMapClass.map_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddZeroClass G] [Add H] [AddConstMapClass F G H a b] (f : F) :
        f a = f 0 + b
        theorem AddConstMapClass.map_one {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddZeroClass G] [One G] [Add H] [AddConstMapClass F G H 1 b] (f : F) :
        f 1 = f 0 + b
        theorem AddConstMapClass.map_nsmul_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ) :
        f (n a) = f 0 + n b
        theorem AddConstMapClass.map_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ) :
        f n = f 0 + n b
        theorem AddConstMapClass.map_ofNat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ) [n.AtLeastTwo] :
        f (OfNat.ofNat n) = f 0 + OfNat.ofNat n b
        theorem AddConstMapClass.map_nat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ) :
        f n = f 0 + n
        theorem AddConstMapClass.map_ofNat {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ) [n.AtLeastTwo] :
        theorem AddConstMapClass.map_const_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommSemigroup G] [Add H] [AddConstMapClass F G H a b] (f : F) (x : G) :
        f (a + x) = f x + b
        theorem AddConstMapClass.map_one_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :
        f (1 + x) = f x + b
        theorem AddConstMapClass.map_nsmul_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ) (x : G) :
        f (n a + x) = f x + n b
        theorem AddConstMapClass.map_nat_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ) (x : G) :
        f (n + x) = f x + n b
        theorem AddConstMapClass.map_ofNat_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ) [n.AtLeastTwo] (x : G) :
        f (OfNat.ofNat n + x) = f x + OfNat.ofNat n b
        theorem AddConstMapClass.map_nat_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ) (x : G) :
        f (n + x) = f x + n
        theorem AddConstMapClass.map_ofNat_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddCommMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ) [n.AtLeastTwo] (x : G) :
        f (OfNat.ofNat n + x) = f x + OfNat.ofNat n
        theorem AddConstMapClass.map_sub_nsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ) :
        f (x - n a) = f x - n b
        theorem AddConstMapClass.map_sub_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) :
        f (x - a) = f x - b
        theorem AddConstMapClass.map_sub_one {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroup G] [One G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) :
        f (x - 1) = f x - b
        theorem AddConstMapClass.map_sub_nat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ) :
        f (x - n) = f x - n b
        theorem AddConstMapClass.map_sub_ofNat' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ) [n.AtLeastTwo] :
        f (x - OfNat.ofNat n) = f x - OfNat.ofNat n b
        theorem AddConstMapClass.map_add_zsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ) :
        f (x + n a) = f x + n b
        theorem AddConstMapClass.map_zsmul_const {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ) :
        f (n a) = f 0 + n b
        theorem AddConstMapClass.map_add_int' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ) :
        f (x + n) = f x + n b
        theorem AddConstMapClass.map_add_int {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ) :
        f (x + n) = f x + n
        theorem AddConstMapClass.map_sub_zsmul {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ) :
        f (x - n a) = f x - n b
        theorem AddConstMapClass.map_sub_int' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ) :
        f (x - n) = f x - n b
        theorem AddConstMapClass.map_sub_int {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ) :
        f (x - n) = f x - n
        theorem AddConstMapClass.map_zsmul_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ) (x : G) :
        f (n a + x) = f x + n b
        theorem AddConstMapClass.map_int_add' {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {b : H} [AddCommGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (n : ) (x : G) :
        f (n + x) = f x + n b
        theorem AddConstMapClass.map_int_add {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] [AddCommGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ) (x : G) :
        f (n + x) = f x + n
        theorem AddConstMapClass.map_fract {F : Type u_1} {H : Type u_3} {b : H} {R : Type u_4} [LinearOrderedRing R] [FloorRing R] [AddGroup H] [FunLike F R H] [AddConstMapClass F R H 1 b] (f : F) (x : R) :
        f (Int.fract x) = f x - x b
        theorem AddConstMapClass.rel_map_of_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [AddGroup H] [AddConstMapClass F G H a b] {f : F} {R : HHProp} [IsTrans H R] [hR : CovariantClass H H (fun (x y : H) => y + x) R] (ha : 0 < a) {l : G} (hf : xSet.Icc l (l + a), ySet.Icc l (l + a), x < yR (f x) (f y)) :
        ((fun (x1 x2 : G) => x1 < x2) R) f f

        Auxiliary lemmas for the "monotonicity on a fundamental interval implies monotonicity" lemmas. We formulate it for any relation so that the proof works both for Monotone and StrictMono.

        theorem AddConstMapClass.monotone_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
        Monotone f MonotoneOn (⇑f) (Set.Icc l (l + a))
        theorem AddConstMapClass.antitone_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
        Antitone f AntitoneOn (⇑f) (Set.Icc l (l + a))
        theorem AddConstMapClass.strictMono_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
        StrictMono f StrictMonoOn (⇑f) (Set.Icc l (l + a))
        theorem AddConstMapClass.strictAnti_iff_Icc {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [LinearOrderedAddCommGroup G] [Archimedean G] [OrderedAddCommGroup H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
        StrictAnti f StrictAntiOn (⇑f) (Set.Icc l (l + a))

        Coercion to function #

        instance AddConstMap.instFunLike {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} :
        FunLike (AddConstMap G H a b) G H
        Equations
        • AddConstMap.instFunLike = { coe := AddConstMap.toFun, coe_injective' := }
        @[simp]
        theorem AddConstMap.coe_mk {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : GH) (hf : ∀ (x : G), f (x + a) = f x + b) :
        { toFun := f, map_add_const' := hf } = f
        @[simp]
        theorem AddConstMap.mk_coe {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :
        { toFun := f, map_add_const' := } = f
        @[simp]
        theorem AddConstMap.toFun_eq_coe {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :
        f.toFun = f
        instance AddConstMap.instAddConstMapClass {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} :
        AddConstMapClass (AddConstMap G H a b) G H a b
        Equations
        • =
        theorem AddConstMap.ext_iff {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {f : AddConstMap G H a b} {g : AddConstMap G H a b} :
        f = g ∀ (x : G), f x = g x
        theorem AddConstMap.ext {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {f : AddConstMap G H a b} {g : AddConstMap G H a b} (h : ∀ (x : G), f x = g x) :
        f = g

        Constructions about G →+c[a, b] H #

        @[simp]
        theorem AddConstMap.coe_id {G : Type u_1} [Add G] {a : G} :
        AddConstMap.id = id
        def AddConstMap.id {G : Type u_1} [Add G] {a : G} :
        AddConstMap G G a a

        The identity map as G →+c[a, a] G.

        Equations
        • AddConstMap.id = { toFun := id, map_add_const' := }
        Instances For
          instance AddConstMap.instInhabited {G : Type u_1} [Add G] {a : G} :
          Equations
          • AddConstMap.instInhabited = { default := AddConstMap.id }
          @[simp]
          theorem AddConstMap.coe_comp {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [Add K] {c : K} (g : AddConstMap H K b c) (f : AddConstMap G H a b) :
          (g.comp f) = g f
          def AddConstMap.comp {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [Add K] {c : K} (g : AddConstMap H K b c) (f : AddConstMap G H a b) :
          AddConstMap G K a c

          Composition of two AddConstMaps.

          Equations
          • g.comp f = { toFun := g f, map_add_const' := }
          Instances For
            @[simp]
            theorem AddConstMap.comp_id {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :
            f.comp AddConstMap.id = f
            @[simp]
            theorem AddConstMap.id_comp {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) :
            AddConstMap.id.comp f = f
            @[simp]
            theorem AddConstMap.coe_replaceConsts {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) (a' : G) (b' : H) (ha : a = a') (hb : b = b') :
            (f.replaceConsts a' b' ha hb) = f
            def AddConstMap.replaceConsts {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (f : AddConstMap G H a b) (a' : G) (b' : H) (ha : a = a') (hb : b = b') :
            AddConstMap G H a' b'

            Change constants a and b in (f : G →+c[a, b] H) to improve definitional equalities.

            Equations
            • f.replaceConsts a' b' ha hb = { toFun := f, map_add_const' := }
            Instances For

              Additive action on G →+c[a, b] H #

              instance AddConstMap.instVAddOfVAddAssocClass {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [VAdd K H] [VAddAssocClass K H H] :
              VAdd K (AddConstMap G H a b)

              If f is an AddConstMap, then so is (c +ᵥ f ·).

              Equations
              • AddConstMap.instVAddOfVAddAssocClass = { vadd := fun (c : K) (f : AddConstMap G H a b) => { toFun := c +ᵥ f, map_add_const' := } }
              @[simp]
              theorem AddConstMap.coe_vadd {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [VAdd K H] [VAddAssocClass K H H] (c : K) (f : AddConstMap G H a b) :
              (c +ᵥ f) = c +ᵥ f
              instance AddConstMap.instAddActionOfVAddAssocClass {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {K : Type u_3} [AddMonoid K] [AddAction K H] [VAddAssocClass K H H] :
              Equations

              Monoid structure on endomorphisms G →+c[a, a] G #

              instance AddConstMap.instMul {G : Type u_1} [Add G] {a : G} :
              Mul (AddConstMap G G a a)
              Equations
              • AddConstMap.instMul = { mul := AddConstMap.comp }
              instance AddConstMap.instOne {G : Type u_1} [Add G] {a : G} :
              One (AddConstMap G G a a)
              Equations
              • AddConstMap.instOne = { one := AddConstMap.id }
              instance AddConstMap.instPowNat {G : Type u_1} [Add G] {a : G} :
              Pow (AddConstMap G G a a)
              Equations
              • AddConstMap.instPowNat = { pow := fun (f : AddConstMap G G a a) (n : ) => { toFun := (⇑f)^[n], map_add_const' := } }
              instance AddConstMap.instMonoid {G : Type u_1} [Add G] {a : G} :
              Equations
              theorem AddConstMap.mul_def {G : Type u_1} [Add G] {a : G} (f : AddConstMap G G a a) (g : AddConstMap G G a a) :
              f * g = f.comp g
              @[simp]
              theorem AddConstMap.coe_mul {G : Type u_1} [Add G] {a : G} (f : AddConstMap G G a a) (g : AddConstMap G G a a) :
              (f * g) = f g
              theorem AddConstMap.one_def {G : Type u_1} [Add G] {a : G} :
              1 = AddConstMap.id
              @[simp]
              theorem AddConstMap.coe_one {G : Type u_1} [Add G] {a : G} :
              1 = id
              @[simp]
              theorem AddConstMap.coe_pow {G : Type u_1} [Add G] {a : G} (f : AddConstMap G G a a) (n : ) :
              (f ^ n) = (⇑f)^[n]
              theorem AddConstMap.pow_apply {G : Type u_1} [Add G] {a : G} (f : AddConstMap G G a a) (n : ) (x : G) :
              (f ^ n) x = (⇑f)^[n] x
              @[simp]
              theorem AddConstMap.toEnd_apply {G : Type u_1} [Add G] {a : G} :
              AddConstMap.toEnd = DFunLike.coe
              def AddConstMap.toEnd {G : Type u_1} [Add G] {a : G} :

              Coercion to functions as a monoid homomorphism to Function.End G.

              Equations
              • AddConstMap.toEnd = { toFun := DFunLike.coe, map_one' := , map_mul' := }
              Instances For

                Multiplicative action on (b : H) × (G →+c[a, b] H) #

                If K acts distributively on H, then for each f : G →+c[a, b] H we define (AddConstMap.smul c f : G →+c[a, c • b] H).

                One can show that this defines a multiplicative action of K on (b : H) × (G →+c[a, b] H) but we don't do this at the moment because we don't need this.

                @[simp]
                theorem AddConstMap.coe_smul {G : Type u_1} {H : Type u_2} {K : Type u_3} [Add G] [AddZeroClass H] {a : G} {b : H} [DistribSMul K H] (c : K) (f : AddConstMap G H a b) :
                (AddConstMap.smul c f) = c f
                def AddConstMap.smul {G : Type u_1} {H : Type u_2} {K : Type u_3} [Add G] [AddZeroClass H] {a : G} {b : H} [DistribSMul K H] (c : K) (f : AddConstMap G H a b) :
                AddConstMap G H a (c b)

                Pointwise scalar multiplication of f : G →+c[a, b] H as a map G →+c[a, c • b] H.

                Equations
                Instances For
                  @[simp]
                  theorem AddConstMap.coe_addLeftHom_apply {G : Type u_1} [AddMonoid G] {a : G} (c : Multiplicative G) :
                  (AddConstMap.addLeftHom c) = c id

                  The map that sends c to a translation by c as a monoid homomorphism from Multiplicative G to G →+c[a, a] G.

                  Equations
                  • AddConstMap.addLeftHom = { toFun := fun (c : Multiplicative G) => Multiplicative.toAdd c +ᵥ AddConstMap.id, map_one' := , map_mul' := }
                  Instances For
                    @[simp]
                    theorem AddConstMap.coe_conjNeg_apply {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] {a : G} {b : H} (f : AddConstMap G H a b) (x : G) :
                    (AddConstMap.conjNeg f) x = -f (-x)
                    def AddConstMap.conjNeg {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] {a : G} {b : H} :
                    AddConstMap G H a b AddConstMap G H a b

                    If f : G → H is an AddConstMap, then so is fun x ↦ -f (-x).

                    Equations
                    Instances For
                      @[simp]
                      theorem AddConstMap.conjNeg_symm {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] {a : G} {b : H} :
                      AddConstMap.conjNeg.symm = AddConstMap.conjNeg
                      def AddConstMap.mkFract {R : Type u_1} {G : Type u_2} [LinearOrderedRing R] [FloorRing R] [AddGroup G] (a : G) :
                      ((Set.Ico 0 1)G) AddConstMap R G 1 a

                      A map f : R →+c[1, a] G is defined by its values on Set.Ico 0 1.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For