IH.inj – Calculemus

La composición por la izquierda con una inyectiva es una operación inyectiva

PorJosé A. Alonso 20 agosto 202121 agosto 2021

Sean f₁ y f₂ funciones de X en Y y g una función de X en Y. Demostrar que si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂.

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

import tactic

variables {X Y Z : Type*}
variables {f₁ f₂ : X → Y}
variable  {g : Y → Z}

example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
sorry

import tactic

variables {X Y Z : Type*}

variables {f₁ f₂ : X → Y}

variable {g : Y → Z}

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variables {X Y Z : Type*}
variables {f₁ f₂ : X → Y}
variable  {g : Y → Z}

-- 1ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  calc g (f₁ x)
       = (g ∘ f₁) x : rfl
   ... = (g ∘ f₂) x : congr_fun hgf x
   ... = g (f₂ x)   : rfl,
end

-- 2ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  exact congr_fun hgf x,
end

-- 3ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  refine funext (λ i, hg _),
  exact congr_fun hgf i,
end

-- 4ª demostración
example
  (hg : function.injective g)
  : function.injective ((∘) g : (X → Y) → (X → Z)) :=
λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))

-- 5ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : (left_id f₁).symm
    ... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl
    ... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _
    ... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf
    ... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _
    ... = id ∘ f₂              : congr_arg2 (∘) (inv_fun_comp hg) rfl
    ... = f₂                   : left_id f₂

-- 6ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : by finish
    ... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp]
    ... = inv_fun g ∘ (g ∘ f₁) : by refl
    ... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf]
    ... = (inv_fun g ∘ g) ∘ f₂ : by refl
    ... = id ∘ f₂              : by finish [inv_fun_comp]
    ... = f₂                   : by finish

import tactic

variables {X Y Z : Type*}

variables {f₁ f₂ : X → Y}

variable {g : Y → Z}

-- 1ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

funext,

apply hg,

calc g (f₁ x)

= (g ∘ f₁) x : rfl

... = (g ∘ f₂) x : congr_fun hgf x

... = g (f₂ x) : rfl,

end

-- 2ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

funext,

apply hg,

exact congr_fun hgf x,

end

-- 3ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

refine funext (λ i, hg _),

exact congr_fun hgf i,

end

-- 4ª demostración

example

(hg : function.injective g)

: function.injective ((∘) g : (X → Y) → (X → Z)) :=

λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))

-- 5ª demostración

example

[hY : nonempty Y]

(hg : injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

calc f₁ = id ∘ f₁ : (left_id f₁).symm

... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl

... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _

... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf

... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _

... = id ∘ f₂ : congr_arg2 (∘) (inv_fun_comp hg) rfl

... = f₂ : left_id f₂

-- 6ª demostración

example

[hY : nonempty Y]

(hg : injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

calc f₁ = id ∘ f₁ : by finish

... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp]

... = inv_fun g ∘ (g ∘ f₁) : by refl

... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf]

... = (inv_fun g ∘ g) ∘ f₂ : by refl

... = id ∘ f₂ : by finish [inv_fun_comp]

... = f₂ : by finish

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 La_composicion_por_la_izquierda_con_una_inyectiva_es_inyectiva
imports Main
begin

(* 1ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof (rule ext)
  fix x
  have "(g ∘ f1) x = (g ∘ f2) x"
    using ‹g ∘ f1 = g ∘ f2› by (rule fun_cong)
  then have "g (f1 x) = g (f2 x)"
    by (simp only: o_apply)
  then show "f1 x = f2 x"
    using ‹inj g› by (simp only: injD)
qed

(* 2ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof
  fix x
  have "(g ∘ f1) x = (g ∘ f2) x"
    using ‹g ∘ f1 = g ∘ f2› by simp
  then have "g (f1 x) = g (f2 x)"
    by simp
  then show "f1 x = f2 x"
    using ‹inj g› by (simp only: injD)
qed

(* 3ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
using assms
by (metis fun.inj_map_strong inj_eq)

(* 4ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = id ∘ f1"
    by (rule id_o [symmetric])
  also have "… = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = inv g ∘ (g ∘ f1)"
    by (simp add: comp_assoc)
  also have "… = inv g ∘ (g ∘ f2)"
    using assms(2) by (rule arg_cong)
  also have "… = (inv g ∘ g) ∘ f2"
    by (simp add: comp_assoc)
  also have "… = id ∘ f2"
    by (simp add: assms(1))
  also have "… = f2"
    by (rule id_o)
  finally show "f1 = f2"
    by this
qed

(* 5ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = (inv g ∘ g) ∘ f2"
    using assms(2) by (simp add: comp_assoc)
  also have "… = f2"
    using assms(1) by simp
  finally show "f1 = f2" .
qed

end

theory La_composicion_por_la_izquierda_con_una_inyectiva_es_inyectiva

imports Main

begin

(* 1ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof (rule ext)

fix x

have "(g ∘ f1) x = (g ∘ f2) x"

using ‹g ∘ f1 = g ∘ f2› by (rule fun_cong)

then have "g (f1 x) = g (f2 x)"

by (simp only: o_apply)

then show "f1 x = f2 x"

using ‹inj g› by (simp only: injD)

qed

(* 2ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof

fix x

have "(g ∘ f1) x = (g ∘ f2) x"

using ‹g ∘ f1 = g ∘ f2› by simp

then have "g (f1 x) = g (f2 x)"

by simp

then show "f1 x = f2 x"

using ‹inj g› by (simp only: injD)

qed

(* 3ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

using assms

by (metis fun.inj_map_strong inj_eq)

(* 4ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof -

have "f1 = id ∘ f1"

by (rule id_o [symmetric])

also have "… = (inv g ∘ g) ∘ f1"

by (simp add: assms(1))

also have "… = inv g ∘ (g ∘ f1)"

by (simp add: comp_assoc)

also have "… = inv g ∘ (g ∘ f2)"

using assms(2) by (rule arg_cong)

also have "… = (inv g ∘ g) ∘ f2"

by (simp add: comp_assoc)

also have "… = id ∘ f2"

by (simp add: assms(1))

also have "… = f2"

by (rule id_o)

finally show "f1 = f2"

by this

qed

(* 5ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof -

have "f1 = (inv g ∘ g) ∘ f1"

by (simp add: assms(1))

also have "… = (inv g ∘ g) ∘ f2"

using assms(2) by (simp add: comp_assoc)

also have "… = f2"

using assms(1) by simp

finally show "f1 = f2" .

qed

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]