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

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

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} :
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
instance AddConstEquiv.instAddConstMapClass {G : Type u_4} {H : Type u_5} [Add G] [Add H] {a : G} {b : H} :
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) :

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) :
HG

A custom projection for simps.

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

The identity map as an AddConstEquiv.

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

Composition of AddConstEquivs, as an AddConstEquiv.

Equations
@[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) :
@[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) :
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
instance AddConstEquiv.instInv {G : Type u_1} [Add G] {a : G} :
Inv (AddConstEquiv G G a a)
Equations
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
instance AddConstEquiv.instPowInt {G : Type u_1} [Add G] {a : G} :
Equations
instance AddConstEquiv.instGroup {G : Type u_1} [Add G] {a : G} :
Equations
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
@[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} :

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

Equations
@[simp]
theorem AddConstEquiv.toAddConstMapHom_apply {G : Type u_1} [Add G] {a : G} (self : AddConstEquiv G G a a) :
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) :
(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⁻¹
@[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