chore(data/equiv/basic): rename involutive.to_equiv to to_perm (#…

…12486)

src/algebra/quandle.lean

@@ -354,13 +354,13 @@ by { intro b, dsimp [dihedral_act], ring }
 instance (n : ℕ) : quandle (dihedral n) :=
 { act := dihedral_act n,
   self_distrib := λ x y z, begin
-    dsimp [function.involutive.to_equiv, dihedral_act], ring,
+    dsimp [dihedral_act], ring,
   end,
   inv_act := dihedral_act n,
   left_inv := λ x, (dihedral_act.inv n x).left_inverse,
   right_inv := λ x, (dihedral_act.inv n x).right_inverse,
   fix := λ x, begin
-    dsimp [function.involutive.to_equiv, dihedral_act], ring,
+    dsimp [dihedral_act], ring,
   end }
 
 end quandle

src/algebra/star/basic.lean

@@ -77,7 +77,7 @@ star_involutive.injective
 
 /-- `star` as an equivalence when it is involutive. -/
 protected def equiv.star [has_involutive_star R] : equiv.perm R :=
-star_involutive.to_equiv _
+star_involutive.to_perm _
 
 lemma eq_star_of_eq_star [has_involutive_star R] {r s : R} (h : r = star s) : s = star r :=
 by simp [h]
@@ -117,14 +117,14 @@ attribute [simp] star_mul
 def star_mul_equiv [semigroup R] [star_semigroup R] : R ≃* Rᵐᵒᵖ :=
 { to_fun := λ x, mul_opposite.op (star x),
   map_mul' := λ x y, (star_mul x y).symm ▸ (mul_opposite.op_mul _ _),
-  ..(has_involutive_star.star_involutive.to_equiv star).trans op_equiv}
+  ..(has_involutive_star.star_involutive.to_perm star).trans op_equiv}
 
 /-- `star` as a `mul_aut` for commutative `R`. -/
 @[simps apply]
 def star_mul_aut [comm_semigroup R] [star_semigroup R] : mul_aut R :=
 { to_fun := star,
   map_mul' := star_mul',
-  ..(has_involutive_star.star_involutive.to_equiv star) }
+  ..(has_involutive_star.star_involutive.to_perm star) }
 
 variables (R)
 
@@ -194,7 +194,7 @@ attribute [simp] star_add
 def star_add_equiv [add_monoid R] [star_add_monoid R] : R ≃+ R :=
 { to_fun := star,
   map_add' := star_add,
-  ..(has_involutive_star.star_involutive.to_equiv star)}
+  ..(has_involutive_star.star_involutive.to_perm star)}
 
 variables (R)
 

src/data/equiv/basic.lean

@@ -82,15 +82,11 @@ instance {F} [equiv_like F α β] : has_coe_t F (α ≃ β) :=
 ⟨λ f, { to_fun := f, inv_fun := equiv_like.inv f, left_inv := equiv_like.left_inv f,
   right_inv := equiv_like.right_inv f }⟩
 
-/-- Convert an involutive function `f` to an equivalence with `to_fun = inv_fun = f`. -/
-def function.involutive.to_equiv (f : α → α) (h : involutive f) : α ≃ α :=
-⟨f, f, h.left_inverse, h.right_inverse⟩
+/-- `perm α` is the type of bijections from `α` to itself. -/
+@[reducible] def equiv.perm (α : Sort*) := equiv α α
 
 namespace equiv
 
-/-- `perm α` is the type of bijections from `α` to itself. -/
-@[reducible] def perm (α : Sort*) := equiv α α
-
 instance : equiv_like (α ≃ β) α β :=
 { coe := to_fun, inv := inv_fun, left_inv := left_inv, right_inv := right_inv,
   coe_injective' := λ e₁ e₂ h₁ h₂, by { cases e₁, cases e₂, congr' } }
@@ -134,9 +130,6 @@ def simps.symm_apply (e : α ≃ β) : β → α := e.symm
 
 initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
 
--- Generate the `simps` projections for previously defined equivs.
-attribute [simps] function.involutive.to_equiv
-
 /-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
 @[trans] protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm,
@@ -1754,6 +1747,20 @@ end swap
 
 end equiv
 
+namespace function.involutive
+
+/-- Convert an involutive function `f` to a permutation with `to_fun = inv_fun = f`. -/
+def to_perm (f : α → α) (h : involutive f) : equiv.perm α :=
+⟨f, f, h.left_inverse, h.right_inverse⟩
+
+@[simp] lemma coe_to_perm {f : α → α} (h : involutive f) : (h.to_perm f : α → α) = f := rfl
+
+@[simp] lemma to_perm_symm {f : α → α} (h : involutive f) : (h.to_perm f).symm = h.to_perm f := rfl
+
+lemma to_perm_involutive {f : α → α} (h : involutive f) : involutive (h.to_perm f) := h
+
+end function.involutive
+
 lemma plift.eq_up_iff_down_eq {x : plift α} {y : α} : x = plift.up y ↔ x.down = y :=
 equiv.plift.eq_symm_apply
 

src/data/equiv/module.lean

@@ -355,7 +355,7 @@ variables [add_comm_monoid M] [add_comm_monoid M₁] [add_comm_monoid M₂]
 def of_involutive {σ σ' : R →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ]
   {module_M : module R M} (f : M →ₛₗ[σ] M) (hf : involutive f) :
   M ≃ₛₗ[σ] M :=
-{ .. f, .. hf.to_equiv f }
+{ .. f, .. hf.to_perm f }
 
 @[simp] lemma coe_of_involutive {σ σ' : R →+* R} [ring_hom_inv_pair σ σ']
   [ring_hom_inv_pair σ' σ] {module_M : module R M} (f : M →ₛₗ[σ] M) (hf : involutive f) :

src/data/equiv/mul_add.lean

@@ -538,7 +538,7 @@ variables (G) [has_involutive_inv G]
 /-- Inversion on a `group` or `group_with_zero` is a permutation of the underlying type. -/
 @[to_additive "Negation on an `add_group` is a permutation of the underlying type.",
   simps apply {fully_applied := ff}]
-protected def inv : perm G := inv_involutive.to_equiv _
+protected def inv : perm G := inv_involutive.to_perm _
 
 variable {G}