chore(algebra): add `sub{_mul_action,module,semiring,ring,field,algeb…

…ra}.copy` (#7220)


We already have this for sub{monoid,group}. With this in place, we can make `coe subalgebra.range` defeq to `set.range` and similar (left for a follow-up).

src/algebra/algebra/subalgebra.lean

@@ -42,6 +42,14 @@ lemma mem_carrier {s : subalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s :=
 
 @[ext] theorem ext {S T : subalgebra R A} (h : ∀ x : A, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h
 
+/-- Copy of a submodule with a new `carrier` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (S : subalgebra R A) (s : set A) (hs : s = ↑S) : subalgebra R A :=
+{ carrier := s,
+  add_mem' := hs.symm ▸ S.add_mem',
+  mul_mem' := hs.symm ▸ S.mul_mem',
+  algebra_map_mem' := hs.symm ▸ S.algebra_map_mem' }
+
 variables (S : subalgebra R A)
 
 theorem algebra_map_mem (r : R) : algebra_map R A r ∈ S :=

src/algebra/module/submodule.lean

@@ -55,6 +55,14 @@ variables {p q : submodule R M}
 
 @[ext] theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h
 
+/-- Copy of a submodule with a new `carrier` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (p : submodule R M) (s : set M) (hs : s = ↑p) : submodule R M :=
+{ carrier := s,
+  zero_mem' := hs.symm ▸ p.zero_mem',
+  add_mem' := hs.symm ▸ p.add_mem',
+  smul_mem' := hs.symm ▸ p.smul_mem' }
+
 theorem to_add_submonoid_injective :
   injective (to_add_submonoid : submodule R M → add_submonoid M) :=
 λ p q h, set_like.ext'_iff.2 (show _, from set_like.ext'_iff.1 h)

src/data/set_like.lean

@@ -19,12 +19,20 @@ structure my_subobject (X : Type*) :=
 
 namespace my_subobject
 
-instance : set_like (my_subobject R) M :=
+variables (X : Type*)
+
+instance : set_like (my_subobject X) X :=
 ⟨sub_mul_action.carrier, λ p q h, by cases p; cases q; congr'⟩
 
-@[simp] lemma mem_carrier {p : my_subobject R} : x ∈ p.carrier ↔ x ∈ (p : set M) := iff.rfl
+@[simp] lemma mem_carrier {p : my_subobject X} : x ∈ p.carrier ↔ x ∈ (p : set X) := iff.rfl
+
+@[ext] theorem ext {p q : my_subobject X} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h
 
-@[ext] theorem ext {p q : my_subobject R} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h
+/-- Copy of a `my_subobject` with a new `carrier` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (p : my_subobject X) (s : set X) (hs : s = ↑p) : my_subobject X :=
+{ carrier := s,
+  op_mem' := hs.symm ▸ p.op_mem' }
 
 end my_subobject
 ```

src/field_theory/subfield.lean

@@ -94,6 +94,12 @@ lemma mem_carrier {s : subfield K} {x : K} : x ∈ s.carrier ↔ x ∈ s := iff.
 /-- Two subfields are equal if they have the same elements. -/
 @[ext] theorem ext {S T : subfield K} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h
 
+/-- Copy of a submodule with a new `carrier` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (S : subfield K) (s : set K) (hs : s = ↑S) : subfield K :=
+{ carrier := s,
+  inv_mem' := hs.symm ▸ S.inv_mem',
+  ..S.to_subring.copy s hs }
 
 @[simp] lemma coe_to_subring (s : subfield K) : (s.to_subring : set K) = s :=
 rfl

src/group_theory/group_action/sub_mul_action.lean

@@ -52,6 +52,12 @@ iff.rfl
 
 @[ext] theorem ext {p q : sub_mul_action R M} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := set_like.ext h
 
+/-- Copy of a sub_mul_action with a new `carrier` equal to the old one. Useful to fix definitional
+equalities.-/
+protected def copy (p : sub_mul_action R M) (s : set M) (hs : s = ↑p) : sub_mul_action R M :=
+{ carrier := s,
+  smul_mem' := hs.symm ▸ p.smul_mem' }
+
 instance : has_bot (sub_mul_action R M) :=
 ⟨{ carrier := ∅, smul_mem' := λ c, set.not_mem_empty}⟩
 

src/group_theory/submonoid/basic.lean

@@ -91,7 +91,7 @@ attribute [ext] add_submonoid.ext
 
 /-- Copy a submonoid replacing `carrier` with a set that is equal to it. -/
 @[to_additive "Copy an additive submonoid replacing `carrier` with a set that is equal to it."]
-def copy (S : submonoid M) (s : set M) (hs : s = S) : submonoid M :=
+protected def copy (S : submonoid M) (s : set M) (hs : s = S) : submonoid M :=
 { carrier := s,
   one_mem' := hs.symm ▸ S.one_mem',
   mul_mem' := hs.symm ▸ S.mul_mem' }

src/ring_theory/subring.lean

@@ -95,6 +95,13 @@ lemma mem_carrier {s : subring R} {x : R} : x ∈ s.carrier ↔ x ∈ s := iff.r
 /-- Two subrings are equal if they have the same elements. -/
 @[ext] theorem ext {S T : subring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h
 
+/-- Copy of a subring with a new `carrier` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (S : subring R) (s : set R) (hs : s = ↑S) : subring R :=
+{ carrier := s,
+  neg_mem' := hs.symm ▸ S.neg_mem',
+  ..S.to_subsemiring.copy s hs }
+
 lemma to_subsemiring_injective : function.injective (to_subsemiring : subring R → subsemiring R)
 | r s h := ext (set_like.ext_iff.mp h : _)
 

src/ring_theory/subsemiring.lean

@@ -46,6 +46,13 @@ lemma mem_carrier {s : subsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s := i
 /-- Two subsemirings are equal if they have the same elements. -/
 @[ext] theorem ext {S T : subsemiring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := set_like.ext h
 
+/-- Copy of a subsemiring with a new `carrier` equal to the old one. Useful to fix definitional
+equalities.-/
+protected def copy (S : subsemiring R) (s : set R) (hs : s = ↑S) : subsemiring R :=
+{ carrier := s,
+  ..S.to_add_submonoid.copy s hs,
+  ..S.to_submonoid.copy s hs }
+
 lemma to_submonoid_injective : function.injective (to_submonoid : subsemiring R → submonoid R)
 | r s h := ext (set_like.ext_iff.mp h : _)