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 G ≃ H, AddConstMap G H a b : Type (max u_1 u_2)

An equivalence between G and H conjugating (· + a) to (· + b), denoted as G ≃+c[a, b] H.

• toFun : G → H
• invFun : H → G
• 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

def AddConstMap.«term_≃+c[_,_]_» : Lean.TrailingParserDescr

An equivalence between G and H conjugating (· + a) to (· + b), denoted as G ≃+c[a, b] H.

theorem AddConstEquiv.toEquiv_injective {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} : Function.Injective toEquiv

@[implicit_reducible]

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

instance AddConstEquiv.instAddConstMapClass {G : Type u_4} {H : Type u_5} [Add G] [Add H] {a : G} {b : H} : AddConstMapClass (AddConstEquiv G H a b) G H a b

theorem AddConstEquiv.ext {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {e₁ e₂ : AddConstEquiv G H a b} (h : ∀ (x : G), e₁ x = e₂ x) : e₁ = e₂

theorem AddConstEquiv.ext_iff {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {e₁ e₂ : AddConstEquiv G H a b} : e₁ = e₂ ↔ ∀ (x : G), e₁ x = e₂ x

@[simp]

theorem AddConstEquiv.toEquiv_inj {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} {e₁ 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) : AddConstEquiv H G b a

Inverse map of an AddConstEquiv, as an AddConstEquiv.

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) : H → G

A custom projection for simps.

@[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

def AddConstEquiv.refl {G : Type u_1} [Add G] (a : G) : AddConstEquiv G G a a

The identity map as an AddConstEquiv.

@[simp]

theorem AddConstEquiv.refl_apply {G : Type u_1} [Add G] (a a✝ : G) : (refl a) a✝ = a✝

@[simp]

theorem AddConstEquiv.refl_toEquiv {G : Type u_1} [Add G] (a : G) : (refl a).toEquiv = Equiv.refl G

@[simp]

theorem AddConstEquiv.symm_refl {G : Type u_1} [Add G] (a : G) : (refl a).symm = refl a

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) : AddConstEquiv G K a c

Composition of AddConstEquivs, as an AddConstEquiv.

@[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✝ : G) : (e₁.trans e₂) a✝ = e₂ (e₁ a✝)

@[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 (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) : (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 = 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 = refl b

@[simp]

theorem AddConstEquiv.coe_symm_toEquiv {G : Type u_1} {H : Type u_2} [Add G] [Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) : ⇑e.symm = ⇑e.symm

@[simp]

theorem AddConstEquiv.toEquiv_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.toEquiv = e.symm

@[simp]

theorem AddConstEquiv.toEquiv_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) : (e₁.trans e₂).toEquiv = e₁.trans e₂.toEquiv

@[implicit_reducible]

instance AddConstEquiv.instOne {G : Type u_1} [Add G] {a : G} : One (AddConstEquiv G G a a)

@[implicit_reducible]

instance AddConstEquiv.instMul {G : Type u_1} [Add G] {a : G} : Mul (AddConstEquiv G G a a)

@[implicit_reducible]

instance AddConstEquiv.instInv {G : Type u_1} [Add G] {a : G} : Inv (AddConstEquiv G G a a)

@[implicit_reducible]

instance AddConstEquiv.instDiv {G : Type u_1} [Add G] {a : G} : Div (AddConstEquiv G G a a)

@[implicit_reducible]

instance AddConstEquiv.instPowNat {G : Type u_1} [Add G] {a : G} : Pow (AddConstEquiv G G a a) ℕ

@[implicit_reducible]

instance AddConstEquiv.instPowInt {G : Type u_1} [Add G] {a : G} : Pow (AddConstEquiv G G a a) ℤ

@[implicit_reducible]

instance AddConstEquiv.instGroup {G : Type u_1} [Add G] {a : G} : Group (AddConstEquiv G G a a)

def AddConstEquiv.toPerm {G : Type u_1} [Add G] {a : G} : AddConstEquiv G G a a →* Equiv.Perm G

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

@[simp]

theorem AddConstEquiv.toPerm_apply {G : Type u_1} [Add G] {a : G} (self : AddConstEquiv G G a a) : toPerm self = self.toEquiv

def AddConstEquiv.toAddConstMapHom {G : Type u_1} [Add G] {a : G} : AddConstEquiv G G a a →* AddConstMap G G a a

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

@[simp]

theorem AddConstEquiv.toAddConstMapHom_apply {G : Type u_1} [Add G] {a : G} (self : AddConstEquiv G G a a) : toAddConstMapHom self = self.toAddConstMap

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.

@[simp]

theorem AddConstEquiv.coe_val_inv_equivUnits_apply {G : Type u_1} [Add G] {a : G} (a✝ : AddConstEquiv G G a a) (a✝¹ : G) : ↑(equivUnits a✝)⁻¹ a✝¹ = a✝⁻¹ a✝¹

@[simp]

theorem AddConstEquiv.equivUnits_symm_apply_apply {G : Type u_1} [Add G] {a : G} (u : (AddConstMap G G a a)ˣ) : ⇑(equivUnits.symm u) = ⇑↑u

@[simp]

theorem AddConstEquiv.coe_val_equivUnits_apply {G : Type u_1} [Add G] {a : G} (a✝ : AddConstEquiv G G a a) (a✝¹ : G) : ↑(equivUnits a✝) a✝¹ = a✝ a✝¹

@[simp]

theorem AddConstEquiv.equivUnits_symm_apply_symm_apply {G : Type u_1} [Add G] {a : G} (u : (AddConstMap G G a a)ˣ) : ⇑(equivUnits.symm u).symm = ⇑↑u⁻¹