Inverso del inverso en grupos

Sea G un grupo y a ∈ G. Demostrar que

    (a⁻¹)⁻¹ = a

1	(a⁻¹)⁻¹ = a

Para ello, completar la siguiente teoría de Lean:

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b : G}

example : (a⁻¹)⁻¹ = a :=
sorry

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b : G}

example : (a⁻¹)⁻¹ = a :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b : G}

-- 1ª demostración
-- ===============

example : (a⁻¹)⁻¹ = a :=
calc (a⁻¹)⁻¹
     = (a⁻¹)⁻¹ * 1         : (mul_one (a⁻¹)⁻¹).symm
 ... = (a⁻¹)⁻¹ * (a⁻¹ * a) : congr_arg ((*) (a⁻¹)⁻¹) (inv_mul_self a).symm
 ... = ((a⁻¹)⁻¹ * a⁻¹) * a : (mul_assoc _ _ _).symm
 ... = 1 * a               : congr_arg (* a) (inv_mul_self a⁻¹)
 ... = a                   : one_mul a

-- 2ª demostración
-- ===============

example : (a⁻¹)⁻¹ = a :=
calc (a⁻¹)⁻¹
     = (a⁻¹)⁻¹ * 1         : by simp only [mul_one]
 ... = (a⁻¹)⁻¹ * (a⁻¹ * a) : by simp only [inv_mul_self]
 ... = ((a⁻¹)⁻¹ * a⁻¹) * a : by simp only [mul_assoc]
 ... = 1 * a               : by simp only [inv_mul_self]
 ... = a                   : by simp only [one_mul]

-- 3ª demostración
-- ===============

example : (a⁻¹)⁻¹ = a :=
calc (a⁻¹)⁻¹
     = (a⁻¹)⁻¹ * 1         : by simp
 ... = (a⁻¹)⁻¹ * (a⁻¹ * a) : by simp
 ... = ((a⁻¹)⁻¹ * a⁻¹) * a : by simp
 ... = 1 * a               : by simp
 ... = a                   : by simp

-- 4ª demostración
-- ===============

example : (a⁻¹)⁻¹ = a :=
begin
  apply inv_eq_of_mul_eq_one,
  exact mul_left_inv a,
end

-- 5ª demostración
-- ===============

example : (a⁻¹)⁻¹ = a :=
inv_eq_of_mul_eq_one (mul_left_inv a)

-- 6ª demostración
-- ===============

example : (a⁻¹)⁻¹ = a:=
inv_inv a

-- 7ª demostración
-- ===============

example : (a⁻¹)⁻¹ = a:=
by simp

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b : G}

-- 1ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a :=

calc (a⁻¹)⁻¹

= (a⁻¹)⁻¹ * 1 : (mul_one (a⁻¹)⁻¹).symm

... = (a⁻¹)⁻¹ * (a⁻¹ * a) : congr_arg ((*) (a⁻¹)⁻¹) (inv_mul_self a).symm

... = ((a⁻¹)⁻¹ * a⁻¹) * a : (mul_assoc _ _ _).symm

... = 1 * a : congr_arg (* a) (inv_mul_self a⁻¹)

... = a : one_mul a

-- 2ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a :=

calc (a⁻¹)⁻¹

= (a⁻¹)⁻¹ * 1 : by simp only [mul_one]

... = (a⁻¹)⁻¹ * (a⁻¹ * a) : by simp only [inv_mul_self]

... = ((a⁻¹)⁻¹ * a⁻¹) * a : by simp only [mul_assoc]

... = 1 * a : by simp only [inv_mul_self]

... = a : by simp only [one_mul]

-- 3ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a :=

calc (a⁻¹)⁻¹

= (a⁻¹)⁻¹ * 1 : by simp

... = (a⁻¹)⁻¹ * (a⁻¹ * a) : by simp

... = ((a⁻¹)⁻¹ * a⁻¹) * a : by simp

