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.

source

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 : 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
An AddConstMap satisfies f (x + a) = f x + b. Use map_add_const instead.

Instances For

source

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

source

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.

Instances For

source

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

Function.Injective AddConstEquiv.toEquiv

source

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' := ⋯ }

source

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

⋯ = ⋯

source

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

source

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₂

source

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

source

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

source

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' := ⋯ }

Instances For

source

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

Instances For

source

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

source

@[simp]

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

(AddConstEquiv.refl a✝) a = a

source

@[simp]

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

(AddConstEquiv.refl a).toEquiv = Equiv.refl G

source

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' := ⋯ }

Instances For

source

@[simp]

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

(AddConstEquiv.refl a).symm = AddConstEquiv.refl a

source

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

source

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

source

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' := ⋯ }

Instances For

source

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

source

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

source

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

source

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

source

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

One (AddConstEquiv G G a a)

Equations

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

source

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 }

source

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

Inv (AddConstEquiv G G a a)

Equations

AddConstEquiv.instInv = { inv := AddConstEquiv.symm }

source

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⁻¹ }

source

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' := ⋯ } }

source

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' := ⋯ } }

source

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

@[simp]

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

AddConstEquiv.toPerm self = self.toEquiv

source

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 ⋯

Instances For

source

@[simp]

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

AddConstEquiv.toAddConstMapHom self = self.toAddConstMap

source

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' := ⋯ }

Instances For

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.Algebra.AddConstMap.Equiv

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

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

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