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).

• 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).

Equations

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

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} : AddConstMapClass (AddConstEquiv G H a b) G H a b

Equations

• ⋯ = ⋯

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₂

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

Equations

• e.symm = { toEquiv := e.symm, map_add_const' := ⋯ }

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.

Equations

• AddConstEquiv.Simps.symm_apply e = ⇑e.symm

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

Equations

• AddConstEquiv.refl a = { toEquiv := Equiv.refl G, map_add_const' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem AddConstEquiv.symm_refl {G : Type u_1} [Add G] (a : G) : (AddConstEquiv.refl a).symm = AddConstEquiv.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.

Equations

• e₁.trans e₂ = { toEquiv := e₁.trans e₂.toEquiv, map_add_const' := ⋯ }

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

• AddConstEquiv.instOne = { one := AddConstEquiv.refl a }

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

• AddConstEquiv.instDiv = { div := fun (f g : AddConstEquiv G G a a) => f * g⁻¹ }

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

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} : Pow (AddConstEquiv G G a a) ℤ

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} : Group (AddConstEquiv G G a a)

Equations

• AddConstEquiv.instGroup = Function.Injective.group AddConstEquiv.toEquiv ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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.

Equations

• AddConstEquiv.toPerm = MonoidHom.mk' AddConstEquiv.toEquiv ⋯

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

Equations

• AddConstEquiv.toAddConstMapHom = { toFun := AddConstEquiv.toAddConstMap, map_one' := ⋯, map_mul' := ⋯ }

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

@[simp]

theorem AddConstEquiv.coe_val_equivUnits_apply {G : Type u_1} [Add G] {a : G} (a✝ : AddConstEquiv G G a a) (a✝¹ : G) : ↑(AddConstEquiv.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)ˣ) : ⇑(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✝¹ : G) : ↑(AddConstEquiv.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)ˣ) : ⇑(AddConstEquiv.equivUnits.symm u) = ⇑↑u