[Merged by Bors] - chore(algebra/algebra/subalgebra): Add missing coe_sort for subalgebra

src/algebra/algebra/subalgebra.lean

@@ -34,29 +34,33 @@ variables {R : Type u} {A : Type v} {B : Type w}
 variables [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B]
 include R
 
-instance : has_coe (subalgebra R A) (subsemiring A) :=
-⟨λ S, { ..S }⟩
+/- While we could add coercion aliases for `to_subsemiring` and `to_submodule`, they're not needed
+very often, harder to use than the projections themselves, and none of the other subobjects define
+that type of coercion. -/
+instance : has_coe_t (subalgebra R A) (set A) := ⟨λ s, s.carrier⟩
+instance : has_mem A (subalgebra R A) := ⟨λ x p, x ∈ (p : set A)⟩
+instance : has_coe_to_sort (subalgebra R A) := ⟨_, λ p, {x : A // x ∈ p}⟩
 
-instance : has_mem A (subalgebra R A) :=
-⟨λ x S, x ∈ (S : set A)⟩
+lemma coe_injective : function.injective (coe : subalgebra R A → set A) :=
+λ S T h, by cases S; cases T; congr'
 
-variables {A}
-theorem mem_coe {x : A} {s : subalgebra R A} : x ∈ (s : set A) ↔ x ∈ s :=
-iff.rfl
+@[simp]
+lemma mem_carrier {s : subalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s := iff.rfl
+
+@[simp] theorem mem_coe {s : subalgebra R A} {x : A} : x ∈ (s : set A) ↔ x ∈ s := iff.rfl
 
-@[ext] theorem ext {S T : subalgebra R A}
-  (h : ∀ x : A, x ∈ S ↔ x ∈ T) : S = T :=
-by cases S; cases T; congr; ext x; exact h x
+@[ext] theorem ext {S T : subalgebra R A} (h : ∀ x : A, x ∈ S ↔ x ∈ T) : S = T :=
+coe_injective $ set.ext h
 
-theorem ext_iff {S T : subalgebra R A} : S = T ↔ ∀ x : A, x ∈ S ↔ x ∈ T :=
-⟨λ h x, by rw h, ext⟩
+theorem ext_iff {S T : subalgebra R A} : S = T ↔ (∀ x : A, x ∈ S ↔ x ∈ T) :=
+coe_injective.eq_iff.symm.trans set.ext_iff
 
 variables (S : subalgebra R A)
 
 theorem algebra_map_mem (r : R) : algebra_map R A r ∈ S :=
 S.algebra_map_mem' r
 
-theorem srange_le : (algebra_map R A).srange ≤ S :=
+theorem srange_le : (algebra_map R A).srange ≤ S.to_subsemiring :=
 λ x ⟨r, _, hr⟩, hr ▸ S.algebra_map_mem r
 
 theorem range_subset : set.range (algebra_map R A) ⊆ S :=
@@ -66,22 +70,22 @@ theorem range_le : set.range (algebra_map R A) ≤ S :=
 S.range_subset
 
 theorem one_mem : (1 : A) ∈ S :=
-subsemiring.one_mem S
+S.to_subsemiring.one_mem
 
 theorem mul_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x * y ∈ S :=
-subsemiring.mul_mem S hx hy
+S.to_subsemiring.mul_mem hx hy
 
 theorem smul_mem {x : A} (hx : x ∈ S) (r : R) : r • x ∈ S :=
 (algebra.smul_def r x).symm ▸ S.mul_mem (S.algebra_map_mem r) hx
 
 theorem pow_mem {x : A} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S :=
-subsemiring.pow_mem S hx n
+S.to_subsemiring.pow_mem hx n
 
 theorem zero_mem : (0 : A) ∈ S :=
-subsemiring.zero_mem S
+S.to_subsemiring.zero_mem
 
 theorem add_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S :=
-subsemiring.add_mem S hx hy
+S.to_subsemiring.add_mem hx hy
 
 theorem neg_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) : -x ∈ S :=
@@ -92,40 +96,40 @@ theorem sub_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
 by simpa only [sub_eq_add_neg] using S.add_mem hx (S.neg_mem hy)
 
 theorem nsmul_mem {x : A} (hx : x ∈ S) (n : ℕ) : n •ℕ x ∈ S :=
-subsemiring.nsmul_mem S hx n
+S.to_subsemiring.nsmul_mem hx n
 
 theorem gsmul_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) (n : ℤ) : n •ℤ x ∈ S :=
 int.cases_on n (λ i, S.nsmul_mem hx i) (λ i, S.neg_mem $ S.nsmul_mem hx _)
 
 theorem coe_nat_mem (n : ℕ) : (n : A) ∈ S :=
