chore(data/equiv/basic): arrow_congr preserves properties of binary o…

…perators (#4759)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/data/equiv/basic.lean

@@ -409,6 +409,32 @@ lemma conj_comp (e : α ≃ β) (f₁ f₂ : α → α) :
   e.conj (f₁ ∘ f₂) = (e.conj f₁) ∘ (e.conj f₂) :=
 by apply arrow_congr_comp
 
+section binary_op
+
+variables {α₁ β₁ : Type*} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁)
+
+lemma semiconj_conj (f : α₁ → α₁) : semiconj e f (e.conj f) := λ x, by simp
+
+lemma semiconj₂_conj : semiconj₂ e f (e.arrow_congr e.conj f) := λ x y, by simp
+
+instance [is_associative α₁ f] :
+  is_associative β₁ (e.arrow_congr (e.arrow_congr e) f) :=
+(e.semiconj₂_conj f).is_associative_right e.surjective
+
+instance [is_idempotent α₁ f] :
+  is_idempotent β₁ (e.arrow_congr (e.arrow_congr e) f) :=
+(e.semiconj₂_conj f).is_idempotent_right e.surjective
+
+instance [is_left_cancel α₁ f] :
+  is_left_cancel β₁ (e.arrow_congr (e.arrow_congr e) f) :=
+⟨e.surjective.forall₃.2 $ λ x y z, by simpa using @is_left_cancel.left_cancel _ f _ x y z⟩
+
+instance [is_right_cancel α₁ f] :
+  is_right_cancel β₁ (e.arrow_congr (e.arrow_congr e) f) :=
+⟨e.surjective.forall₃.2 $ λ x y z, by simpa using @is_right_cancel.right_cancel _ f _ x y z⟩
+
+end binary_op
+
 /-- `punit` sorts in any two universes are equivalent. -/
 def punit_equiv_punit : punit.{v} ≃ punit.{w} :=
 ⟨λ _, punit.star, λ _, punit.star, λ u, by { cases u, refl }, λ u, by { cases u, reflexivity }⟩

src/logic/function/conjugate.lean

@@ -98,6 +98,22 @@ lemma comp {f' : β → γ} {gc : γ → γ → γ} (hf' : semiconj₂ f' gb gc)
   semiconj₂ (f' ∘ f) ga gc :=
 λ x y, by simp only [hf'.eq, hf.eq, comp_app]
 
+lemma is_associative_right [is_associative α ga] (h : semiconj₂ f ga gb) (h_surj : surjective f) :
+  is_associative β gb :=
+⟨h_surj.forall₃.2 $ λ x₁ x₂ x₃, by simp only [← h.eq, @is_associative.assoc _ ga]⟩
+
+lemma is_associative_left [is_associative β gb] (h : semiconj₂ f ga gb) (h_inj : injective f) :
+  is_associative α ga :=
+⟨λ x₁ x₂ x₃, h_inj $ by simp only [h.eq, @is_associative.assoc _ gb]⟩
+
+lemma is_idempotent_right [is_idempotent α ga] (h : semiconj₂ f ga gb) (h_surj : surjective f) :
+  is_idempotent β gb :=
+⟨h_surj.forall.2 $ λ x, by simp only [← h.eq, @is_idempotent.idempotent _ ga]⟩
+
+lemma is_idempotent_left [is_idempotent β gb] (h : semiconj₂ f ga gb) (h_inj : injective f) :
+  is_idempotent α ga :=
+⟨λ x, h_inj $ by rw [h.eq, @is_idempotent.idempotent _ gb]⟩
+
 end semiconj₂
 
 end function