Documentation

Mathlib.Algebra.Group.Units.Equiv

Multiplicative and additive equivalence acting on units. #

theorem toAddUnits.proof_3 {G : Type u_1} [AddGroup G] :

∀ (x x_1 : G), { toFun := fun (x : G) => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits G) => ↑x, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : G) => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits G) => ↑x, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun (x : G) => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits G) => ↑x, left_inv := ⋯, right_inv := ⋯ }.toFun x_1

def toAddUnits {G : Type u_10} [AddGroup G] :

G ≃+ AddUnits G

An additive group is isomorphic to its group of additive units

Equations

toAddUnits = { toFun := fun (x : G) => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits G) => ↑x, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

theorem toAddUnits.proof_2 {G : Type u_1} [AddGroup G] :

∀ (x : AddUnits G), (fun (x : G) => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }) ((fun (x : AddUnits G) => ↑x) x) = x

theorem toAddUnits.proof_1 {G : Type u_1} [AddGroup G] :

∀ (x : G), (fun (x : AddUnits G) => ↑x) ((fun (x : G) => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }) x) = (fun (x : AddUnits G) => ↑x) ((fun (x : G) => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }) x)

@[simp]

theorem toUnits_symm_apply {G : Type u_10} [Group G] (x : Gˣ) :

toUnits.symm x = ↑x

@[simp]

theorem toAddUnits_symm_apply {G : Type u_10} [AddGroup G] (x : AddUnits G) :

toAddUnits.symm x = ↑x

@[simp]

theorem val_toAddUnits_apply {G : Type u_10} [AddGroup G] (x : G) :

↑(toAddUnits x) = x

@[simp]

theorem val_toUnits_apply {G : Type u_10} [Group G] (x : G) :

↑(toUnits x) = x

def toUnits {G : Type u_10} [Group G] :

A group is isomorphic to its group of units.

Equations