-subsemiring.coe_nat_mem S n
+S.to_subsemiring.coe_nat_mem n
 
 theorem coe_int_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) (n : ℤ) : (n : A) ∈ S :=
 int.cases_on n (λ i, S.coe_nat_mem i) (λ i, S.neg_mem $ S.coe_nat_mem $ i + 1)
 
 theorem list_prod_mem {L : list A} (h : ∀ x ∈ L, x ∈ S) : L.prod ∈ S :=
-subsemiring.list_prod_mem S h
+S.to_subsemiring.list_prod_mem h
 
 theorem list_sum_mem {L : list A} (h : ∀ x ∈ L, x ∈ S) : L.sum ∈ S :=
-subsemiring.list_sum_mem S h
+S.to_subsemiring.list_sum_mem h
 
 theorem multiset_prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
   [algebra R A] (S : subalgebra R A) {m : multiset A} (h : ∀ x ∈ m, x ∈ S) : m.prod ∈ S :=
-subsemiring.multiset_prod_mem S m h
+S.to_subsemiring.multiset_prod_mem m h
 
 theorem multiset_sum_mem {m : multiset A} (h : ∀ x ∈ m, x ∈ S) : m.sum ∈ S :=
-subsemiring.multiset_sum_mem S m h
+S.to_subsemiring.multiset_sum_mem m h
 
 theorem prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
   [algebra R A] (S : subalgebra R A) {ι : Type w} {t : finset ι} {f : ι → A}
   (h : ∀ x ∈ t, f x ∈ S) : ∏ x in t, f x ∈ S :=
-subsemiring.prod_mem S h
+S.to_subsemiring.prod_mem h
 
 theorem sum_mem {ι : Type w} {t : finset ι} {f : ι → A}
   (h : ∀ x ∈ t, f x ∈ S) : ∑ x in t, f x ∈ S :=
-subsemiring.sum_mem S h
+S.to_subsemiring.sum_mem h
 
 instance {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A]
   (S : subalgebra R A) : is_add_submonoid (S : set A) :=
@@ -147,7 +151,7 @@ instance {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : sub
   is_subring (S : set A) :=
 { neg_mem := λ _, S.neg_mem }
 
-instance : inhabited S := ⟨0⟩
+instance : inhabited S := ⟨(0 : S.to_subsemiring)⟩
 
 section
 
@@ -171,7 +175,7 @@ instance to_ordered_semiring {R A}
   ordered_semiring S := S.to_subsemiring.to_ordered_semiring
 instance to_ordered_comm_semiring {R A}
   [comm_semiring R] [ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
-  ordered_comm_semiring S := subsemiring.to_ordered_comm_semiring S
+  ordered_comm_semiring S := S.to_subsemiring.to_ordered_comm_semiring
 instance to_ordered_ring {R A}
   [comm_ring R] [ordered_ring A] [algebra R A] (S : subalgebra R A) :
   ordered_ring S := S.to_subring.to_ordered_ring
@@ -196,14 +200,14 @@ instance algebra : algebra R S :=
 { smul := λ (c:R) x, ⟨c • x.1, S.smul_mem x.2 c⟩,
   commutes' := λ c x, subtype.eq $ algebra.commutes _ _,
   smul_def' := λ c x, subtype.eq $ algebra.smul_def _ _,
-  .. (algebra_map R A).cod_srestrict S $ λ x, S.range_le ⟨x, rfl⟩ }
+  .. (algebra_map R A).cod_srestrict S.to_subsemiring $ λ x, S.range_le ⟨x, rfl⟩ }
 
 instance to_algebra {R A B : Type*} [comm_semiring R] [comm_semiring A] [semiring B]
   [algebra R A] [algebra A B] (A₀ : subalgebra R A) : algebra A₀ B :=
-algebra.of_subsemiring A₀
+algebra.of_subsemiring A₀.to_subsemiring
 
 instance nontrivial [nontrivial A] : nontrivial S :=
-subsemiring.nontrivial S
+S.to_subsemiring.nontrivial
 
 instance no_zero_smul_divisors_bot [no_zero_smul_divisors R A] : no_zero_smul_divisors R S :=
 ⟨λ c x h,
@@ -254,22 +258,20 @@ def to_submodule : submodule R A :=
   smul_mem' := λ c x hx, (algebra.smul_def c x).symm ▸
     (⟨algebra_map R A c, S.range_le ⟨c, rfl⟩⟩ * ⟨x, hx⟩:S).2 }
 
