feat: def ofClass and CanLift instances for algebraic subobjects (#23708)

For each algebraic subobject, this creates an `ofClass` definition which takes an element of a `SetLike` with the appropriate hypotheses and turns it into a subobject of this type. This is *not* marked as a coercion (unlike for morphisms).

In addition, we provide `CanLift` instances from `Set` to the various subobjects for use in proofs.

We already have these declarations for `Submonoid` and `Subgroup`.

In addition, there are two very minor housekeeping items that we fix which arose during the creation of this PR.

1. renaming an instance
2. protecting `StarSubalgebra.algebraMap_mem`

Author: j-loreaux

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -75,6 +75,29 @@ instance : SetLike (NonUnitalSubalgebra R A) A where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective h
 
+/-- The actual `NonUnitalSubalgebra` obtained from an element of a type satisfying
+`NonUnitalSubsemiringClass` and `SMulMemClass`. -/
+@[simps]
+def ofClass {S R A : Type*} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A]
+    [SetLike S A] [NonUnitalSubsemiringClass S A] [SMulMemClass S R A]
+    (s : S) : NonUnitalSubalgebra R A where
+  carrier := s
+  add_mem' := add_mem
+  zero_mem' := zero_mem _
+  mul_mem' := mul_mem
+  smul_mem' := SMulMemClass.smul_mem
+
+instance (priority := 100) : CanLift (Set A) (NonUnitalSubalgebra R A) (↑)
+    (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧
+      ∀ (r : R) {x}, x ∈ s → r • x ∈ s) where
+  prf s h :=
+    ⟨ { carrier := s
+        zero_mem' := h.1
+        add_mem' := h.2.1
+        mul_mem' := h.2.2.1
+        smul_mem' := h.2.2.2 },
+      rfl ⟩
+
 instance instNonUnitalSubsemiringClass :
     NonUnitalSubsemiringClass (NonUnitalSubalgebra R A) A where
   add_mem {s} := s.add_mem'

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -39,14 +39,40 @@ instance : SetLike (Subalgebra R A) A where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
 
-instance SubsemiringClass : SubsemiringClass (Subalgebra R A) A where
+initialize_simps_projections Subalgebra (carrier → coe, as_prefix coe)
+
+/-- The actual `Subalgebra` obtained from an element of a type satisfying `SubsemiringClass` and
+`SMulMemClass`. -/
+@[simps]
+def ofClass {S R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
+    [SetLike S A] [SubsemiringClass S A] [SMulMemClass S R A] (s : S) :
+    Subalgebra R A where
+  carrier := s
+  add_mem' := add_mem
+  zero_mem' := zero_mem _
+  mul_mem' := mul_mem
+  one_mem' := one_mem _
+  algebraMap_mem' r :=
+    Algebra.algebraMap_eq_smul_one (A := A) r ▸ SMulMemClass.smul_mem r (one_mem s)
+
+instance (priority := 100) : CanLift (Set A) (Subalgebra R A) (↑)
+    (fun s ↦ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧
+      (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), algebraMap R A r ∈ s) where
+  prf s h :=
+    ⟨ { carrier := s
+        zero_mem' := by simpa using h.2.2 0
+        add_mem' := h.1
+        one_mem' := by simpa using h.2.2 1
+        mul_mem' := h.2.1
+        algebraMap_mem' := h.2.2 },
+      rfl ⟩
+
+instance : SubsemiringClass (Subalgebra R A) A where
   add_mem {s} := add_mem (s := s.toSubsemiring)
   mul_mem {s} := mul_mem (s := s.toSubsemiring)
   one_mem {s} := one_mem s.toSubsemiring
   zero_mem {s} := zero_mem s.toSubsemiring
 
-initialize_simps_projections Subalgebra (carrier → coe, as_prefix coe)
-
 @[simp]
 theorem mem_toSubsemiring {S : Subalgebra R A} {x} : x ∈ S.toSubsemiring ↔ x ∈ S :=
   Iff.rfl
@@ -157,7 +183,7 @@ lemma one_mem_toNonUnitalSubalgebra (S : Subalgebra R A) : (1 : A) ∈ S.toNonUn
   S.one_mem
 
 instance {R A : Type*} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) A :=
-  { Subalgebra.SubsemiringClass with
+  { Subalgebra.instSubsemiringClass with
     neg_mem := fun {S x} hx => neg_one_smul R x ▸ S.smul_mem hx _ }
 
 protected theorem neg_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]

Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -286,12 +286,6 @@ add_decl_doc AddSubgroup.toAddSubmonoid
 
 namespace Subgroup
 
-/-- The actual `Subgroup` obtained from an element of a `SubgroupClass` -/
-@[to_additive "The actual `AddSubgroup` obtained from an element of a `AddSubgroupClass`"]
-def ofClass {S G : Type*} [Group G] [SetLike S G] [SubgroupClass S G]
-    (s : S) : Subgroup G :=
-  ⟨⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩, InvMemClass.inv_mem⟩
-
 @[to_additive]
 instance : SetLike (Subgroup G) G where
   coe s := s.carrier
@@ -300,8 +294,18 @@ instance : SetLike (Subgroup G) G where
     obtain ⟨⟨⟨hq,_⟩,_⟩,_⟩ := q
     congr
 
+initialize_simps_projections Subgroup (carrier → coe, as_prefix coe)
+initialize_simps_projections AddSubgroup (carrier → coe, as_prefix coe)
+
+/-- The actual `Subgroup` obtained from an element of a `SubgroupClass` -/
+@[to_additive (attr := simps) "The actual `AddSubgroup` obtained from an element of a
+`AddSubgroupClass`"]
+def ofClass {S G : Type*} [Group G] [SetLike S G] [SubgroupClass S G]
+    (s : S) : Subgroup G :=
+  ⟨⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩, InvMemClass.inv_mem⟩
+
 @[to_additive]
-instance : CanLift (Set G) (Subgroup G) (↑)
+instance (priority := 100) : CanLift (Set G) (Subgroup G) (↑)
     (fun s ↦ 1 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → x⁻¹ ∈ s) where
   prf s h := ⟨{ carrier := s, one_mem' := h.1, mul_mem' := h.2.1, inv_mem' := h.2.2}, rfl⟩
 
@@ -333,9 +337,6 @@ theorem mk_le_mk {s t : Set G} (h_one) (h_mul) (h_inv) (h_one') (h_mul') (h_inv'
     mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ≤ mk ⟨⟨t, h_one'⟩, h_mul'⟩ h_inv' ↔ s ⊆ t :=
   Iff.rfl
 
-initialize_simps_projections Subgroup (carrier → coe, as_prefix coe)
-initialize_simps_projections AddSubgroup (carrier → coe, as_prefix coe)
-
 @[to_additive (attr := simp)]
 theorem coe_toSubmonoid (K : Subgroup G) : (K.toSubmonoid : Set G) = K :=
   rfl

Mathlib/Algebra/Group/Submonoid/Defs.lean

@@ -122,18 +122,22 @@ theorem pow_mem {M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x :
 
 namespace Submonoid
 
-/-- The actual `Submonoid` obtained from an element of a `SubmonoidClass` -/
-@[to_additive "The actual `AddSubmonoid` obtained from an element of a `AddSubmonoidClass`"]
-def ofClass {S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M] (s : S) : Submonoid M :=
-  ⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩
-
 @[to_additive]
 instance : SetLike (Submonoid M) M where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
 
+initialize_simps_projections Submonoid (carrier → coe, as_prefix coe)
+initialize_simps_projections AddSubmonoid (carrier → coe, as_prefix coe)
+
+/-- The actual `Submonoid` obtained from an element of a `SubmonoidClass` -/
+@[to_additive (attr := simps) "The actual `AddSubmonoid` obtained from an element of a
+`AddSubmonoidClass`"]
+def ofClass {S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M] (s : S) : Submonoid M :=
+  ⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩
+
 @[to_additive]
-instance : CanLift (Set M) (Submonoid M) (↑)
+instance (priority := 100) : CanLift (Set M) (Submonoid M) (↑)
     (fun s ↦ 1 ∈ s ∧ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) where
   prf s h := ⟨{ carrier := s, one_mem' := h.1, mul_mem' := h.2 }, rfl⟩
 
@@ -142,9 +146,6 @@ instance : SubmonoidClass (Submonoid M) M where
   one_mem := Submonoid.one_mem'
   mul_mem {s} := s.mul_mem'
 
-initialize_simps_projections Submonoid (carrier → coe, as_prefix coe)
-initialize_simps_projections AddSubmonoid (carrier → coe, as_prefix coe)
-
 @[to_additive (attr := simp)]
 theorem mem_toSubsemigroup {s : Submonoid M} {x : M} : x ∈ s.toSubsemigroup ↔ x ∈ s :=
   Iff.rfl

Mathlib/Algebra/Group/Subsemigroup/Defs.lean

@@ -94,12 +94,23 @@ namespace Subsemigroup
 instance : SetLike (Subsemigroup M) M :=
   ⟨Subsemigroup.carrier, fun p q h => by cases p; cases q; congr⟩
 
-@[to_additive]
-instance : MulMemClass (Subsemigroup M) M where mul_mem := fun {_ _ _} => Subsemigroup.mul_mem' _
-
 initialize_simps_projections Subsemigroup (carrier → coe, as_prefix coe)
 initialize_simps_projections AddSubsemigroup (carrier → coe, as_prefix coe)
 
+/-- The actual `Subsemigroup` obtained from an element of a `MulMemClass`. -/
+@[to_additive (attr := simps) "The actual `AddSubsemigroup` obtained from an element of a
+`AddMemClass`"]
+def ofClass {S M : Type*} [Mul M] [SetLike S M] [MulMemClass S M] (s : S) : Subsemigroup M :=
+  ⟨s, MulMemClass.mul_mem⟩
+
+@[to_additive]
+instance (priority := 100) : CanLift (Set M) (Subsemigroup M) (↑)
+    (fun s ↦ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) where
+  prf s h := ⟨{ carrier := s, mul_mem' := h }, rfl⟩
+
+@[to_additive]
+instance : MulMemClass (Subsemigroup M) M where mul_mem := fun {_ _ _} => Subsemigroup.mul_mem' _
+
 @[to_additive (attr := simp)]
 theorem mem_carrier {s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s :=
   Iff.rfl

Mathlib/Algebra/Module/Submodule/Defs.lean

@@ -51,15 +51,33 @@ instance setLike : SetLike (Submodule R M) M where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
 
+initialize_simps_projections Submodule (carrier → coe, as_prefix coe)
+
+/-- The actual `Submodule` obtained from an element of a `SMulMemClass` and `AddSubmonoidClass`. -/
+@[simps]
+def ofClass {S R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M]
+    [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) : Submodule R M where
+  carrier := s
+  add_mem' := add_mem
+  zero_mem' := zero_mem _
+  smul_mem' := SMulMemClass.smul_mem
+
+instance (priority := 100) : CanLift (Set M) (Submodule R M) (↑)
+    (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x}, x ∈ s → r • x ∈ s) where
+  prf s h :=
+    ⟨ { carrier := s
+        zero_mem' := h.1
+        add_mem' := h.2.1
+        smul_mem' := h.2.2 },
+      rfl ⟩
+
 instance addSubmonoidClass : AddSubmonoidClass (Submodule R M) M where
   zero_mem _ := AddSubmonoid.zero_mem' _
   add_mem := AddSubsemigroup.add_mem' _
 
 instance smulMemClass : SMulMemClass (Submodule R M) R M where
   smul_mem {s} c _ h := SubMulAction.smul_mem' s.toSubMulAction c h
 
-initialize_simps_projections Submodule (carrier → coe, as_prefix coe)
-
 @[simp]
 theorem mem_toAddSubmonoid (p : Submodule R M) (x : M) : x ∈ p.toAddSubmonoid ↔ x ∈ p :=
   Iff.rfl

Mathlib/Algebra/Ring/Subring/Defs.lean

@@ -164,15 +164,38 @@ instance : SetLike (Subring R) R where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
 
+initialize_simps_projections Subring (carrier → coe, as_prefix coe)
+
+/-- The actual `Subring` obtained from an element of a `SubringClass`. -/
+@[simps]
+def ofClass {S R : Type*} [Ring R] [SetLike S R] [SubringClass S R]
+    (s : S) : Subring R where
+  carrier := s
+  add_mem' := add_mem
+  zero_mem' := zero_mem _
+  mul_mem' := mul_mem
+  neg_mem' := neg_mem
+  one_mem' := one_mem _
+
+instance (priority := 100) : CanLift (Set R) (Subring R) (↑)
+    (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧
+      (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → -x ∈ s) where
+  prf s h :=
+    ⟨ { carrier := s
+        zero_mem' := h.1
+        add_mem' := h.2.1
+        one_mem' := h.2.2.1
+        mul_mem' := h.2.2.2.1
+        neg_mem' := h.2.2.2.2 },
+      rfl ⟩
+
 instance : SubringClass (Subring R) R where
   zero_mem s := s.zero_mem'
   add_mem {s} := s.add_mem'
   one_mem s := s.one_mem'
   mul_mem {s} := s.mul_mem'
   neg_mem {s} := s.neg_mem'
 
-initialize_simps_projections Subring (carrier → coe, as_prefix coe)
-
 /-- Turn a `Subring` into a `NonUnitalSubring` by forgetting that it contains `1`. -/
 def toNonUnitalSubring (S : Subring R) : NonUnitalSubring R where __ := S
 

Mathlib/Algebra/Ring/Subsemiring/Defs.lean

@@ -139,14 +139,35 @@ instance : SetLike (Subsemiring R) R where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
 
+initialize_simps_projections Subsemiring (carrier → coe, as_prefix coe)
+
+/-- The actual `Subsemiring` obtained from an element of a `SubsemiringClass`. -/
+@[simps]
+def ofClass {S R : Type*} [NonAssocSemiring R] [SetLike S R] [SubsemiringClass S R]
+    (s : S) : Subsemiring R where
+  carrier := s
+  add_mem' := add_mem
+  zero_mem' := zero_mem _
+  mul_mem' := mul_mem
+  one_mem' := one_mem _
+
+instance (priority := 100) : CanLift (Set R) (Subsemiring R) (↑)
+    (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧
+      ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) where
+  prf s h :=
+    ⟨ { carrier := s
+        zero_mem' := h.1
+        add_mem' := h.2.1
+        one_mem' := h.2.2.1
+        mul_mem' := h.2.2.2 },
+      rfl ⟩
+
 instance : SubsemiringClass (Subsemiring R) R where
   zero_mem := zero_mem'
   add_mem {s} := AddSubsemigroup.add_mem' s.toAddSubmonoid.toAddSubsemigroup
   one_mem {s} := Submonoid.one_mem' s.toSubmonoid
   mul_mem {s} := Subsemigroup.mul_mem' s.toSubmonoid.toSubsemigroup
 
-initialize_simps_projections Subsemiring (carrier → coe, as_prefix coe)
-
 /-- Turn a `Subsemiring` into a `NonUnitalSubsemiring` by forgetting that it contains `1`. -/
 def toNonUnitalSubsemiring (S : Subsemiring R) : NonUnitalSubsemiring R where __ := S
 

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -115,6 +115,31 @@ instance instSetLike : SetLike (NonUnitalStarSubalgebra R A) A where
   coe {s} := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective h
 
+/-- The actual `NonUnitalStarSubalgebra` obtained from an element of a type satisfying
+`NonUnitalSubsemiringClass`, `SMulMemClass` and `StarMemClass`. -/
+@[simps]
+def ofClass {S R A : Type*} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A]
+    [SetLike S A] [NonUnitalSubsemiringClass S A] [SMulMemClass S R A] [StarMemClass S A]
+    (s : S) : NonUnitalStarSubalgebra R A where
+  carrier := s
+  add_mem' := add_mem
+  zero_mem' := zero_mem _
+  mul_mem' := mul_mem
+  smul_mem' := SMulMemClass.smul_mem
+  star_mem' := star_mem
+
+instance (priority := 100) : CanLift (Set A) (NonUnitalStarSubalgebra R A) (↑)
+    (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧
+      (∀ (r : R) {x}, x ∈ s → r • x ∈ s) ∧ ∀ {x}, x ∈ s → star x ∈ s) where
+  prf s h :=
+    ⟨ { carrier := s
+        zero_mem' := h.1
+        add_mem' := h.2.1
+        mul_mem' := h.2.2.1
+        smul_mem' := h.2.2.2.1
+        star_mem' := h.2.2.2.2 },
+      rfl ⟩
+
 instance instNonUnitalSubsemiringClass :
     NonUnitalSubsemiringClass (NonUnitalStarSubalgebra R A) A where
   add_mem {s} := s.add_mem'

Mathlib/Algebra/Star/NonUnitalSubsemiring.lean

@@ -46,12 +46,38 @@ section NonUnitalStarSubsemiring
 
 namespace NonUnitalStarSubsemiring
 
-variable {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R]
-
-instance instSetLike : SetLike (NonUnitalStarSubsemiring R) R where
+instance instSetLike {R : Type v} [NonUnitalNonAssocSemiring R] [Star R] :
+    SetLike (NonUnitalStarSubsemiring R) R where
   coe {s} := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective h
 
+initialize_simps_projections NonUnitalStarSubsemiring (carrier → coe, as_prefix coe)
+
+variable {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R]
+
+/-- The actual `NonUnitalStarSubsemiring` obtained from an element of a type satisfying
+`NonUnitalSubsemiringClass` and `StarMemClass`. -/
+@[simps]
+def ofClass {S R : Type*} [NonUnitalNonAssocSemiring R] [StarRing R] [SetLike S R]
+    [NonUnitalSubsemiringClass S R] [StarMemClass S R] (s : S) : NonUnitalStarSubsemiring R where
+  carrier := s
+  add_mem' := add_mem
+  zero_mem' := zero_mem _
+  mul_mem' := mul_mem
+  star_mem' := star_mem
+
+instance (priority := 100) : CanLift (Set R) (NonUnitalStarSubsemiring R) (↑)
+    (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧
+      ∀ {x}, x ∈ s → star x ∈ s)
+    where
+  prf s h :=
+    ⟨ { carrier := s
+        zero_mem' := h.1
+        add_mem' := h.2.1
+        mul_mem' := h.2.2.1
+        star_mem' := h.2.2.2 },
+      rfl ⟩
+
 instance instNonUnitalSubsemiringClass :
     NonUnitalSubsemiringClass (NonUnitalStarSubsemiring R) R where
   add_mem {s} := s.add_mem'