feat(data/equiv/basic): lemmas about composition with equivalences (#…

…10693)




Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/equiv/basic.lean

@@ -473,6 +473,22 @@ lemma conj_comp (e : α ≃ β) (f₁ f₂ : α → α) :
   e.conj (f₁ ∘ f₂) = (e.conj f₁) ∘ (e.conj f₂) :=
 by apply arrow_congr_comp
 
+lemma eq_comp_symm {α β γ} (e : α ≃ β) (f : β → γ) (g : α → γ) :
+  f = g ∘ e.symm ↔ f ∘ e = g :=
+(e.arrow_congr (equiv.refl γ)).symm_apply_eq.symm
+
+lemma comp_symm_eq {α β γ} (e : α ≃ β) (f : β → γ) (g : α → γ) :
+  g ∘ e.symm = f ↔ g = f ∘ e :=
+(e.arrow_congr (equiv.refl γ)).eq_symm_apply.symm
+
+lemma eq_symm_comp {α β γ} (e : α ≃ β) (f : γ → α) (g : γ → β) :
+  f = e.symm ∘ g ↔ e ∘ f = g :=
+((equiv.refl γ).arrow_congr e).eq_symm_apply
+
+lemma symm_comp_eq {α β γ} (e : α ≃ β) (f : γ → α) (g : γ → β) :
+  e.symm ∘ g = f ↔ g = e ∘ f :=
+((equiv.refl γ).arrow_congr e).symm_apply_eq
+
 section binary_op
 
 variables {α₁ β₁ : Type*} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁)

src/data/equiv/module.lean

@@ -238,6 +238,56 @@ lemma symm_apply_eq {x y} : e.symm x = y ↔ x = e y := e.to_equiv.symm_apply_eq
 lemma eq_symm_apply {x y} : y = e.symm x ↔ e y = x := e.to_equiv.eq_symm_apply
 omit σ'
 
+lemma eq_comp_symm {α : Type*} (f : M₂ → α) (g : M₁ → α) :
+  f = g ∘ e₁₂.symm ↔ f ∘ e₁₂ = g := e₁₂.to_equiv.eq_comp_symm f g
+
+lemma comp_symm_eq {α : Type*} (f : M₂ → α) (g : M₁ → α) :
+  g ∘ e₁₂.symm = f ↔ g = f ∘ e₁₂ := e₁₂.to_equiv.comp_symm_eq f g
+
+lemma eq_symm_comp {α : Type*} (f : α → M₁) (g : α → M₂) :
+  f = e₁₂.symm ∘ g ↔ e₁₂ ∘ f = g := e₁₂.to_equiv.eq_symm_comp f g
+
+lemma symm_comp_eq {α : Type*} (f : α → M₁) (g : α → M₂) :
+  e₁₂.symm ∘ g = f ↔ g = e₁₂ ∘ f := e₁₂.to_equiv.symm_comp_eq f g
+
+variables [ring_hom_comp_triple σ₂₁ σ₁₃ σ₂₃] [ring_hom_comp_triple σ₃₁ σ₁₂ σ₃₂]
+
+include module_M₃
+
+lemma eq_comp_to_linear_map_symm (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
+  f = g.comp e₁₂.symm.to_linear_map ↔ f.comp e₁₂.to_linear_map = g :=
+begin
+  split; intro H; ext,
+  { simp [H, e₁₂.to_equiv.eq_comp_symm f g] },
+  { simp [←H, ←e₁₂.to_equiv.eq_comp_symm f g] }
+end
+
+lemma comp_to_linear_map_symm_eq (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
+  g.comp e₁₂.symm.to_linear_map = f ↔ g = f.comp e₁₂.to_linear_map :=
+begin
+  split; intro H; ext,
+  { simp [←H, ←e₁₂.to_equiv.comp_symm_eq f g] },
+  { simp [H, e₁₂.to_equiv.comp_symm_eq f g] }
+end
+
+lemma eq_to_linear_map_symm_comp (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
+  f = e₁₂.symm.to_linear_map.comp g ↔ e₁₂.to_linear_map.comp f = g :=
+begin
+  split; intro H; ext,
+  { simp [H, e₁₂.to_equiv.eq_symm_comp f g] },
+  { simp [←H, ←e₁₂.to_equiv.eq_symm_comp f g] }
+end
+
+lemma to_linear_map_symm_comp_eq (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
+  e₁₂.symm.to_linear_map.comp g = f ↔ g = e₁₂.to_linear_map.comp f :=
+begin
+  split; intro H; ext,
+  { simp [←H, ←e₁₂.to_equiv.symm_comp_eq f g] },
+  { simp [H, e₁₂.to_equiv.symm_comp_eq f g] }
+end
+
+omit module_M₃
+
 @[simp] lemma refl_symm [module R M] : (refl R M).symm = linear_equiv.refl R M := rfl
 
 @[simp] lemma self_trans_symm [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :

src/data/equiv/mul_add.lean

@@ -279,6 +279,18 @@ e.to_equiv.symm_apply_eq
 lemma eq_symm_apply (e : M ≃* N) {x y} : y = e.symm x ↔ e y = x :=
 e.to_equiv.eq_symm_apply
 
+@[to_additive] lemma eq_comp_symm {α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) :
+  f = g ∘ e.symm ↔ f ∘ e = g := e.to_equiv.eq_comp_symm f g
+
+@[to_additive] lemma comp_symm_eq {α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) :
+  g ∘ e.symm = f ↔ g = f ∘ e := e.to_equiv.comp_symm_eq f g
+
+@[to_additive] lemma eq_symm_comp {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
+  f = e.symm ∘ g ↔ e ∘ f = g := e.to_equiv.eq_symm_comp f g
+
+@[to_additive] lemma symm_comp_eq {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
+  e.symm ∘ g = f ↔ g = e ∘ f := e.to_equiv.symm_comp_eq f g
+
 /-- Two multiplicative isomorphisms agree if they are defined by the
     same underlying function. -/
 @[ext, to_additive