-instance coe_to_submodule : has_coe (subalgebra R A) (submodule R A) :=
-⟨to_submodule⟩
-
 instance to_submodule.is_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
-  (S : subalgebra R A) : is_subring ((S : submodule R A) : set A) := S.is_subring
+  (S : subalgebra R A) : is_subring (S.to_submodule : set A) := S.is_subring
 
-@[simp] lemma mem_to_submodule {x} : x ∈ (S : submodule R A) ↔ x ∈ S := iff.rfl
+@[simp] lemma mem_to_submodule {x} : x ∈ S.to_submodule ↔ x ∈ S := iff.rfl
 
-theorem to_submodule_injective {S U : subalgebra R A} (h : (S : submodule R A) = U) : S = U :=
-ext $ λ x, by rw [← mem_to_submodule, ← mem_to_submodule, h]
+theorem to_submodule_injective :
+  function.injective (to_submodule : subalgebra R A → submodule R A) :=
+λ S T h, ext $ λ x, by rw [← mem_to_submodule, ← mem_to_submodule, h]
 
-theorem to_submodule_inj {S U : subalgebra R A} : (S : submodule R A) = U ↔ S = U :=
-⟨to_submodule_injective, congr_arg _⟩
+theorem to_submodule_inj {S U : subalgebra R A} : S.to_submodule = U.to_submodule ↔ S = U :=
+to_submodule_injective.eq_iff
 
 /-- As submodules, subalgebras are idempotent. -/
-@[simp] theorem mul_self : (S : submodule R A) * (S : submodule R A) = (S : submodule R A) :=
+@[simp] theorem mul_self : S.to_submodule * S.to_submodule = S.to_submodule :=
 begin
   apply le_antisymm,
   { rw submodule.mul_le,
@@ -282,14 +284,14 @@ end
 
 /-- Linear equivalence between `S : submodule R A` and `S`. Though these types are equal,
 we define it as a `linear_equiv` to avoid type equalities. -/
-def to_submodule_equiv (S : subalgebra R A) : (S : submodule R A) ≃ₗ[R] S :=
+def to_submodule_equiv (S : subalgebra R A) : S.to_submodule ≃ₗ[R] S :=
 linear_equiv.of_eq _ _ rfl
 
 instance : partial_order (subalgebra R A) :=
-{ le := λ S T, (S : set A) ⊆ (T : set A),
-  le_refl := λ S, set.subset.refl S,
-  le_trans := λ _ _ _, set.subset.trans,
-  le_antisymm := λ S T hst hts, ext $ λ x, ⟨@hst x, @hts x⟩ }
+{ le := λ p q, ∀ ⦃x⦄, x ∈ p → x ∈ q,
+  ..partial_order.lift (coe : subalgebra R A → set A) coe_injective }
+
+lemma le_def {p q : subalgebra R A} : p ≤ q ↔ (p : set A) ⊆ q := iff.rfl
 
 /-- Reinterpret an `S`-subalgebra as an `R`-subalgebra in `comap R S A`. -/
 def comap {R : Type u} {S : Type v} {A : Type w}
@@ -309,13 +311,13 @@ def under {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
 /-- Transport a subalgebra via an algebra homomorphism. -/
 def map (S : subalgebra R A) (f : A →ₐ[R] B) : subalgebra R B :=
 { algebra_map_mem' := λ r, f.commutes r ▸ set.mem_image_of_mem _ (S.algebra_map_mem r),
-  .. subsemiring.map (f : A →+* B) S,}
+  .. S.to_subsemiring.map (f : A →+* B) }
 
 /-- Preimage of a subalgebra under an algebra homomorphism. -/
 def comap' (S : subalgebra R B) (f : A →ₐ[R] B) : subalgebra R A :=
 { algebra_map_mem' := λ r, show f (algebra_map R A r) ∈ S,
     from (f.commutes r).symm ▸ S.algebra_map_mem r,
-  .. subsemiring.comap (f : A →+* B) S,}
+  .. S.to_subsemiring.comap (f : A →+* B) }
 
 lemma map_mono {S₁ S₂ : subalgebra R A} {f : A →ₐ[R] B} :
   S₁ ≤ S₂ → S₁.map f ≤ S₂.map f :=
@@ -327,7 +329,7 @@ set.image_subset_iff
 
 lemma map_injective {S₁ S₂ : subalgebra R A} (f : A →ₐ[R] B)
   (hf : function.injective f) (ih : S₁.map f = S₂.map f) : S₁ = S₂ :=
