feat(group_theory/group_action/defs): add ext attributes (#11936)

This adds `ext` attributes to `has_scalar`, `mul_action`, `distrib_mul_action`, `mul_distrib_mul_action`, and `module`.

The `ext` and `ext_iff` lemmas were eventually generated by `category_theory/preadditive/schur.lean` anyway - we may as well generate them much earlier.

The generated lemmas are slightly uglier than the `module_ext` we already have, but it doesn't really seem worth the trouble of writing out the "nice" versions when the `ext` tactic cleans up the mess for us anyway.

Author: eric-wieser

src/algebra/group/defs.lean

@@ -43,7 +43,7 @@ class has_vadd (G : Type*) (P : Type*) := (vadd : G → P → P)
 class has_vsub (G : out_param Type*) (P : Type*) := (vsub : P → P → G)
 
 /-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
-@[to_additive has_vadd]
+@[ext, to_additive has_vadd]
 class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α)
 
 infix ` +ᵥ `:65 := has_vadd.vadd

src/algebra/module/basic.lean

@@ -47,7 +47,7 @@ variables {R : Type u} {k : Type u'} {S : Type v} {M : Type w} {M₂ : Type x} {
   connected by a "scalar multiplication" operation `r • x : M`
   (where `r : R` and `x : M`) with some natural associativity and
   distributivity axioms similar to those on a ring. -/
-@[protect_proj] class module (R : Type u) (M : Type v) [semiring R]
+@[ext, protect_proj] class module (R : Type u) (M : Type v) [semiring R]
   [add_comm_monoid M] extends distrib_mul_action R M :=
 (add_smul : ∀(r s : R) (x : M), (r + s) • x = r • x + s • x)
 (zero_smul : ∀x : M, (0 : R) • x = 0)
@@ -212,19 +212,14 @@ by letI := H.to_has_scalar; exact
 
 end add_comm_group
 
-/--
-To prove two module structures on a fixed `add_comm_monoid` agree,
-it suffices to check the scalar multiplications agree.
--/
+/-- A variant of `module.ext` that's convenient for term-mode. -/
 -- We'll later use this to show `module ℕ M` and `module ℤ M` are subsingletons.
-@[ext]
-lemma module_ext {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M] (P Q : module R M)
+lemma module.ext' {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M] (P Q : module R M)
   (w : ∀ (r : R) (m : M), by { haveI := P, exact r • m } = by { haveI := Q, exact r • m }) :
   P = Q :=
 begin
-  unfreezingI { rcases P with ⟨⟨⟨⟨P⟩⟩⟩⟩, rcases Q with ⟨⟨⟨⟨Q⟩⟩⟩⟩ },
-  obtain rfl : P = Q, by { funext r m, exact w r m },
-  congr
+  ext,
+  exact w _ _
 end
 
 section module
@@ -318,7 +313,7 @@ by rw [nsmul_eq_smul_cast ℕ n x, nat.cast_id]
 should normally have exactly one `ℕ`-module structure by design. -/
 def add_comm_monoid.nat_module.unique : unique (module ℕ M) :=
 { default := by apply_instance,
-  uniq := λ P, module_ext P _ $ λ n, nat_smul_eq_nsmul P n }
+  uniq := λ P, module.ext' P _ $ λ n, nat_smul_eq_nsmul P n }
 
 instance add_comm_monoid.nat_is_scalar_tower :
   is_scalar_tower ℕ R M :=
@@ -360,7 +355,7 @@ by rw [zsmul_eq_smul_cast ℤ n x, int.cast_id]
 should normally have exactly one `ℤ`-module structure by design. -/
 def add_comm_group.int_module.unique : unique (module ℤ M) :=
 { default := by apply_instance,
-  uniq := λ P, module_ext P _ $ λ n, int_smul_eq_zsmul P n }
+  uniq := λ P, module.ext' P _ $ λ n, int_smul_eq_zsmul P n }
 
 end add_comm_group
 
@@ -422,7 +417,7 @@ end add_monoid_hom
 an instance because `simp` becomes very slow if we have many `subsingleton` instances,
 see [gh-6025]. -/
 lemma subsingleton_rat_module (E : Type*) [add_comm_group E] : subsingleton (module ℚ E) :=
-⟨λ P Q, module_ext P Q $ λ r x,
+⟨λ P Q, module.ext' P Q $ λ r x,
   @add_monoid_hom.map_rat_module_smul E ‹_› P E ‹_› Q (add_monoid_hom.id _) r x⟩
 
 /-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications

src/category_theory/preadditive/schur.lean

@@ -87,8 +87,6 @@ variables [is_alg_closed 𝕜] [linear 𝕜 C]
 -- These are definitionally equal, but without eta reduction Lean can't see this.
 -- To get around this, we use `convert I`,
 -- then check the various instances agree field-by-field,
--- using `ext` equipped with the following extra lemmas:
-local attribute [ext] module distrib_mul_action mul_action has_scalar
 
 /--
 An auxiliary lemma for Schur's lemma.

src/group_theory/group_action/defs.lean

@@ -76,12 +76,12 @@ instance has_mul.to_has_scalar (α : Type*) [has_mul α] : has_scalar α α := 
 @[simp, to_additive] lemma smul_eq_mul (α : Type*) [has_mul α] {a a' : α} : a • a' = a * a' := rfl
 
 /-- Type class for additive monoid actions. -/
-@[protect_proj] class add_action (G : Type*) (P : Type*) [add_monoid G] extends has_vadd G P :=
+@[ext, protect_proj] class add_action (G : Type*) (P : Type*) [add_monoid G] extends has_vadd G P :=
 (zero_vadd : ∀ p : P, (0 : G) +ᵥ p = p)
 (add_vadd : ∀ (g₁ g₂ : G) (p : P), (g₁ + g₂) +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p))
 
 /-- Typeclass for multiplicative actions by monoids. This generalizes group actions. -/
-@[protect_proj, to_additive]
+@[ext, protect_proj, to_additive]
 class mul_action (α : Type*) (β : Type*) [monoid α] extends has_scalar α β :=
 (one_smul : ∀ b : β, (1 : α) • b = b)
 (mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)
@@ -452,7 +452,7 @@ lemma is_scalar_tower.of_smul_one_mul {M N} [monoid N] [has_scalar M N]
 end compatible_scalar
 
 /-- Typeclass for multiplicative actions on additive structures. This generalizes group modules. -/
-class distrib_mul_action (M : Type*) (A : Type*) [monoid M] [add_monoid A]
+@[ext] class distrib_mul_action (M : Type*) (A : Type*) [monoid M] [add_monoid A]
   extends mul_action M A :=
 (smul_add : ∀(r : M) (x y : A), r • (x + y) = r • x + r • y)
 (smul_zero : ∀(r : M), r • (0 : A) = 0)
@@ -547,7 +547,7 @@ end
 
 /-- Typeclass for multiplicative actions on multiplicative structures. This generalizes
 conjugation actions. -/
-class mul_distrib_mul_action (M : Type*) (A : Type*) [monoid M] [monoid A]
+@[ext] class mul_distrib_mul_action (M : Type*) (A : Type*) [monoid M] [monoid A]
   extends mul_action M A :=
 (smul_mul : ∀ (r : M) (x y : A), r • (x * y) = (r • x) * (r • y))
 (smul_one : ∀ (r : M), r • (1 : A) = 1)

src/number_theory/number_field.lean

@@ -107,14 +107,16 @@ namespace rat
 
 open number_field
 
+local attribute [instance] subsingleton_rat_module
+
 instance rat.number_field : number_field ℚ :=
 { to_char_zero := infer_instance,
-  to_finite_dimensional := by { convert (infer_instance : finite_dimensional ℚ ℚ),
-             -- The vector space structure of `ℚ` over itself can arise in multiple ways:
-             -- all fields are vector spaces over themselves (used in `rat.finite_dimensional`)
-             -- all char 0 fields have a canonical embedding of `ℚ` (used in `number_field`).
-             -- Show that these coincide:
-             ext1, simp [algebra.smul_def] } }
+  to_finite_dimensional :=
+    -- The vector space structure of `ℚ` over itself can arise in multiple ways:
+    -- all fields are vector spaces over themselves (used in `rat.finite_dimensional`)
+    -- all char 0 fields have a canonical embedding of `ℚ` (used in `number_field`).
+    -- Show that these coincide:
+    by convert (infer_instance : finite_dimensional ℚ ℚ), }
 
 /-- The ring of integers of `ℚ` as a number field is just `ℤ`. -/
 noncomputable def ring_of_integers_equiv : ring_of_integers ℚ ≃+* ℤ :=