toUnits = { toFun := fun (x : G) => { val := x, inv := x⁻¹, val_inv := ⋯, inv_val := ⋯ }, invFun := fun (x : Gˣ) => ↑x, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

@[simp]

theorem toAddUnits_val_apply {G : Type u_12} [AddGroup G] (x : AddUnits G) :

toAddUnits ↑x = x

@[simp]

theorem toUnits_val_apply {G : Type u_12} [Group G] (x : Gˣ) :

toUnits ↑x = x

def Units.mapEquiv {M : Type u_6} {N : Type u_7} [Monoid M] [Monoid N] (h : M ≃* N) :

A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.

Equations

Units.mapEquiv h = let __src := Units.map h.toMonoidHom; { toFun := (↑__src).toFun, invFun := ⇑(Units.map h.symm.toMonoidHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

@[simp]

theorem Units.mapEquiv_symm {M : Type u_6} {N : Type u_7} [Monoid M] [Monoid N] (h : M ≃* N) :

(Units.mapEquiv h).symm = Units.mapEquiv h.symm

@[simp]

theorem Units.coe_mapEquiv {M : Type u_6} {N : Type u_7} [Monoid M] [Monoid N] (h : M ≃* N) (x : Mˣ) :

↑((Units.mapEquiv h) x) = h ↑x

def AddUnits.addLeft {M : Type u_6} [AddMonoid M] (u : AddUnits M) :

Left addition of an additive unit is a permutation of the underlying type.

Equations

u.addLeft = { toFun := fun (x : M) => ↑u + x, invFun := fun (x : M) => ↑(-u) + x, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem Units.mulLeft_apply {M : Type u_6} [Monoid M] (u : Mˣ) :

⇑u.mulLeft = fun (x : M) => ↑u * x

@[simp]

theorem AddUnits.addLeft_apply {M : Type u_6} [AddMonoid M] (u : AddUnits M) :

⇑u.addLeft = fun (x : M) => ↑u + x

def Units.mulLeft {M : Type u_6} [Monoid M] (u : Mˣ) :

Left multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

u.mulLeft = { toFun := fun (x : M) => ↑u * x, invFun := fun (x : M) => ↑u⁻¹ * x, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem AddUnits.addLeft_symm {M : Type u_6} [AddMonoid M] (u : AddUnits M) :

Equiv.symm u.addLeft = (-u).addLeft

@[simp]

theorem Units.mulLeft_symm {M : Type u_6} [Monoid M] (u : Mˣ) :

Equiv.symm u.mulLeft = u⁻¹.mulLeft

theorem AddUnits.addLeft_bijective {M : Type u_6} [AddMonoid M] (a : AddUnits M) :

Function.Bijective fun (x : M) => ↑a + x

theorem Units.mulLeft_bijective {M : Type u_6} [Monoid M] (a : Mˣ) :

Function.Bijective fun (x : M) => ↑a * x

def AddUnits.addRight {M : Type u_6} [AddMonoid M] (u : AddUnits M) :

Right addition of an additive unit is a permutation of the underlying type.

Equations

u.addRight = { toFun := fun (x : M) => x + ↑u, invFun := fun (x : M) => x + ↑(-u), left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem AddUnits.addRight_apply {M : Type u_6} [AddMonoid M] (u : AddUnits M) :

⇑u.addRight = fun (x : M) => x + ↑u

@[simp]

theorem Units.mulRight_apply {M : Type u_6} [Monoid M] (u : Mˣ) :

⇑u.mulRight = fun (x : M) => x * ↑u

def Units.mulRight {M : Type u_6} [Monoid M] (u : Mˣ) :

Right multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

u.mulRight = { toFun := fun (x : M) => x * ↑u, invFun := fun (x : M) => x * ↑u⁻¹, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem AddUnits.addRight_symm {M : Type u_6} [AddMonoid M] (u : AddUnits M) :

Equiv.symm u.addRight = (-u).addRight

@[simp]

theorem Units.mulRight_symm {M : Type u_6} [Monoid M] (u : Mˣ) :

Equiv.symm u.mulRight = u⁻¹.mulRight

theorem AddUnits.addRight_bijective {M : Type u_6} [AddMonoid M] (a : AddUnits M) :

Function.Bijective fun (x : M) => x + ↑a

theorem Units.mulRight_bijective {M : Type u_6} [Monoid M] (a : Mˣ) :

Function.Bijective fun (x : M) => x * ↑a

def Equiv.addLeft {G : Type u_10} [AddGroup G] (a : G) :

Left addition in an AddGroup is a permutation of the underlying type.

Equations

Equiv.addLeft a = (toAddUnits a).addLeft

Instances For

def Equiv.mulLeft {G : Type u_10} [Group G] (a : G) :

Left multiplication in a Group is a permutation of the underlying type.

Equations

Equiv.mulLeft a = (toUnits a).mulLeft

Instances For

@[simp]

theorem Equiv.coe_addLeft {G : Type u_10} [AddGroup G] (a : G) :

⇑(Equiv.addLeft a) = fun (x : G) => a + x

@[simp]

theorem Equiv.coe_mulLeft {G : Type u_10} [Group G] (a : G) :

⇑(Equiv.mulLeft a) = fun (x : G) => a * x

theorem Equiv.addLeft_symm_apply {G : Type u_10} [AddGroup G] (a : G) :

⇑(Equiv.symm (Equiv.addLeft a)) = fun (x : G) => -a + x

Extra simp lemma that dsimp can use. simp will never use this.

@[simp]

theorem Equiv.mulLeft_symm_apply {G : Type u_10} [Group G] (a : G) :

⇑(Equiv.symm (Equiv.mulLeft a)) = fun (x : G) => a⁻¹ * x

Extra simp lemma that dsimp can use. simp will never use this.

@[simp]

theorem Equiv.addLeft_symm {G : Type u_10} [AddGroup G] (a : G) :

Equiv.symm (Equiv.addLeft a) = Equiv.addLeft (-a)

@[simp]

theorem Equiv.mulLeft_symm {G : Type u_10} [Group G] (a : G) :

Equiv.symm (Equiv.mulLeft a) = Equiv.mulLeft a⁻¹

theorem AddGroup.addLeft_bijective {G : Type u_10} [AddGroup G] (a : G) :

Function.Bijective fun (x : G) => a + x

theorem Group.mulLeft_bijective {G : Type u_10} [Group G] (a : G) :

Function.Bijective fun (x : G) => a * x

def Equiv.addRight {G : Type u_10} [AddGroup G] (a : G) :

Right addition in an AddGroup is a permutation of the underlying type.

Equations

Equiv.addRight a = (toAddUnits a).addRight

Instances For

def Equiv.mulRight {G : Type u_10} [Group G] (a : G) :

Right multiplication in a Group is a permutation of the underlying type.

Equations

Equiv.mulRight a = (toUnits a).mulRight

Instances For

@[simp]

theorem Equiv.coe_addRight {G : Type u_10} [AddGroup G] (a : G) :

⇑(Equiv.addRight a) = fun (x : G) => x + a

@[simp]

theorem Equiv.coe_mulRight {G : Type u_10} [Group G] (a : G) :

⇑(Equiv.mulRight a) = fun (x : G) => x * a

@[simp]

theorem Equiv.addRight_symm {G : Type u_10} [AddGroup G] (a : G) :

Equiv.symm (Equiv.addRight a) = Equiv.addRight (-a)

@[simp]

theorem Equiv.mulRight_symm {G : Type u_10} [Group G] (a : G) :

Equiv.symm (Equiv.mulRight a) = Equiv.mulRight a⁻¹

theorem Equiv.addRight_symm_apply {G : Type u_10} [AddGroup G] (a : G) :

⇑(Equiv.symm (Equiv.addRight a)) = fun (x : G) => x + -a

Extra simp lemma that dsimp can use. simp will never use this.

@[simp]

theorem Equiv.mulRight_symm_apply {G : Type u_10} [Group G] (a : G) :

⇑(Equiv.symm (Equiv.mulRight a)) = fun (x : G) => x * a⁻¹

Extra simp lemma that dsimp can use. simp will never use this.

theorem AddGroup.addRight_bijective {G : Type u_10} [AddGroup G] (a : G) :

Function.Bijective fun (x : G) => x + a

theorem Group.mulRight_bijective {G : Type u_10} [Group G] (a : G) :

Function.Bijective fun (x : G) => x * a

theorem Equiv.subLeft.proof_2 {G : Type u_1} [AddGroup G] (a : G) (b : G) :

a - (-b + a) = b

theorem Equiv.subLeft.proof_1 {G : Type u_1} [AddGroup G] (a : G) (b : G) :

-(a - b) + a = b

def Equiv.subLeft {G : Type u_10} [AddGroup G] (a : G) :

G ≃ G

A version of Equiv.addLeft a (-b) that is defeq to a - b.

Equations

Equiv.subLeft a = { toFun := fun (b : G) => a - b, invFun := fun (b : G) => -b + a, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem Equiv.divLeft_symm_apply {G : Type u_10} [Group G] (a : G) (b : G) :

(Equiv.divLeft a).symm b = b⁻¹ * a

@[simp]

theorem Equiv.subLeft_apply {G : Type u_10} [AddGroup G] (a : G) (b : G) :

(Equiv.subLeft a) b = a - b

@[simp]

theorem Equiv.subLeft_symm_apply {G : Type u_10} [AddGroup G] (a : G) (b : G) :

(Equiv.subLeft a).symm b = -b + a

@[simp]

theorem Equiv.divLeft_apply {G : Type u_10} [Group G] (a : G) (b : G) :

(Equiv.divLeft a) b = a / b

def Equiv.divLeft {G : Type u_10} [Group G] (a : G) :

G ≃ G

A version of Equiv.mulLeft a b⁻¹ that is defeq to a / b.

Equations

Equiv.divLeft a = { toFun := fun (b : G) => a / b, invFun := fun (b : G) => b⁻¹ * a, left_inv := ⋯, right_inv := ⋯ }

Instances For

theorem Equiv.subLeft_eq_neg_trans_addLeft {G : Type u_10} [AddGroup G] (a : G) :

Equiv.subLeft a = Equiv.trans (Equiv.neg G) (Equiv.addLeft a)

theorem Equiv.divLeft_eq_inv_trans_mulLeft {G : Type u_10} [Group G] (a : G) :

Equiv.divLeft a = Equiv.trans (Equiv.inv G) (Equiv.mulLeft a)

theorem Equiv.subRight.proof_1 {G : Type u_1} [AddGroup G] (a : G) (b : G) :

b - a + a = b

def Equiv.subRight {G : Type u_10} [AddGroup G] (a : G) :

G ≃ G

A version of Equiv.addRight (-a) b that is defeq to b - a.

Equations

Equiv.subRight a = { toFun := fun (b : G) => b - a, invFun := fun (b : G) => b + a, left_inv := ⋯, right_inv := ⋯ }

Instances For

theorem Equiv.subRight.proof_2 {G : Type u_1} [AddGroup G] (a : G) (b : G) :

b + a - a = b

@[simp]

theorem Equiv.divRight_symm_apply {G : Type u_10} [Group G] (a : G) (b : G) :

(Equiv.divRight a).symm b = b * a

@[simp]

theorem Equiv.subRight_symm_apply {G : Type u_10} [AddGroup G] (a : G) (b : G) :

(Equiv.subRight a).symm b = b + a

@[simp]

theorem Equiv.subRight_apply {G : Type u_10} [AddGroup G] (a : G) (b : G) :

(Equiv.subRight a) b = b - a

@[simp]

theorem Equiv.divRight_apply {G : Type u_10} [Group G] (a : G) (b : G) :

(Equiv.divRight a) b = b / a

def Equiv.divRight {G : Type u_10} [Group G] (a : G) :

G ≃ G

A version of Equiv.mulRight a⁻¹ b that is defeq to b / a.

Equations

Equiv.divRight a = { toFun := fun (b : G) => b / a, invFun := fun (b : G) => b * a, left_inv := ⋯, right_inv := ⋯ }

Instances For

theorem Equiv.subRight_eq_addRight_neg {G : Type u_10} [AddGroup G] (a : G) :

Equiv.subRight a = Equiv.addRight (-a)

theorem Equiv.divRight_eq_mulRight_inv {G : Type u_10} [Group G] (a : G) :

Equiv.divRight a = Equiv.mulRight a⁻¹

@[simp]

theorem val_inv_unitsEquivProdSubtype_symm_apply (α : Type u_2) [Monoid α] (p : { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }) :

↑((unitsEquivProdSubtype α).symm p)⁻¹ = (↑p).2

@[simp]

theorem val_unitsEquivProdSubtype_symm_apply (α : Type u_2) [Monoid α] (p : { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }) :

↑((unitsEquivProdSubtype α).symm p) = (↑p).1

@[simp]

theorem unitsEquivProdSubtype_apply_coe (α : Type u_2) [Monoid α] (u : αˣ) :

↑((unitsEquivProdSubtype α) u) = (↑u, ↑u⁻¹)

def unitsEquivProdSubtype (α : Type u_2) [Monoid α] :

αˣ ≃ { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }

The αˣ type is equivalent to a subtype of α × α.

Equations

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

Instances For

def AddEquiv.neg (G : Type u_12) [SubtractionCommMonoid G] :

G ≃+ G

When the AddGroup is commutative, Equiv.neg is an AddEquiv.

Equations

AddEquiv.neg G = let __src := Equiv.neg G; { toFun := Neg.neg, invFun := Neg.neg, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem MulEquiv.inv_apply (G : Type u_12) [DivisionCommMonoid G] :

∀ (a : G), (MulEquiv.inv G) a = a⁻¹

@[simp]

theorem AddEquiv.neg_apply (G : Type u_12) [SubtractionCommMonoid G] :

∀ (a : G), (AddEquiv.neg G) a = -a

def MulEquiv.inv (G : Type u_12) [DivisionCommMonoid G] :

G ≃* G

In a DivisionCommMonoid, Equiv.inv is a MulEquiv. There is a variant of this MulEquiv.inv' G : G ≃* Gᵐᵒᵖ for the non-commutative case.

Equations

MulEquiv.inv G = let __src := Equiv.inv G; { toFun := Inv.inv, invFun := Inv.inv, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

@[simp]

theorem AddEquiv.neg_symm (G : Type u_12) [SubtractionCommMonoid G] :

(AddEquiv.neg G).symm = AddEquiv.neg G

@[simp]

theorem MulEquiv.inv_symm (G : Type u_12) [DivisionCommMonoid G] :

(MulEquiv.inv G).symm = MulEquiv.inv G

theorem AddEquiv.map_isAddUnit_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [AddMonoid M] [AddMonoid N] [EquivLike F M N] [AddMonoidHomClass F M N] (f : F) {m : M} :

IsAddUnit (f m) ↔ IsAddUnit m

theorem MulEquiv.map_isUnit_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [Monoid M] [Monoid N] [EquivLike F M N] [MonoidHomClass F M N] (f : F) {m : M} :

IsUnit (f m) ↔ IsUnit m