-ext $ set.ext_iff.1 $ set.image_injective.2 hf $ set.ext $ ext_iff.1 ih
+ext $ set.ext_iff.1 $ set.image_injective.2 hf $ set.ext $ ext_iff.mp ih
 
 lemma mem_map {S : subalgebra R A} {f : A →ₐ[R] B} {y : B} :
   y ∈ map S f ↔ ∃ x ∈ S, f x = y :=
@@ -372,7 +374,7 @@ by { ext, rw [subalgebra.mem_coe, mem_range], refl }
 /-- Restrict the codomain of an algebra homomorphism. -/
 def cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) : A →ₐ[R] S :=
 { commutes' := λ r, subtype.eq $ f.commutes r,
-  .. ring_hom.cod_srestrict (f : A →+* B) S hf }
+  .. ring_hom.cod_srestrict (f : A →+* B) S.to_subsemiring hf }
 
 @[simp] lemma val_comp_cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) :
   S.val.comp (f.cod_restrict S hf) = f :=
@@ -468,7 +470,8 @@ variables {R}
 
 protected lemma gc : galois_connection (adjoin R : set A → subalgebra R A) coe :=
 λ s S, ⟨λ H, le_trans (le_trans (set.subset_union_right _ _) subsemiring.subset_closure) H,
-λ H, subsemiring.closure_le.2 $ set.union_subset S.range_subset H⟩
+λ H, show subsemiring.closure (set.range (algebra_map R A) ∪ s) ≤ S.to_subsemiring,
+     from subsemiring.closure_le.2 $ set.union_subset S.range_subset H⟩
 
 /-- Galois insertion between `adjoin` and `coe`. -/
 protected def gi : galois_insertion (adjoin R : set A → subalgebra R A) coe :=
@@ -484,16 +487,16 @@ instance : inhabited (subalgebra R A) := ⟨⊥⟩
 
 theorem mem_bot {x : A} : x ∈ (⊥ : subalgebra R A) ↔ x ∈ set.range (algebra_map R A) :=
 suffices (of_id R A).range = (⊥ : subalgebra R A),
-by { rw [← this, ← subalgebra.mem_coe, alg_hom.coe_range], refl },
+by { rw [← this, ←subalgebra.mem_coe, alg_hom.coe_range], refl },
 le_bot_iff.mp (λ x hx, subalgebra.range_le _ ((of_id R A).coe_range ▸ hx))
 
-theorem to_submodule_bot : ((⊥ : subalgebra R A) : submodule R A) = R ∙ 1 :=
+theorem to_submodule_bot : (⊥ : subalgebra R A).to_submodule = R ∙ 1 :=
 by { ext x, simp [mem_bot, -set.singleton_one, submodule.mem_span_singleton, algebra.smul_def] }
 
 @[simp] theorem mem_top {x : A} : x ∈ (⊤ : subalgebra R A) :=
 subsemiring.subset_closure $ or.inr trivial
 
-@[simp] theorem coe_top : ((⊤ : subalgebra R A) : submodule R A) = ⊤ :=
+@[simp] theorem coe_top : (⊤ : subalgebra R A).to_submodule = ⊤ :=
 submodule.ext $ λ x, iff_of_true mem_top trivial
 
 @[simp] theorem coe_bot : ((⊥ : subalgebra R A) : set A) = set.range (algebra_map R A) :=
@@ -590,7 +593,7 @@ instance : unique (subalgebra R R) :=
   begin
     intro S,
     refine le_antisymm (λ r hr, _) bot_le,
-    simp only [set.mem_range, coe_bot, id.map_eq_self, exists_apply_eq_apply, default],
+    simp only [set.mem_range, mem_bot, id.map_eq_self, exists_apply_eq_apply, default],
   end
   .. algebra.subalgebra.inhabited }
 

src/field_theory/adjoin.lean

@@ -314,7 +314,7 @@ begin
   rw mul_inv_cancel (mt (λ key, _) h),
   rw ← ϕ.map_zero at key,
   change ↑(⟨x, hx⟩ : algebra.adjoin F {α}) = _,
-  rw [ϕ.injective key, submodule.coe_zero]
+  rw [ϕ.injective key, subalgebra.coe_zero]
 end
 
 end adjoin_simple

src/field_theory/intermediate_field.lean

