Documentation

Mathlib.Algebra.AddConstMap.Equiv

Equivalences conjugating (· + a) to (· + b) #

In this file we define AddConstEquiv G H a b (notation: G ≃+c[a, b] H) to be the type of equivalences such that ∀ x, f (x + a) = f x + b.

We also define the corresponding typeclass and prove some basic properties.

structure AddConstEquiv (G : Type u_1) (H : Type u_2) [Add G] [Add H] (a : G) (b : H) extends Equiv :
Type (max u_1 u_2)

An equivalence between G and H conjugating (· + a) to (· + b).

  • toFun : GH
  • invFun : HG
  • left_inv : Function.LeftInverse self.invFun self.toFun
  • right_inv : Function.RightInverse self.invFun self.toFun
  • 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
    @[reducible]
    abbrev AddConstEquiv.toAddConstMap {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (self : AddConstEquiv G H a b) :
    AddConstMap G H a b

    Interpret an AddConstEquiv as an AddConstMap.

    Equations
    • self.toAddConstMap = { toFun := self.toFun, map_add_const' := }
    Instances For

      An equivalence between G and H conjugating (· + a) to (· + b).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem AddConstEquiv.toEquiv_injective {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} :
        Function.Injective AddConstEquiv.toEquiv
        instance AddConstEquiv.instEquivLike {G : Type u_4} {H : Type u_5} [Add G] [Add H] {a : G} {b : H} :
        EquivLike (AddConstEquiv G H a b) G H
        Equations
        • AddConstEquiv.instEquivLike = { coe := fun (f : AddConstEquiv G H a b) => f.toEquiv, inv := fun (f : AddConstEquiv G H a b) => f.symm, left_inv := , right_inv := , coe_injective' := }
        instance AddConstEquiv.instAddConstMapClass {G : Type u_4} {H : Type u_5} [Add G] [Add H] {a : G} {b : H} :
        Equations
        • =
        theorem AddConstEquiv.ext_iff {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {e₁ : AddConstEquiv G H a b} {e₂ : AddConstEquiv G H a b} :
        e₁ = e₂ ∀ (x : G), e₁ x = e₂ x
        theorem AddConstEquiv.ext {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {e₁ : AddConstEquiv G H a b} {e₂ : AddConstEquiv G H a b} (h : ∀ (x : G), e₁ x = e₂ x) :
        e₁ = e₂
        @[simp]
        theorem AddConstEquiv.toEquiv_inj {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {e₁ : AddConstEquiv G H a b} {e₂ : AddConstEquiv G H a b} :
        e₁.toEquiv = e₂.toEquiv e₁ = e₂
        @[simp]
        theorem AddConstEquiv.coe_toEquiv {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :
        e.toEquiv = e
        def AddConstEquiv.symm {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :

        Inverse map of an AddConstEquiv, as an AddConstEquiv.

        Equations
        • e.symm = { toEquiv := e.symm, map_add_const' := }
        Instances For
          def AddConstEquiv.Simps.symm_apply {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :
          HG

          A custom projection for simps.

          Equations
          Instances For
            @[simp]
            theorem AddConstEquiv.symm_symm {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :
            e.symm.symm = e
            @[simp]
            theorem AddConstEquiv.refl_apply {G : Type u_1} [Add G] (a : G) (a : G) :
            @[simp]
            theorem AddConstEquiv.refl_toEquiv {G : Type u_1} [Add G] (a : G) :
            def AddConstEquiv.refl {G : Type u_1} [Add G] (a : G) :

            The identity map as an AddConstEquiv.

            Equations
            Instances For
              @[simp]
              theorem AddConstEquiv.symm_refl {G : Type u_1} [Add G] (a : G) :
              @[simp]
              theorem AddConstEquiv.trans_toEquiv {G : Type u_1} {H : Type u_2} {K : Type u_3} [Add G] [Add H] [Add K] {a : G} {b : H} {c : K} (e₁ : AddConstEquiv G H a b) (e₂ : AddConstEquiv H K b c) :
              (e₁.trans e₂).toEquiv = e₁.trans e₂.toEquiv
              @[simp]
              theorem AddConstEquiv.trans_apply {G : Type u_1} {H : Type u_2} {K : Type u_3} [Add G] [Add H] [Add K] {a : G} {b : H} {c : K} (e₁ : AddConstEquiv G H a b) (e₂ : AddConstEquiv H K b c) :
              ∀ (a_1 : G), (e₁.trans e₂) a_1 = e₂ (e₁ a_1)
              def AddConstEquiv.trans {G : Type u_1} {H : Type u_2} {K : Type u_3} [Add G] [Add H] [Add K] {a : G} {b : H} {c : K} (e₁ : AddConstEquiv G H a b) (e₂ : AddConstEquiv H K b c) :

              Composition of AddConstEquivs, as an AddConstEquiv.

              Equations
              • e₁.trans e₂ = { toEquiv := e₁.trans e₂.toEquiv, map_add_const' := }
              Instances For
                @[simp]
                theorem AddConstEquiv.trans_refl {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :
                e.trans (AddConstEquiv.refl b) = e
                @[simp]
                theorem AddConstEquiv.refl_trans {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :
                (AddConstEquiv.refl a).trans e = e
                @[simp]
                theorem AddConstEquiv.self_trans_symm {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :
                e.trans e.symm = AddConstEquiv.refl a
                @[simp]
                theorem AddConstEquiv.symm_trans_self {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) :
                e.symm.trans e = AddConstEquiv.refl b
                instance AddConstEquiv.instOne {G : Type u_1} [Add G] {a : G} :
                One (AddConstEquiv G G a a)
                Equations
                instance AddConstEquiv.instMul {G : Type u_1} [Add G] {a : G} :
                Mul (AddConstEquiv G G a a)
                Equations
                • AddConstEquiv.instMul = { mul := fun (f g : AddConstEquiv G G a a) => g.trans f }
                instance AddConstEquiv.instInv {G : Type u_1} [Add G] {a : G} :
                Inv (AddConstEquiv G G a a)
                Equations
                • AddConstEquiv.instInv = { inv := AddConstEquiv.symm }
                instance AddConstEquiv.instDiv {G : Type u_1} [Add G] {a : G} :
                Div (AddConstEquiv G G a a)
                Equations
                instance AddConstEquiv.instPowNat {G : Type u_1} [Add G] {a : G} :
                Equations
                • AddConstEquiv.instPowNat = { pow := fun (e : AddConstEquiv G G a a) (n : ) => { toEquiv := e ^ n, map_add_const' := } }
                instance AddConstEquiv.instPowInt {G : Type u_1} [Add G] {a : G} :
                Equations
                • AddConstEquiv.instPowInt = { pow := fun (e : AddConstEquiv G G a a) (n : ) => { toEquiv := e ^ n, map_add_const' := } }
                instance AddConstEquiv.instGroup {G : Type u_1} [Add G] {a : G} :
                Equations
                @[simp]
                theorem AddConstEquiv.toPerm_apply {G : Type u_1} [Add G] {a : G} (self : AddConstEquiv G G a a) :
                AddConstEquiv.toPerm self = self.toEquiv
                def AddConstEquiv.toPerm {G : Type u_1} [Add G] {a : G} :

                Projection from G ≃+c[a, a] G to permutations G ≃ G, as a monoid homomorphism.

                Equations
                Instances For
                  @[simp]
                  theorem AddConstEquiv.toAddConstMapHom_apply {G : Type u_1} [Add G] {a : G} (self : AddConstEquiv G G a a) :
                  AddConstEquiv.toAddConstMapHom self = self.toAddConstMap
                  def AddConstEquiv.toAddConstMapHom {G : Type u_1} [Add G] {a : G} :

                  Projection from G ≃+c[a, a] G to G →+c[a, a] G, as a monoid homomorphism.

                  Equations
                  • AddConstEquiv.toAddConstMapHom = { toFun := AddConstEquiv.toAddConstMap, map_one' := , map_mul' := }
                  Instances For
                    @[simp]
                    theorem AddConstEquiv.coe_val_equivUnits_apply {G : Type u_1} [Add G] {a : G} (a : AddConstEquiv G G a✝ a✝) :
                    ∀ (a_1 : G), (AddConstEquiv.equivUnits a) a_1 = a a_1
                    @[simp]
                    theorem AddConstEquiv.equivUnits_symm_apply_symm_apply {G : Type u_1} [Add G] {a : G} (u : (AddConstMap G G a a)ˣ) :
                    (AddConstEquiv.equivUnits.symm u).symm = u⁻¹
                    @[simp]
                    theorem AddConstEquiv.coe_val_inv_equivUnits_apply {G : Type u_1} [Add G] {a : G} (a : AddConstEquiv G G a✝ a✝) :
                    ∀ (a_1 : G), (AddConstEquiv.equivUnits a)⁻¹ a_1 = a⁻¹ a_1
                    @[simp]
                    theorem AddConstEquiv.equivUnits_symm_apply_apply {G : Type u_1} [Add G] {a : G} (u : (AddConstMap G G a a)ˣ) :
                    (AddConstEquiv.equivUnits.symm u) = u
                    def AddConstEquiv.equivUnits {G : Type u_1} [Add G] {a : G} :
                    AddConstEquiv G G a a ≃* (AddConstMap G G a a)ˣ

                    Group equivalence between G ≃+c[a, a] G and the units of G →+c[a, a] G.

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