doc-next-gen

Mathlib.Algebra.Group.Ext

Module docstring

{"# Extensionality lemmas for monoid and group structures

In this file we prove extensionality lemmas for Monoid and higher algebraic structures with one binary operation. Extensionality lemmas for structures that are lower in the hierarchy can be found in Algebra.Group.Defs.

Implementation details

To get equality of npow etc, we define a monoid homomorphism between two monoid structures on the same type, then apply lemmas like MonoidHom.map_div, MonoidHom.map_pow etc.

To refer to the * operator of a particular instance i, we use (letI := i; HMul.hMul : M → M → M) instead of i.mul (which elaborates to Mul.mul), as the former uses HMul.hMul which is the canonical spelling.

Tags

monoid, group, extensionality "}

Monoid.ext theorem
{M : Type u} ⦃m₁ m₂ : Monoid M⦄ (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
    m₁ = m₂ := by
  have : m₁.toMulOneClass = m₂.toMulOneClass := MulOneClass.ext h_mul
  have h₁ : m₁.one = m₂.one := congr_arg (·.one) this
  let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)
  have : m₁.npow = m₂.npow := by
    ext n x
    exact @MonoidHom.map_pow M M m₁ m₂ f x n
  rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩
  rcases m₂ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩
  congr
Extensionality of Monoid Structures: Equality via Multiplication
Informal description
Let $M$ be a type, and let $m_1$ and $m_2$ be two monoid structures on $M$. If the multiplication operations of $m_1$ and $m_2$ are equal (i.e., $a \cdot_{m_1} b = a \cdot_{m_2} b$ for all $a, b \in M$), then $m_1$ and $m_2$ are equal as monoid structures.
CommMonoid.toMonoid_injective theorem
{M : Type u} : Function.Injective (@CommMonoid.toMonoid M)
Full source 
@[to_additive]
theorem CommMonoid.toMonoid_injective {M : Type u} :
    Function.Injective (@CommMonoid.toMonoid M) := by
  rintro ⟨⟩ ⟨⟩ h
  congr
Injectivity of the Underlying Monoid Structure of a Commutative Monoid
Informal description
For any type $M$, the function that maps a commutative monoid structure on $M$ to its underlying monoid structure is injective. In other words, if two commutative monoid structures on $M$ have the same underlying monoid structure, then they must be equal.
CommMonoid.ext theorem
{M : Type*} ⦃m₁ m₂ : CommMonoid M⦄ (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem CommMonoid.ext {M : Type*} ⦃m₁ m₂ : CommMonoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂ :=
  CommMonoid.toMonoid_injective <| Monoid.ext h_mul
Extensionality of Commutative Monoid Structures via Multiplication
Informal description
Let $M$ be a type, and let $m_1$ and $m_2$ be two commutative monoid structures on $M$. If the multiplication operations of $m_1$ and $m_2$ are equal (i.e., $a \cdot_{m_1} b = a \cdot_{m_2} b$ for all $a, b \in M$), then $m_1$ and $m_2$ are equal as commutative monoid structures.
LeftCancelMonoid.toMonoid_injective theorem
{M : Type u} : Function.Injective (@LeftCancelMonoid.toMonoid M)
Full source 
@[to_additive]
theorem LeftCancelMonoid.toMonoid_injective {M : Type u} :
    Function.Injective (@LeftCancelMonoid.toMonoid M) := by
  rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h
  congr <;> injection h
Injectivity of the Underlying Monoid Structure of a Left-Cancellative Monoid
Informal description
For any type $M$, the function that maps a left-cancellative monoid structure on $M$ to its underlying monoid structure is injective. In other words, if two left-cancellative monoid structures on $M$ have the same underlying monoid structure, then they must be equal.
LeftCancelMonoid.ext theorem
{M : Type u} ⦃m₁ m₂ : LeftCancelMonoid M⦄ (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem LeftCancelMonoid.ext {M : Type u} ⦃m₁ m₂ : LeftCancelMonoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
    m₁ = m₂ :=
  LeftCancelMonoid.toMonoid_injective <| Monoid.ext h_mul
Extensionality of Left-Cancellative Monoid Structures via Multiplication
Informal description
Let $M$ be a type, and let $m_1$ and $m_2$ be two left-cancellative monoid structures on $M$. If the multiplication operations of $m_1$ and $m_2$ are equal (i.e., $a \cdot_{m_1} b = a \cdot_{m_2} b$ for all $a, b \in M$), then $m_1$ and $m_2$ are equal as left-cancellative monoid structures.
RightCancelMonoid.toMonoid_injective theorem
{M : Type u} : Function.Injective (@RightCancelMonoid.toMonoid M)
Full source 
@[to_additive]
theorem RightCancelMonoid.toMonoid_injective {M : Type u} :
    Function.Injective (@RightCancelMonoid.toMonoid M) := by
  rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h
  congr <;> injection h
Injectivity of the Right-Cancellative Monoid to Monoid Structure Map
Informal description
The function that maps a right-cancellative monoid structure on a type $M$ to its underlying monoid structure is injective. That is, if two right-cancellative monoid structures on $M$ induce the same monoid structure, then the two right-cancellative monoid structures must be equal.
RightCancelMonoid.ext theorem
{M : Type u} ⦃m₁ m₂ : RightCancelMonoid M⦄ (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem RightCancelMonoid.ext {M : Type u} ⦃m₁ m₂ : RightCancelMonoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))  :
    m₁ = m₂ :=
  RightCancelMonoid.toMonoid_injective <| Monoid.ext h_mul
Extensionality of Right-Cancellative Monoid Structures via Multiplication
Informal description
Let $M$ be a type, and let $m_1$ and $m_2$ be two right-cancellative monoid structures on $M$. If the multiplication operations of $m_1$ and $m_2$ are equal (i.e., $a \cdot_{m_1} b = a \cdot_{m_2} b$ for all $a, b \in M$), then $m_1$ and $m_2$ are equal as right-cancellative monoid structures.
CancelMonoid.toLeftCancelMonoid_injective theorem
{M : Type u} : Function.Injective (@CancelMonoid.toLeftCancelMonoid M)
Full source 
@[to_additive]
theorem CancelMonoid.toLeftCancelMonoid_injective {M : Type u} :
    Function.Injective (@CancelMonoid.toLeftCancelMonoid M) := by
  rintro ⟨⟩ ⟨⟩ h
  congr
Injectivity of the Cancellative Monoid to Left-Cancellative Monoid Structure Map
Informal description
The function that maps a cancellative monoid structure on a type $M$ to its underlying left-cancellative monoid structure is injective. That is, if two cancellative monoid structures on $M$ induce the same left-cancellative monoid structure, then the two cancellative monoid structures must be equal.
CancelMonoid.ext theorem
{M : Type*} ⦃m₁ m₂ : CancelMonoid M⦄ (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem CancelMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelMonoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
    m₁ = m₂ :=
  CancelMonoid.toLeftCancelMonoid_injective <| LeftCancelMonoid.ext h_mul
Extensionality of Cancellative Monoid Structures via Multiplication
Informal description
Let $M$ be a type, and let $m_1$ and $m_2$ be two cancellative monoid structures on $M$. If the multiplication operations of $m_1$ and $m_2$ are equal (i.e., $a \cdot_{m_1} b = a \cdot_{m_2} b$ for all $a, b \in M$), then $m_1$ and $m_2$ are equal as cancellative monoid structures.
CancelCommMonoid.toCommMonoid_injective theorem
{M : Type u} : Function.Injective (@CancelCommMonoid.toCommMonoid M)
Full source 
@[to_additive]
theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} :
    Function.Injective (@CancelCommMonoid.toCommMonoid M) := by
  rintro @⟨@⟨@⟨⟩⟩⟩ @⟨@⟨@⟨⟩⟩⟩ h
  congr <;> {
    injection h with h'
    injection h' }
Injectivity of Cancellative Commutative Monoid to Commutative Monoid Structure Map
Informal description
The function that maps a cancellative commutative monoid structure on a type $M$ to its underlying commutative monoid structure is injective. That is, if two cancellative commutative monoid structures on $M$ induce the same commutative monoid structure, then the two cancellative commutative monoid structures must be equal.
CancelCommMonoid.ext theorem
{M : Type*} ⦃m₁ m₂ : CancelCommMonoid M⦄ (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem CancelCommMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelCommMonoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
    m₁ = m₂ :=
  CancelCommMonoid.toCommMonoid_injective <| CommMonoid.ext h_mul
Extensionality of Cancellative Commutative Monoid Structures via Multiplication
Informal description
Let $M$ be a type, and let $m_1$ and $m_2$ be two cancellative commutative monoid structures on $M$. If the multiplication operations of $m_1$ and $m_2$ are equal (i.e., $a \cdot_{m_1} b = a \cdot_{m_2} b$ for all $a, b \in M$), then $m_1$ and $m_2$ are equal as cancellative commutative monoid structures.
DivInvMonoid.ext theorem
{M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄ (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) (h_inv : (letI := m₁; Inv.inv : M → M) = (letI := m₂; Inv.inv : M → M)) : m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem DivInvMonoid.ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))
    (h_inv : (letI := m₁; Inv.inv : M → M) = (letI := m₂; Inv.inv : M → M)) : m₁ = m₂ := by
  have h_mon := Monoid.ext h_mul
  have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon
  let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)
  have : m₁.npow = m₂.npow := congr_arg (·.npow) h_mon
  have : m₁.zpow = m₂.zpow := by
    ext m x
    exact @MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m
  have : m₁.div = m₂.div := by
    ext a b
    exact @map_div' _ _
      (F := @MonoidHom _ _ (_) _) _ (id _) _ inferInstance f (congr_fun h_inv) a b
  rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩⟩
  rcases m₂ with @⟨_, ⟨_⟩, ⟨_⟩⟩
  congr
Extensionality of Division-Inversion Monoid Structures: Equality via Multiplication and Inversion
Informal description
Let $M$ be a type, and let $m_1$ and $m_2$ be two division-inversion monoid structures on $M$. If the multiplication operations of $m_1$ and $m_2$ are equal (i.e., $a \cdot_{m_1} b = a \cdot_{m_2} b$ for all $a, b \in M$) and the inversion operations are equal (i.e., $a^{-1}_{m_1} = a^{-1}_{m_2}$ for all $a \in M$), then $m_1$ and $m_2$ are equal as division-inversion monoid structures.
Group.toDivInvMonoid_injective theorem
{G : Type*} : Injective (@Group.toDivInvMonoid G)
Full source 
@[to_additive]
lemma Group.toDivInvMonoid_injective {G : Type*} : Injective (@Group.toDivInvMonoid G) := by
  rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
Injectivity of Group-to-DivInvMonoid Map
Informal description
The canonical map from a group structure to its underlying division-inversion monoid structure is injective. In other words, if two group structures on the same type induce the same division-inversion monoid structure, then the group structures must be equal.
Group.ext theorem
{G : Type*} ⦃g₁ g₂ : Group G⦄ (h_mul : (letI := g₁; HMul.hMul : G → G → G) = (letI := g₂; HMul.hMul : G → G → G)) : g₁ = g₂
Full source 
@[to_additive (attr := ext)]
theorem Group.ext {G : Type*} ⦃g₁ g₂ : Group G⦄
    (h_mul : (letI := g₁; HMul.hMul : G → G → G) = (letI := g₂; HMul.hMul : G → G → G)) :
    g₁ = g₂ := by
  have h₁ : g₁.one = g₂.one := congr_arg (·.one) (Monoid.ext h_mul)
  let f : @MonoidHom G G g₁.toMulOneClass g₂.toMulOneClass :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)
  exact
    Group.toDivInvMonoid_injective
      (DivInvMonoid.ext h_mul
        (funext <| @MonoidHom.map_inv G G g₁ g₂.toDivisionMonoid f))
Extensionality of Group Structures: Equality via Multiplication
Informal description
Let $G$ be a type, and let $g_1$ and $g_2$ be two group structures on $G$. If the multiplication operations of $g_1$ and $g_2$ are equal (i.e., $a \cdot_{g_1} b = a \cdot_{g_2} b$ for all $a, b \in G$), then $g_1$ and $g_2$ are equal as group structures.
CommGroup.toGroup_injective theorem
{G : Type*} : Injective (@CommGroup.toGroup G)
Full source 
@[to_additive]
lemma CommGroup.toGroup_injective {G : Type*} : Injective (@CommGroup.toGroup G) := by
  rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl
Injectivity of the Underlying Group Structure in Commutative Groups
Informal description
For any type $G$, the function that maps a commutative group structure on $G$ to its underlying group structure is injective. In other words, if two commutative group structures on $G$ have the same underlying group structure, then they are equal.
CommGroup.ext theorem
{G : Type*} ⦃g₁ g₂ : CommGroup G⦄ (h_mul : (letI := g₁; HMul.hMul : G → G → G) = (letI := g₂; HMul.hMul : G → G → G)) : g₁ = g₂
Full source 
@[to_additive (attr := ext)]
theorem CommGroup.ext {G : Type*} ⦃g₁ g₂ : CommGroup G⦄
    (h_mul : (letI := g₁; HMul.hMul : G → G → G) = (letI := g₂; HMul.hMul : G → G → G)) : g₁ = g₂ :=
  CommGroup.toGroup_injective <| Group.ext h_mul
Extensionality of Commutative Group Structures: Equality via Multiplication
Informal description
Let $G$ be a type, and let $g_1$ and $g_2$ be two commutative group structures on $G$. If the multiplication operations of $g_1$ and $g_2$ are equal (i.e., $a \cdot_{g_1} b = a \cdot_{g_2} b$ for all $a, b \in G$), then $g_1$ and $g_2$ are equal as commutative group structures.