@@ -345,8 +345,7 @@ by { rw [subalgebra.ext_iff, intermediate_field.ext'_iff, set.ext_iff], refl }
 
 lemma eq_of_le_of_findim_le [finite_dimensional K L] (h_le : F ≤ E)
   (h_findim : findim K E ≤ findim K F) : F = E :=
-intermediate_field.ext'_iff.mpr (submodule.ext'_iff.mp (eq_of_le_of_findim_le
-  (show F.to_subalgebra.to_submodule ≤ E.to_subalgebra.to_submodule, by exact h_le) h_findim))
+to_subalgebra_injective $ subalgebra.to_submodule_injective $ eq_of_le_of_findim_le h_le h_findim
 
 lemma eq_of_le_of_findim_eq [finite_dimensional K L] (h_le : F ≤ E)
   (h_findim : findim K F = findim K E) : F = E :=

src/field_theory/splitting_field.lean

@@ -451,9 +451,11 @@ alg_equiv.symm $ alg_equiv.of_bijective
 
 open finset
 
--- Speed up the following proof.
-local attribute [irreducible] minpoly
--- TODO: Why is this so slow?
+/-- If a `subalgebra` is finite_dimensional as a submodule then it is `finite_dimensional`. -/
+lemma finite_dimensional.of_subalgebra_to_submodule
+  {K V : Type*} [field K] [ring V] [algebra K V] {s : subalgebra K V}
+  (h : finite_dimensional K s.to_submodule) : finite_dimensional K s := h
+
 /-- If `K` and `L` are field extensions of `F` and we have `s : finset K` such that
 the minimal polynomial of each `x ∈ s` splits in `L` then `algebra.adjoin F s` embeds in `L`. -/
 theorem lift_of_splits {F K L : Type*} [field F] [field K] [field L]
@@ -468,8 +470,9 @@ begin
   choose H3 H4 using H3,
   rw [coe_insert, set.insert_eq, set.union_comm, algebra.adjoin_union],
   letI := (f : algebra.adjoin F (↑s : set K) →+* L).to_algebra,
-  haveI : finite_dimensional F (algebra.adjoin F (↑s : set K)) :=
-    (submodule.fg_iff_finite_dimensional _).1 (fg_adjoin_of_finite (set.finite_mem_finset s) H3),
+  haveI : finite_dimensional F (algebra.adjoin F (↑s : set K)) := (
+    (submodule.fg_iff_finite_dimensional _).1
+      (fg_adjoin_of_finite (set.finite_mem_finset s) H3)).of_subalgebra_to_submodule,
   letI := field_of_finite_dimensional F (algebra.adjoin F (↑s : set K)),
   have H5 : is_integral (algebra.adjoin F (↑s : set K)) a := is_integral_of_is_scalar_tower a H1,
   have H6 : (minpoly (algebra.adjoin F (↑s : set K)) a).splits
@@ -706,7 +709,7 @@ theorem splits_iff (f : polynomial K) [is_splitting_field K L f] :
 ⟨λ h, eq_bot_iff.2 $ adjoin_roots L f ▸ (roots_map (algebra_map K L) h).symm ▸
   algebra.adjoin_le_iff.2 (λ y hy,
     let ⟨x, hxs, hxy⟩ := finset.mem_image.1 (by rwa multiset.to_finset_map at hy) in
-    hxy ▸ subalgebra.algebra_map_mem _ _),
+    hxy ▸ subalgebra.mem_coe.2 $ subalgebra.algebra_map_mem _ _),
  λ h, @ring_equiv.to_ring_hom_refl K _ ▸
   ring_equiv.trans_symm (ring_equiv.of_bijective _ $ algebra.bijective_algebra_map_iff.2 h) ▸
   by { rw ring_equiv.to_ring_hom_trans, exact splits_comp_of_splits _ _ (splits L f) }⟩

src/linear_algebra/finite_dimensional.lean

@@ -1187,7 +1187,8 @@ variables {F E : Type*} [field F] [field E] [algebra F E]
 lemma subalgebra.dim_eq_one_of_eq_bot {S : subalgebra F E} (h : S = ⊥) : dim F S = 1 :=
 begin
   rw [← S.to_submodule_equiv.dim_eq, h,
-    (linear_equiv.of_eq ↑(⊥ : subalgebra F E) _ algebra.to_submodule_bot).dim_eq, dim_span_set],
+    (linear_equiv.of_eq (⊥ : subalgebra F E).to_submodule _ algebra.to_submodule_bot).dim_eq,
+    dim_span_set],
   exacts [mk_singleton _, linear_independent_singleton one_ne_zero]
 end
 
@@ -1232,7 +1233,7 @@ begin
   obtain ⟨_, b_spans⟩ := set_is_basis_of_linear_independent_of_card_eq_findim
     b_lin_ind (by simp only [*, set.to_finset_card]),
   intros x hx,
-  rw [subalgebra.mem_coe, algebra.mem_bot],
+  rw [algebra.mem_bot],
   have x_in_span_b : (⟨x, hx⟩ : S) ∈ submodule.span F b,
   { rw subtype.range_coe at b_spans,
     rw b_spans,