... = 1 * a : by simp

... = a : by simp

-- 4ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a :=

begin

apply inv_eq_of_mul_eq_one,

exact mul_left_inv a,

end

-- 5ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a :=

inv_eq_of_mul_eq_one (mul_left_inv a)

-- 6ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a:=

inv_inv a

-- 7ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a:=

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Inverso_del_inverso_en_grupos
imports Main
begin

context group
begin

(* 1ª demostración *)

lemma "inverse (inverse a) = a"
proof -
  have "inverse (inverse a) =
        (inverse (inverse a)) * 1"
    by (simp only: right_neutral)
  also have "… = inverse (inverse a) * (inverse a * a)"
    by (simp only: left_inverse)
  also have "… = (inverse (inverse a) * inverse a) * a"
    by (simp only: assoc)
  also have "… = 1 * a"
    by (simp only: left_inverse)
  also have "… = a"
    by (simp only: left_neutral)
  finally show "inverse (inverse a) = a"
    by this
qed

(* 2ª demostración *)

lemma "inverse (inverse a) = a"
proof -
  have "inverse (inverse a) =
        (inverse (inverse a)) * 1"                      by simp
  also have "… = inverse (inverse a) * (inverse a * a)" by simp
  also have "… = (inverse (inverse a) * inverse a) * a" by simp
  also have "… = 1 * a"                                 by simp
  finally show "inverse (inverse a) = a"                by simp
qed

(* 3ª demostración *)

lemma "inverse (inverse a) = a"
proof (rule inverse_unique)
  show "inverse a * a = 1"
    by (simp only: left_inverse)
qed

(* 4ª demostración *)

lemma "inverse (inverse a) = a"
proof (rule inverse_unique)
  show "inverse a * a = 1" by simp
qed

(* 5ª demostración *)

lemma "inverse (inverse a) = a"
  by (rule inverse_unique) simp

(* 6ª demostración *)

lemma "inverse (inverse a) = a"
  by (simp only: inverse_inverse)

(* 7ª demostración *)

lemma "inverse (inverse a) = a"
  by simp

end

end

theory Inverso_del_inverso_en_grupos

imports Main

begin

context group

begin

(* 1ª demostración *)

lemma "inverse (inverse a) = a"

proof -

have "inverse (inverse a) =

(inverse (inverse a)) * 1"

by (simp only: right_neutral)

also have "… = inverse (inverse a) * (inverse a * a)"

by (simp only: left_inverse)

also have "… = (inverse (inverse a) * inverse a) * a"

by (simp only: assoc)

also have "… = 1 * a"

by (simp only: left_inverse)

also have "… = a"

by (simp only: left_neutral)

finally show "inverse (inverse a) = a"

by this

qed

(* 2ª demostración *)

lemma "inverse (inverse a) = a"

proof -

have "inverse (inverse a) =

(inverse (inverse a)) * 1" by simp

also have "… = inverse (inverse a) * (inverse a * a)" by simp

also have "… = (inverse (inverse a) * inverse a) * a" by simp

also have "… = 1 * a" by simp

finally show "inverse (inverse a) = a" by simp

qed

(* 3ª demostración *)

lemma "inverse (inverse a) = a"

proof (rule inverse_unique)

show "inverse a * a = 1"

by (simp only: left_inverse)

qed

(* 4ª demostración *)

lemma "inverse (inverse a) = a"

proof (rule inverse_unique)

show "inverse a * a = 1" by simp

qed

(* 5ª demostración *)

lemma "inverse (inverse a) = a"

by (rule inverse_unique) simp

(* 6ª demostración *)

lemma "inverse (inverse a) = a"

by (simp only: inverse_inverse)

(* 7ª demostración *)

lemma "inverse (inverse a) = a"

by simp

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Referencia

Propiedad 3.20 del libro Abstract algebra: Theory and applications de Thomas W. Judson.

Referencia

Share this:

Escribe un comentarioCancel reply