diff --git a/src/algebra/algebra/subalgebra/basic.lean b/src/algebra/algebra/subalgebra/basic.lean index 78935fa347529..bca2395be81d4 100644 --- a/src/algebra/algebra/subalgebra/basic.lean +++ b/src/algebra/algebra/subalgebra/basic.lean @@ -37,7 +37,14 @@ variables [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [al include R instance : set_like (subalgebra R A) A := -⟨subalgebra.carrier, λ p q h, by cases p; cases q; congr'⟩ +{ coe := subalgebra.carrier, + coe_injective' := λ p q h, by cases p; cases q; congr' } + +instance : subsemiring_class (subalgebra R A) A := +{ add_mem := add_mem', + mul_mem := mul_mem', + one_mem := one_mem', + zero_mem := zero_mem' } @[simp] lemma mem_carrier {s : subalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s := iff.rfl @@ -101,6 +108,10 @@ S.to_subsemiring.zero_mem theorem add_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S := S.to_subsemiring.add_mem hx hy +instance {R A : Type*} [comm_ring R] [ring A] [algebra R A] : subring_class (subalgebra R A) A := +{ neg_mem := λ S x hx, neg_one_smul R x ▸ S.smul_mem hx _, + .. subalgebra.subsemiring_class } + 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 := neg_one_smul R x ▸ S.smul_mem hx _ diff --git a/src/algebra/lie/subalgebra.lean b/src/algebra/lie/subalgebra.lean index 1b59046670fe8..04847fe59df12 100644 --- a/src/algebra/lie/subalgebra.lean +++ b/src/algebra/lie/subalgebra.lean @@ -49,10 +49,20 @@ instance : has_zero (lie_subalgebra R L) := instance : inhabited (lie_subalgebra R L) := ⟨0⟩ instance : has_coe (lie_subalgebra R L) (submodule R L) := ⟨lie_subalgebra.to_submodule⟩ -instance : has_mem L (lie_subalgebra R L) := ⟨λ x L', x ∈ (L' : set L)⟩ namespace lie_subalgebra +open neg_mem_class + +instance : set_like (lie_subalgebra R L) L := +{ coe := λ L', L', + coe_injective' := λ L' L'' h, by { rcases L' with ⟨⟨⟩⟩, rcases L'' with ⟨⟨⟩⟩, congr' } } + +instance : add_subgroup_class (lie_subalgebra R L) L := +{ add_mem := λ L', L'.add_mem', + zero_mem := λ L', L'.zero_mem', + neg_mem := λ L' x hx, show -x ∈ (L' : submodule R L), from neg_mem hx } + /-- A Lie subalgebra forms a new Lie ring. -/ instance (L' : lie_subalgebra R L) : lie_ring L' := { bracket := λ x y, ⟨⁅x.val, y.val⁆, L'.lie_mem' x.property y.property⟩, @@ -119,10 +129,10 @@ lemma coe_zero_iff_zero (x : L') : (x : L) = 0 ↔ x = 0 := (ext_iff L' x 0).sym @[ext] lemma ext (L₁' L₂' : lie_subalgebra R L) (h : ∀ x, x ∈ L₁' ↔ x ∈ L₂') : L₁' = L₂' := -by { cases L₁', cases L₂', simp only [], ext x, exact h x, } +set_like.ext h lemma ext_iff' (L₁' L₂' : lie_subalgebra R L) : L₁' = L₂' ↔ ∀ x, x ∈ L₁' ↔ x ∈ L₂' := -⟨λ h x, by rw h, ext L₁' L₂'⟩ +set_like.ext_iff @[simp] lemma mk_coe (S : set L) (h₁ h₂ h₃ h₄) : ((⟨⟨S, h₁, h₂, h₃⟩, h₄⟩ : lie_subalgebra R L) : set L) = S := rfl @@ -132,12 +142,10 @@ lemma ext_iff' (L₁' L₂' : lie_subalgebra R L) : L₁' = L₂' ↔ ∀ x, x by { cases p, refl, } lemma coe_injective : function.injective (coe : lie_subalgebra R L → set L) := -by { rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ h, congr' } - -instance : set_like (lie_subalgebra R L) L := ⟨coe, coe_injective⟩ +set_like.coe_injective @[norm_cast] theorem coe_set_eq (L₁' L₂' : lie_subalgebra R L) : - (L₁' : set L) = L₂' ↔ L₁' = L₂' := coe_injective.eq_iff + (L₁' : set L) = L₂' ↔ L₁' = L₂' := set_like.coe_set_eq lemma to_submodule_injective : function.injective (coe : lie_subalgebra R L → submodule R L) := @@ -542,8 +550,8 @@ variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [li /-- An injective Lie algebra morphism is an equivalence onto its range. -/ noncomputable def of_injective (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) : L₁ ≃ₗ⁅R⁆ f.range := -{ map_lie' := λ x y, by { apply set_coe.ext, simpa, }, -..(linear_equiv.of_injective ↑f $ by rwa [lie_hom.coe_to_linear_map])} +{ map_lie' := λ x y, by { apply set_coe.ext, simpa }, + .. linear_equiv.of_injective (f : L₁ →ₗ[R] L₂) $ by rwa [lie_hom.coe_to_linear_map] } @[simp] lemma of_injective_apply (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) (x : L₁) : ↑(of_injective f h x) = f x := rfl diff --git a/src/algebra/lie/submodule.lean b/src/algebra/lie/submodule.lean index d4e9e841e8447..4553905a4376c 100644 --- a/src/algebra/lie/submodule.lean +++ b/src/algebra/lie/submodule.lean @@ -49,10 +49,17 @@ namespace lie_submodule variables {R L M} (N N' : lie_submodule R L M) +open neg_mem_class + instance : set_like (lie_submodule R L M) M := { coe := carrier, coe_injective' := λ N O h, by cases N; cases O; congr' } +instance : add_subgroup_class (lie_submodule R L M) M := +{ add_mem := λ N, N.add_mem', + zero_mem := λ N, N.zero_mem', + neg_mem := λ N x hx, show -x ∈ N.to_submodule, from neg_mem hx } + /-- The zero module is a Lie submodule of any Lie module. -/ instance : has_zero (lie_submodule R L M) := ⟨{ lie_mem := λ x m h, by { rw ((submodule.mem_bot R).1 h), apply lie_zero, }, diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean index 0ddcc4728b655..b21d63b6b6227 100644 --- a/src/algebra/module/submodule.lean +++ b/src/algebra/module/submodule.lean @@ -47,7 +47,12 @@ namespace submodule variables [semiring R] [add_comm_monoid M] [module R M] instance : set_like (submodule R M) M := -⟨submodule.carrier, λ p q h, by cases p; cases q; congr'⟩ +{ coe := submodule.carrier, + coe_injective' := λ p q h, by cases p; cases q; congr' } + +instance : add_submonoid_class (submodule R M) M := +{ zero_mem := zero_mem', + add_mem := add_mem' } @[simp] theorem mem_to_add_submonoid (p : submodule R M) (x : M) : x ∈ p.to_add_submonoid ↔ x ∈ p := iff.rfl @@ -282,7 +287,11 @@ variables {module_M : module R M} variables (p p' : submodule R M) variables {r : R} {x y : M} -lemma neg_mem (hx : x ∈ p) : -x ∈ p := p.to_sub_mul_action.neg_mem hx +instance [module R M] : add_subgroup_class (submodule R M) M := +{ neg_mem := λ p x, p.to_sub_mul_action.neg_mem, + .. submodule.add_submonoid_class } + +lemma neg_mem (hx : x ∈ p) : -x ∈ p := neg_mem_class.neg_mem hx /-- Reinterpret a submodule as an additive subgroup. -/ def to_add_subgroup : add_subgroup M := diff --git a/src/analysis/inner_product_space/l2_space.lean b/src/analysis/inner_product_space/l2_space.lean index c6383477da95c..107df8aeee86f 100644 --- a/src/analysis/inner_product_space/l2_space.lean +++ b/src/analysis/inner_product_space/l2_space.lean @@ -224,7 +224,6 @@ end protected lemma range_linear_isometry [Π i, complete_space (G i)] : hV.linear_isometry.to_linear_map.range = (⨆ i, (V i).to_linear_map.range).topological_closure := begin - classical, refine le_antisymm _ _, { rintros x ⟨f, rfl⟩, refine mem_closure_of_tendsto (hV.has_sum_linear_isometry f) (eventually_of_forall _), @@ -237,7 +236,7 @@ begin { refine supr_le _, rintros i x ⟨x, rfl⟩, use lp.single 2 i x, - convert hV.linear_isometry_apply_single _ }, + exact hV.linear_isometry_apply_single x }, exact hV.linear_isometry.isometry.uniform_inducing.is_complete_range.is_closed } end diff --git a/src/field_theory/galois.lean b/src/field_theory/galois.lean index ed2e07e4f0ac3..497234ffcc775 100644 --- a/src/field_theory/galois.lean +++ b/src/field_theory/galois.lean @@ -150,7 +150,7 @@ lemma alg_equiv.transfer_galois (f : E ≃ₐ[F] E') : is_galois F E ↔ is_galo ⟨λ h, by exactI is_galois.of_alg_equiv f, λ h, by exactI is_galois.of_alg_equiv f.symm⟩ lemma is_galois_iff_is_galois_top : is_galois F (⊤ : intermediate_field F E) ↔ is_galois F E := -(intermediate_field.top_equiv).transfer_galois +(intermediate_field.top_equiv : (⊤ : intermediate_field F E) ≃ₐ[F] E).transfer_galois instance is_galois_bot : is_galois F (⊥ : intermediate_field F E) := (intermediate_field.bot_equiv F E).transfer_galois.mpr (is_galois.self F) @@ -401,7 +401,8 @@ begin simp only [P] at *, rw [of_separable_splitting_field_aux hp K (multiset.mem_to_finset.mp hx), hK, finrank_mul_finrank], - exact (linear_equiv.finrank_eq (intermediate_field.lift2_alg_equiv K⟮x⟯).to_linear_equiv).symm, + symmetry, + exact linear_equiv.finrank_eq (alg_equiv.to_linear_equiv (intermediate_field.lift2_alg_equiv _)) end /--Equivalent characterizations of a Galois extension of finite degree-/ diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean index a665b8f471cf8..68e97d12e6564 100644 --- a/src/field_theory/intermediate_field.lean +++ b/src/field_theory/intermediate_field.lean @@ -61,6 +61,14 @@ def to_subfield : subfield L := { ..S.to_subalgebra, ..S } instance : set_like (intermediate_field K L) L := ⟨λ S, S.to_subalgebra.carrier, by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨h⟩, congr, }⟩ +instance : subfield_class (intermediate_field K L) L := +{ add_mem := λ s, s.add_mem', + zero_mem := λ s, s.zero_mem', + neg_mem := neg_mem', + mul_mem := λ s, s.mul_mem', + one_mem := λ s, s.one_mem', + inv_mem := inv_mem' } + @[simp] lemma mem_carrier {s : intermediate_field K L} {x : L} : x ∈ s.carrier ↔ x ∈ s := iff.rfl diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean index 2dfc1e6f948da..506c0169d97b6 100644 --- a/src/field_theory/subfield.lean +++ b/src/field_theory/subfield.lean @@ -63,6 +63,43 @@ universes u v w variables {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M] +/-- `subfield_class S K` states `S` is a type of subsets `s ⊆ K` closed under field operations. -/ +class subfield_class (S : Type*) (K : out_param $ Type*) [field K] [set_like S K] + extends subring_class S K, inv_mem_class S K. + +namespace subfield_class + +variables (S : Type*) [set_like S K] [h : subfield_class S K] +include h + +/-- A subfield contains `1`, products and inverses. + +Be assured that we're not actually proving that subfields are subgroups: +`subgroup_class` is really an abbreviation of `subgroup_with_or_without_zero_class`. + -/ +@[priority 100] -- See note [lower instance priority] +instance subfield_class.to_subgroup_class : subgroup_class S K := { .. h } + +/-- A subfield inherits a field structure -/ +@[priority 75] -- Prefer subclasses of `field` over subclasses of `subfield_class`. +instance to_field (s : S) : field s := +subtype.coe_injective.field (coe : s → K) + rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +omit h + +/-- A subfield of a `linear_ordered_field` is a `linear_ordered_field`. -/ +@[priority 75] -- Prefer subclasses of `field` over subclasses of `subfield_class`. +instance to_linear_ordered_field {K} [linear_ordered_field K] [set_like S K] + [subfield_class S K] (s : S) : + linear_ordered_field s := +subtype.coe_injective.linear_ordered_field coe + rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +end subfield_class + set_option old_structure_cmd true /-- `subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is a @@ -84,10 +121,17 @@ def to_add_subgroup (s : subfield K) : add_subgroup K := def to_submonoid (s : subfield K) : submonoid K := { ..s.to_subring.to_submonoid } - instance : set_like (subfield K) K := ⟨subfield.carrier, λ p q h, by cases p; cases q; congr'⟩ +instance : subfield_class (subfield K) K := +{ add_mem := add_mem', + zero_mem := zero_mem', + neg_mem := neg_mem', + mul_mem := mul_mem', + one_mem := one_mem', + inv_mem := inv_mem' } + @[simp] lemma mem_carrier {s : subfield K} {x : K} : x ∈ s.carrier ↔ x ∈ s := iff.rfl diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean index 28efd3d767905..5c852eb281647 100644 --- a/src/group_theory/subgroup/basic.lean +++ b/src/group_theory/subgroup/basic.lean @@ -89,6 +89,175 @@ open_locale big_operators pointwise variables {G : Type*} [group G] variables {A : Type*} [add_group A] +section subgroup_class + +/-- `inv_mem_class S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/ +class inv_mem_class (S G : Type*) [has_inv G] [set_like S G] := +(inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s) + +/-- `neg_mem_class S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/ +class neg_mem_class (S G : Type*) [has_neg G] [set_like S G] := +(neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s) + +/-- `subgroup_class S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/ +class subgroup_class (S G : Type*) [div_inv_monoid G] [set_like S G] + extends submonoid_class S G := +(inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s) + +/-- `add_subgroup_class S G` states `S` is a type of subsets `s ⊆ G` that are +additive subgroups of `G`. -/ +class add_subgroup_class (S G : Type*) [sub_neg_monoid G] [set_like S G] + extends add_submonoid_class S G := +(neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s) + +attribute [to_additive] inv_mem_class subgroup_class + +namespace subgroup_class + +variables (M S : Type*) [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M] +include hSM + +@[to_additive, priority 100] -- See note [lower instance priority] +instance to_inv_mem_class : inv_mem_class S M := +{ .. hSM } + +variables {S M} {H K : S} + +open mul_mem_class inv_mem_class submonoid_class + +/-- A subgroup is closed under division. -/ +@[to_additive "An additive subgroup is closed under subtraction."] +theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := +by rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy) + +@[to_additive] +lemma zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K +| (n : ℕ) := by { rw [zpow_coe_nat], exact pow_mem hx n } +| -[1+ n] := by { rw [zpow_neg_succ_of_nat], exact inv_mem (pow_mem hx n.succ) } + +omit hSM +variables [set_like S G] [hSG : subgroup_class S G] +include hSG + +@[simp, to_additive] theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H := +⟨λ h, inv_inv x ▸ inv_mem h, inv_mem⟩ + +@[to_additive] lemma div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H := +by rw [← inv_mem_iff, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv] + +@[simp, to_additive] +theorem inv_coe_set : (H : set G)⁻¹ = H := +by { ext, simp } + +@[simp, to_additive] +lemma exists_inv_mem_iff_exists_mem {P : G → Prop} : + (∃ (x : G), x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x := +by split; { rintros ⟨x, x_in, hx⟩, exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩ } + +@[to_additive] +lemma mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H := +⟨λ hba, by simpa using mul_mem hba (inv_mem h), λ hb, mul_mem hb h⟩ + +@[to_additive] +lemma mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H := +⟨λ hab, by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩ + +omit hSG +include hSM + +/-- A subgroup of a group inherits an inverse. -/ +@[to_additive "An additive subgroup of a `add_group` inherits an inverse."] +instance has_inv : has_inv H := ⟨λ a, ⟨a⁻¹, inv_mem a.2⟩⟩ + +/-- A subgroup of a group inherits a division -/ +@[to_additive "An additive subgroup of an `add_group` inherits a subtraction."] +instance has_div : has_div H := ⟨λ a b, ⟨a / b, div_mem a.2 b.2⟩⟩ + +omit hSM +/-- An additive subgroup of an `add_group` inherits an integer scaling. -/ +instance _root_.add_subgroup_class.has_zsmul {M S} [sub_neg_monoid M] [set_like S M] + [add_subgroup_class S M] {H : S} : has_scalar ℤ H := +⟨λ n a, ⟨n • a, add_subgroup_class.zsmul_mem a.2 n⟩⟩ +include hSM + +/-- A subgroup of a group inherits an integer power. -/ +@[to_additive] +instance has_zpow : has_pow H ℤ := ⟨λ a n, ⟨a ^ n, zpow_mem a.2 n⟩⟩ +@[simp, norm_cast, to_additive] lemma coe_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : M) := rfl +@[simp, norm_cast, to_additive] lemma coe_div (x y : H) : (↑(x / y) : M) = ↑x / ↑y := rfl + +omit hSM +variables (H) +include hSG + +/-- A subgroup of a group inherits a group structure. -/ +@[to_additive "An additive subgroup of an `add_group` inherits an `add_group` structure.", +priority 75] -- Prefer subclasses of `group` over subclasses of `subgroup_class`. +instance to_group : group H := +subtype.coe_injective.group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +omit hSG + +/-- A subgroup of a `comm_group` is a `comm_group`. -/ +@[to_additive "An additive subgroup of an `add_comm_group` is an `add_comm_group`.", +priority 75] -- Prefer subclasses of `comm_group` over subclasses of `subgroup_class`. +instance to_comm_group {G : Type*} [comm_group G] [set_like S G] [subgroup_class S G] : + comm_group H := +subtype.coe_injective.comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) + +/-- A subgroup of an `ordered_comm_group` is an `ordered_comm_group`. -/ +@[to_additive "An additive subgroup of an `add_ordered_comm_group` is an `add_ordered_comm_group`.", +priority 75] -- Prefer subclasses of `group` over subclasses of `subgroup_class`. +instance to_ordered_comm_group {G : Type*} [ordered_comm_group G] [set_like S G] + [subgroup_class S G] : ordered_comm_group H := +subtype.coe_injective.ordered_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) + +/-- A subgroup of a `linear_ordered_comm_group` is a `linear_ordered_comm_group`. -/ +@[to_additive "An additive subgroup of a `linear_ordered_add_comm_group` is a + `linear_ordered_add_comm_group`.", + priority 75] -- Prefer subclasses of `group` over subclasses of `subgroup_class`. +instance to_linear_ordered_comm_group {G : Type*} [linear_ordered_comm_group G] [set_like S G] + [subgroup_class S G] : linear_ordered_comm_group H := +subtype.coe_injective.linear_ordered_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) (λ _ _, rfl) + +include hSG + +/-- The natural group hom from a subgroup of group `G` to `G`. -/ +@[to_additive "The natural group hom from an additive subgroup of `add_group` `G` to `G`."] +def subtype : H →* G := ⟨coe, rfl, λ _ _, rfl⟩ + +@[simp, to_additive] theorem coe_subtype : (subtype H : H → G) = coe := rfl + +variables {H} + +@[simp, norm_cast, to_additive coe_smul] +lemma coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = x ^ n := +(subtype H : H →* G).map_pow _ _ + +@[simp, norm_cast, to_additive] lemma coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = x ^ n := +(subtype H : H →* G).map_zpow _ _ + +/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/ +@[to_additive "The inclusion homomorphism from a additive subgroup `H` contained in `K` to `K`."] +def inclusion {H K : S} (h : H ≤ K) : H →* K := +monoid_hom.mk' (λ x, ⟨x, h x.prop⟩) (λ ⟨a, ha⟩ ⟨b, hb⟩, rfl) + +@[simp, to_additive] +lemma coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := +by { cases a, simp only [inclusion, set_like.coe_mk, monoid_hom.mk'_apply] } + +@[simp, to_additive] +lemma subtype_comp_inclusion {H K : S} (hH : H ≤ K) : + (subtype K).comp (inclusion hH) = subtype H := +by { ext, simp only [monoid_hom.comp_apply, coe_subtype, coe_inclusion] } + +end subgroup_class + +end subgroup_class + set_option old_structure_cmd true /-- A subgroup of a group `G` is a subset containing 1, closed under multiplication @@ -114,7 +283,14 @@ namespace subgroup @[to_additive] instance : set_like (subgroup G) G := -⟨subgroup.carrier, λ p q h, by cases p; cases q; congr'⟩ +{ coe := subgroup.carrier, + coe_injective' := λ p q h, by cases p; cases q; congr' } + +@[to_additive] +instance : subgroup_class (subgroup G) G := +{ mul_mem := subgroup.mul_mem', + one_mem := subgroup.one_mem', + inv_mem := subgroup.inv_mem' } @[simp, to_additive] lemma mem_carrier {s : subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s := iff.rfl diff --git a/src/group_theory/submonoid/basic.lean b/src/group_theory/submonoid/basic.lean index 5557835709a1a..64bae1284a465 100644 --- a/src/group_theory/submonoid/basic.lean +++ b/src/group_theory/submonoid/basic.lean @@ -57,31 +57,90 @@ section non_assoc variables [mul_one_class M] {s : set M} variables [add_zero_class A] {t : set A} +/-- `one_mem_class S M` says `S` is a type of subsets `s ≤ M`, such that `1 ∈ s` for all `s`. -/ +class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] [set_like S M] := +(one_mem : ∀ (s : S), (1 : M) ∈ s) + +/-- `zero_mem_class S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`. -/ +class zero_mem_class (S : Type*) (M : out_param $ Type*) [has_zero M] [set_like S M] := +(zero_mem : ∀ (s : S), (0 : M) ∈ s) + +/-- `mul_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(*)` -/ +class mul_mem_class (S : Type*) (M : out_param $ Type*) [has_mul M] [set_like S M] := +(mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) + +/-- `add_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(+)` -/ +class add_mem_class (S : Type*) (M : out_param $ Type*) [has_add M] [set_like S M] := +(add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) + +export add_mem_class (add_mem) + +attribute [to_additive] one_mem_class mul_mem_class + +section + set_option old_structure_cmd true /-- A submonoid of a monoid `M` is a subset containing 1 and closed under multiplication. -/ structure submonoid (M : Type*) [mul_one_class M] extends subsemigroup M := (one_mem' : (1 : M) ∈ carrier) +end + /-- A submonoid of a monoid `M` can be considered as a subsemigroup of that monoid. -/ add_decl_doc submonoid.to_subsemigroup +/-- `submonoid_class S M` says `S` is a type of subsets `s ≤ M` that contain `1` +and are closed under `(*)` -/ +class submonoid_class (S : Type*) (M : out_param $ Type*) [mul_one_class M] [set_like S M] + extends mul_mem_class S M := +(one_mem : ∀ (s : S), (1 : M) ∈ s) + +section + +set_option old_structure_cmd true + /-- An additive submonoid of an additive monoid `M` is a subset containing 0 and closed under addition. -/ structure add_submonoid (M : Type*) [add_zero_class M] extends add_subsemigroup M := (zero_mem' : (0 : M) ∈ carrier) +end + /-- An additive submonoid of an additive monoid `M` can be considered as an additive subsemigroup of that additive monoid. -/ add_decl_doc add_submonoid.to_add_subsemigroup -attribute [to_additive] submonoid +/-- `add_submonoid_class S M` says `S` is a type of subsets `s ≤ M` that contain `0` +and are closed under `(+)` -/ +class add_submonoid_class (S : Type*) (M : out_param $ Type*) [add_zero_class M] [set_like S M] + extends add_mem_class S M := +(zero_mem : ∀ (s : S), (0 : M) ∈ s) + +attribute [to_additive] submonoid submonoid_class + +@[to_additive, priority 100] -- See note [lower instance priority] +instance submonoid_class.to_one_mem_class (S : Type*) (M : out_param $ Type*) [mul_one_class M] + [set_like S M] [h : submonoid_class S M] : one_mem_class S M := +{ ..h } + +@[to_additive] +lemma pow_mem {M} [monoid M] {A : Type*} [set_like A M] [submonoid_class A M] {S : A} {x : M} + (hx : x ∈ S) : ∀ (n : ℕ), x ^ n ∈ S +| 0 := by { rw pow_zero, exact one_mem_class.one_mem S } +| (n + 1) := by { rw pow_succ, exact mul_mem_class.mul_mem hx (pow_mem n) } namespace submonoid @[to_additive] instance : set_like (submonoid M) M := -⟨submonoid.carrier, λ p q h, by cases p; cases q; congr'⟩ +{ coe := submonoid.carrier, + coe_injective' := λ p q h, by cases p; cases q; congr' } + +@[to_additive] +instance : submonoid_class (submonoid M) M := +{ one_mem := submonoid.one_mem', + mul_mem := submonoid.mul_mem' } /-- See Note [custom simps projection] -/ @[to_additive " See Note [custom simps projection]"] diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index 48088e4456add..3ca8561687b5c 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/src/group_theory/submonoid/membership.lean @@ -34,17 +34,56 @@ submonoid, submonoids open_locale big_operators -variables {M : Type*} -variables {A : Type*} - -namespace submonoid +variables {M A B : Type*} section assoc -variables [monoid M] (S : submonoid M) +variables [monoid M] [set_like B M] [submonoid_class B M] {S : B} + +namespace submonoid_class @[simp, norm_cast, to_additive] theorem coe_list_prod (l : list S) : (l.prod : M) = (l.map coe).prod := -S.subtype.map_list_prod l +(submonoid_class.subtype S : _ →* M).map_list_prod l + +@[simp, norm_cast, to_additive] theorem coe_multiset_prod {M} [comm_monoid M] [set_like B M] + [submonoid_class B M] (m : multiset S) : (m.prod : M) = (m.map coe).prod := +(submonoid_class.subtype S : _ →* M).map_multiset_prod m + +@[simp, norm_cast, to_additive] theorem coe_finset_prod {ι M} [comm_monoid M] [set_like B M] + [submonoid_class B M] (f : ι → S) (s : finset ι) : + ↑(∏ i in s, f i) = (∏ i in s, f i : M) := +(submonoid_class.subtype S : _ →* M).map_prod f s + +/-- Product of a list of elements in a submonoid is in the submonoid. -/ +@[to_additive "Sum of a list of elements in an `add_submonoid` is in the `add_submonoid`."] +lemma list_prod_mem {l : list M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S := +by { lift l to list S using hl, rw ← coe_list_prod, exact l.prod.coe_prop } + +/-- Product of a multiset of elements in a submonoid of a `comm_monoid` is in the submonoid. -/ +@[to_additive "Sum of a multiset of elements in an `add_submonoid` of an `add_comm_monoid` is +in the `add_submonoid`."] +lemma multiset_prod_mem {M} [comm_monoid M] [set_like B M] [submonoid_class B M] (m : multiset M) + (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S := +by { lift m to multiset S using hm, rw ← coe_multiset_prod, exact m.prod.coe_prop } + +/-- Product of elements of a submonoid of a `comm_monoid` indexed by a `finset` is in the + submonoid. -/ +@[to_additive "Sum of elements in an `add_submonoid` of an `add_comm_monoid` indexed by a `finset` +is in the `add_submonoid`."] +lemma prod_mem {M : Type*} [comm_monoid M] [set_like B M] [submonoid_class B M] + {ι : Type*} {t : finset ι} {f : ι → M} (h : ∀c ∈ t, f c ∈ S) : + ∏ c in t, f c ∈ S := +multiset_prod_mem (t.1.map f) $ λ x hx, let ⟨i, hi, hix⟩ := multiset.mem_map.1 hx in hix ▸ h i hi + +end submonoid_class + +namespace submonoid + +variables (s : submonoid M) + +@[simp, norm_cast, to_additive] theorem coe_list_prod (l : list s) : + (l.prod : M) = (l.map coe).prod := +s.subtype.map_list_prod l @[simp, norm_cast, to_additive] theorem coe_multiset_prod {M} [comm_monoid M] (S : submonoid M) (m : multiset S) : (m.prod : M) = (m.map coe).prod := @@ -57,8 +96,8 @@ S.subtype.map_prod f s /-- Product of a list of elements in a submonoid is in the submonoid. -/ @[to_additive "Sum of a list of elements in an `add_submonoid` is in the `add_submonoid`."] -lemma list_prod_mem {l : list M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S := -by { lift l to list S using hl, rw ← coe_list_prod, exact l.prod.coe_prop } +lemma list_prod_mem {l : list M} (hl : ∀ x ∈ l, x ∈ s) : l.prod ∈ s := +by { lift l to list s using hl, rw ← coe_list_prod, exact l.prod.coe_prop } /-- Product of a multiset of elements in a submonoid of a `comm_monoid` is in the submonoid. -/ @[to_additive "Sum of a multiset of elements in an `add_submonoid` of an `add_comm_monoid` is @@ -98,13 +137,20 @@ begin exact h x hx, end +end submonoid + end assoc section non_assoc -variables [mul_one_class M] (S : submonoid M) +variables [mul_one_class M] open set +namespace submonoid + +-- TODO: this section can be generalized to `[submonoid_class B M] [complete_lattice B]` +-- such that `complete_lattice.le` coincides with `set_like.le` + @[to_additive] lemma mem_supr_of_directed {ι} [hι : nonempty ι] {S : ι → submonoid M} (hS : directed (≤) S) {x : M} : @@ -194,10 +240,10 @@ begin refine ⟨_, hmul _ _ _ _ Cx Cy⟩ }, end -end non_assoc - end submonoid +end non_assoc + namespace free_monoid variables {α : Type*} @@ -219,7 +265,7 @@ open monoid_hom lemma closure_singleton_eq (x : M) : closure ({x} : set M) = (powers_hom M x).mrange := closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, pow_one x⟩) $ - λ x ⟨n, hn⟩, hn ▸ pow_mem _ (subset_closure $ set.mem_singleton _) _ + λ x ⟨n, hn⟩, hn ▸ submonoid.pow_mem _ (subset_closure $ set.mem_singleton _) _ /-- The submonoid generated by an element of a monoid equals the set of natural number powers of the element. -/ diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean index eef35a646cc79..dca7f7c9d5413 100644 --- a/src/group_theory/submonoid/operations.lean +++ b/src/group_theory/submonoid/operations.lean @@ -378,6 +378,133 @@ lemma comap_strict_mono_of_surjective : strict_mono (comap f) := end galois_insertion +end submonoid + +namespace submonoid_class + +variables {A : Type*} [set_like A M] [hA : submonoid_class A M] (S' : A) +include hA + +open mul_mem_class + +/-- A submonoid of a monoid inherits a multiplication. -/ +@[to_additive "An `add_submonoid` of an `add_monoid` inherits an addition."] +instance has_mul : has_mul S' := ⟨λ a b, ⟨a.1 * b.1, mul_mem a.2 b.2⟩⟩ + +/-- A submonoid of a monoid inherits a 1. -/ +@[to_additive "An `add_submonoid` of an `add_monoid` inherits a zero."] +instance has_one : has_one S' := ⟨⟨_, one_mem S'⟩⟩ + +@[simp, norm_cast, to_additive] lemma coe_mul (x y : S') : (↑(x * y) : M) = ↑x * ↑y := rfl +@[simp, norm_cast, to_additive] lemma coe_one : ((1 : S') : M) = 1 := rfl + +variables {S'} +@[simp, norm_cast, to_additive] lemma coe_eq_one {x : S'} : (↑x : M) = 1 ↔ x = 1 := +(subtype.ext_iff.symm : (x : M) = (1 : S') ↔ x = 1) +variables (S') + +@[simp, to_additive] lemma mk_mul_mk (x y : M) (hx : x ∈ S') (hy : y ∈ S') : + (⟨x, hx⟩ : S') * ⟨y, hy⟩ = ⟨x * y, mul_mem hx hy⟩ := rfl + +@[to_additive] lemma mul_def (x y : S') : x * y = ⟨x * y, mul_mem x.2 y.2⟩ := rfl +@[to_additive] lemma one_def : (1 : S') = ⟨1, one_mem S'⟩ := rfl + +omit hA + +/-- An `add_submonoid` of an `add_monoid` inherits a scalar multiplication. -/ +instance _root_.add_submonoid_class.has_nsmul {M} [add_monoid M] {A : Type*} [set_like A M] + [add_submonoid_class A M] (S : A) : + has_scalar ℕ S := +⟨λ n a, ⟨n • a.1, nsmul_mem a.2 n⟩⟩ + +/-- A submonoid of a monoid inherits a power operator. -/ +instance has_pow {M} [monoid M] {A : Type*} [set_like A M] [submonoid_class A M] (S : A) : + has_pow S ℕ := +⟨λ a n, ⟨a.1 ^ n, pow_mem a.2 n⟩⟩ + +attribute [to_additive] submonoid_class.has_pow + +@[simp, norm_cast, to_additive] lemma coe_pow {M} [monoid M] {A : Type*} [set_like A M] + [submonoid_class A M] {S : A} (x : S) (n : ℕ) : + (↑(x ^ n) : M) = ↑x ^ n := +rfl + +@[simp, to_additive] lemma mk_pow {M} [monoid M] {A : Type*} [set_like A M] + [submonoid_class A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) : + (⟨x, hx⟩ : S) ^ n = ⟨x ^ n, pow_mem hx n⟩ := +rfl + +/-- A submonoid of a unital magma inherits a unital magma structure. -/ +@[to_additive "An `add_submonoid` of an unital additive magma inherits an unital additive magma +structure.", +priority 75] -- Prefer subclasses of `monoid` over subclasses of `submonoid_class`. +instance to_mul_one_class {M : Type*} [mul_one_class M] {A : Type*} [set_like A M] + [submonoid_class A M] (S : A) : mul_one_class S := +subtype.coe_injective.mul_one_class _ rfl (λ _ _, rfl) + +/-- A submonoid of a monoid inherits a monoid structure. -/ +@[to_additive "An `add_submonoid` of an `add_monoid` inherits an `add_monoid` +structure.", +priority 75] -- Prefer subclasses of `monoid` over subclasses of `submonoid_class`. +instance to_monoid {M : Type*} [monoid M] {A : Type*} [set_like A M] [submonoid_class A M] + (S : A) : monoid S := +subtype.coe_injective.monoid coe rfl (λ _ _, rfl) (λ _ _, rfl) + +/-- A submonoid of a `comm_monoid` is a `comm_monoid`. -/ +@[to_additive "An `add_submonoid` of an `add_comm_monoid` is +an `add_comm_monoid`.", +priority 75] -- Prefer subclasses of `monoid` over subclasses of `submonoid_class`. +instance to_comm_monoid {M} [comm_monoid M] {A : Type*} [set_like A M] [submonoid_class A M] + (S : A) : comm_monoid S := +subtype.coe_injective.comm_monoid coe rfl (λ _ _, rfl) (λ _ _, rfl) + +/-- A submonoid of an `ordered_comm_monoid` is an `ordered_comm_monoid`. -/ +@[to_additive "An `add_submonoid` of an `ordered_add_comm_monoid` is +an `ordered_add_comm_monoid`.", +priority 75] -- Prefer subclasses of `monoid` over subclasses of `submonoid_class`. +instance to_ordered_comm_monoid {M} [ordered_comm_monoid M] {A : Type*} [set_like A M] + [submonoid_class A M] (S : A) : ordered_comm_monoid S := +subtype.coe_injective.ordered_comm_monoid coe rfl (λ _ _, rfl) (λ _ _, rfl) + +/-- A submonoid of a `linear_ordered_comm_monoid` is a `linear_ordered_comm_monoid`. -/ +@[to_additive "An `add_submonoid` of a `linear_ordered_add_comm_monoid` is +a `linear_ordered_add_comm_monoid`.", +priority 75] -- Prefer subclasses of `monoid` over subclasses of `submonoid_class`. +instance to_linear_ordered_comm_monoid {M} [linear_ordered_comm_monoid M] {A : Type*} + [set_like A M] [submonoid_class A M] (S : A) : + linear_ordered_comm_monoid S := +subtype.coe_injective.linear_ordered_comm_monoid coe rfl (λ _ _, rfl) (λ _ _, rfl) + +/-- A submonoid of an `ordered_cancel_comm_monoid` is an `ordered_cancel_comm_monoid`. -/ +@[to_additive "An `add_submonoid` of an `ordered_cancel_add_comm_monoid` is +an `ordered_cancel_add_comm_monoid`.", +priority 75] -- Prefer subclasses of `monoid` over subclasses of `submonoid_class`. +instance to_ordered_cancel_comm_monoid {M} [ordered_cancel_comm_monoid M] {A : Type*} + [set_like A M] [submonoid_class A M] (S : A) : + ordered_cancel_comm_monoid S := +subtype.coe_injective.ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) (λ _ _, rfl) + +/-- A submonoid of a `linear_ordered_cancel_comm_monoid` is a `linear_ordered_cancel_comm_monoid`. +-/ +@[to_additive "An `add_submonoid` of a `linear_ordered_cancel_add_comm_monoid` is +a `linear_ordered_cancel_add_comm_monoid`.", +priority 75] -- Prefer subclasses of `monoid` over subclasses of `submonoid_class`. +instance to_linear_ordered_cancel_comm_monoid {M} [linear_ordered_cancel_comm_monoid M] + {A : Type*} [set_like A M] [submonoid_class A M] (S : A) : linear_ordered_cancel_comm_monoid S := +subtype.coe_injective.linear_ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) (λ _ _, rfl) + +include hA + +/-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/ +@[to_additive "The natural monoid hom from an `add_submonoid` of `add_monoid` `M` to `M`."] +def subtype : S' →* M := ⟨coe, rfl, λ _ _, rfl⟩ + +@[simp, to_additive] theorem coe_subtype : (submonoid_class.subtype S' : S' → M) = coe := rfl + +end submonoid_class + +namespace submonoid + /-- A submonoid of a monoid inherits a multiplication. -/ @[to_additive "An `add_submonoid` of an `add_monoid` inherits an addition."] instance has_mul : has_mul S := ⟨λ a b, ⟨a.1 * b.1, S.mul_mem a.2 b.2⟩⟩ @@ -403,11 +530,7 @@ subtype.coe_injective.mul_one_class coe rfl (λ _ _, rfl) @[to_additive] lemma pow_mem {M : Type*} [monoid M] (S : submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S := -begin - induction n with n ih, - { simpa only [pow_zero] using S.one_mem }, - { simpa only [pow_succ] using S.mul_mem hx ih } -end +pow_mem hx n instance _root_.add_submonoid.has_nsmul {M : Type*} [add_monoid M] (S : add_submonoid M) : has_scalar ℕ S := diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean index b254651f8f3fe..ef8665efcf2a4 100644 --- a/src/group_theory/sylow.lean +++ b/src/group_theory/sylow.lean @@ -67,6 +67,11 @@ instance : set_like (sylow p G) G := { coe := coe, coe_injective' := λ P Q h, ext (set_like.coe_injective h) } +instance : subgroup_class (sylow p G) G := +{ mul_mem := λ s, s.mul_mem', + one_mem := λ s, s.one_mem', + inv_mem := λ s, s.inv_mem' } + end sylow /-- A generalization of **Sylow's first theorem**. diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean index 81df6dd539fd1..347bd54990cf2 100644 --- a/src/measure_theory/function/lp_space.lean +++ b/src/measure_theory/function/lp_space.lean @@ -2598,7 +2598,7 @@ linear_map.mk_continuous variables {𝕜} lemma range_to_Lp [normed_field 𝕜] [normed_space 𝕜 E] [fact (1 ≤ p)] : - ((to_Lp p μ 𝕜).range.to_add_subgroup : add_subgroup (Lp E p μ)) + (((to_Lp p μ 𝕜).range : submodule 𝕜 (Lp E p μ)).to_add_subgroup) = measure_theory.Lp.bounded_continuous_function E p μ := range_to_Lp_hom p μ @@ -2631,7 +2631,7 @@ def to_Lp [normed_field 𝕜] [normed_space 𝕜 E] : variables {𝕜} lemma range_to_Lp [normed_field 𝕜] [normed_space 𝕜 E] : - ((to_Lp p μ 𝕜).range.to_add_subgroup : add_subgroup (Lp E p μ)) + ((to_Lp p μ 𝕜).range : submodule 𝕜 (Lp E p μ)).to_add_subgroup = measure_theory.Lp.bounded_continuous_function E p μ := begin refine set_like.ext' _, diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean index d1d924e9a1162..9248b158a2ac6 100644 --- a/src/measure_theory/integral/bochner.lean +++ b/src/measure_theory/integral/bochner.lean @@ -627,10 +627,10 @@ lemma integral_add (f g : α →₁[μ] E) : integral (f + g) = integral f + int map_add integral_clm f g lemma integral_neg (f : α →₁[μ] E) : integral (-f) = - integral f := -integral_clm.map_neg f +map_neg integral_clm f lemma integral_sub (f g : α →₁[μ] E) : integral (f - g) = integral f - integral g := -integral_clm.map_sub f g +map_sub integral_clm f g lemma integral_smul (c : 𝕜) (f : α →₁[μ] E) : integral (c • f) = c • integral f := map_smul (integral_clm' 𝕜) c f diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index a56ef1f4513ac..35aa49991fbd3 100644 --- a/src/ring_theory/jacobson.lean +++ b/src/ring_theory/jacobson.lean @@ -409,8 +409,8 @@ begin change (polynomial.map ((quotient.mk I).comp C).range_restrict f).coeff n = 0 at hf, rw [coeff_map, subtype.ext_iff] at hf, rwa [mem_comap, ← quotient.eq_zero_iff_mem, ← ring_hom.comp_apply], }, - haveI : (ideal.map (map_ring_hom i) I).is_prime := - map_is_prime_of_surjective (map_surjective i hi) hi', + haveI := map_is_prime_of_surjective + (show function.surjective (map_ring_hom i), from map_surjective i hi) hi', suffices : (I.map (polynomial.map_ring_hom i)).jacobson = (I.map (polynomial.map_ring_hom i)), { replace this := congr_arg (comap (polynomial.map_ring_hom i)) this, rw [← map_jacobson_of_surjective _ hi', diff --git a/src/ring_theory/norm.lean b/src/ring_theory/norm.lean index b81e391c6a4e3..298a66638e7ce 100644 --- a/src/ring_theory/norm.lean +++ b/src/ring_theory/norm.lean @@ -202,7 +202,7 @@ lemma _root_.intermediate_field.adjoin_simple.norm_gen_eq_prod_roots (x : L) (algebra_map K F) (norm K (adjoin_simple.gen K x)) = ((minpoly K x).map (algebra_map K F)).roots.prod := begin - have injKxL : function.injective (algebra_map K⟮x⟯ L) := ring_hom.injective _, + have injKxL := (algebra_map K⟮x⟯ L).injective, by_cases hx : _root_.is_integral K x, swap, { simp [minpoly.eq_zero hx, intermediate_field.adjoin_simple.norm_gen_eq_one hx] }, have hx' : _root_.is_integral K (adjoin_simple.gen K x), diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean index 8329e337bec05..6a91cbdb9da0c 100644 --- a/src/ring_theory/polynomial/basic.lean +++ b/src/ring_theory/polynomial/basic.lean @@ -526,7 +526,8 @@ begin obtain ⟨x, hx'⟩ := x, obtain ⟨y, rfl⟩ := (ring_hom.mem_range).1 hx', refine subtype.eq _, - simp only [ring_hom.comp_apply, quotient.eq_zero_iff_mem, subring.coe_zero, subtype.val_eq_coe], + simp only [ring_hom.comp_apply, quotient.eq_zero_iff_mem, add_submonoid_class.coe_zero, + subtype.val_eq_coe], suffices : C (i y) ∈ (I.map (polynomial.map_ring_hom i)), { obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (polynomial.map_ring_hom i) (polynomial.map_surjective _ (((quotient.mk I).comp C).range_restrict_surjective)) this, diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean index e1b15aacfe5de..52c3ea09c4e60 100644 --- a/src/ring_theory/roots_of_unity.lean +++ b/src/ring_theory/roots_of_unity.lean @@ -219,7 +219,7 @@ variables {k R} lemma map_root_of_unity_eq_pow_self [ring_hom_class F R R] (σ : F) (ζ : roots_of_unity k R) : ∃ m : ℕ, σ ζ = ζ ^ m := begin - obtain ⟨m, hm⟩ := (restrict_roots_of_unity σ k).map_cyclic, + obtain ⟨m, hm⟩ := monoid_hom.map_cyclic (restrict_roots_of_unity σ k), rw [←restrict_roots_of_unity_coe_apply, hm, zpow_eq_mod_order_of, ←int.to_nat_of_nonneg (m.mod_nonneg (int.coe_nat_ne_zero.mpr (pos_iff_ne_zero.mp (order_of_pos ζ)))), zpow_coe_nat, roots_of_unity.coe_pow], diff --git a/src/ring_theory/subring/basic.lean b/src/ring_theory/subring/basic.lean index 1c8492cf2460d..8dc75c2c58efa 100644 --- a/src/ring_theory/subring/basic.lean +++ b/src/ring_theory/subring/basic.lean @@ -65,7 +65,97 @@ subring, subrings open_locale big_operators universes u v w -variables {R : Type u} {S : Type v} {T : Type w} [ring R] [ring S] [ring T] +variables {R : Type u} {S : Type v} {T : Type w} [ring R] + +section subring_class + +/-- `subring_class S R` states that `S` is a type of subsets `s ⊆ R` that +are both a multiplicative submonoid and an additive subgroup. -/ +class subring_class (S : Type*) (R : out_param $ Type u) [ring R] [set_like S R] + extends subsemiring_class S R := +(neg_mem : ∀ {s : S} {a : R}, a ∈ s → -a ∈ s) + +@[priority 100] -- See note [lower instance priority] +instance subring_class.add_subgroup_class (S : Type*) (R : out_param $ Type u) [set_like S R] + [ring R] [h : subring_class S R] : add_subgroup_class S R := +{ .. h } + +variables [set_like S R] [hSR : subring_class S R] (s : S) +include hSR + +namespace subring_class + +open one_mem_class add_subgroup_class + +lemma coe_int_mem (n : ℤ) : (n : R) ∈ s := +by simp only [← zsmul_one, zsmul_mem, one_mem] + +/-- A subring of a ring inherits a ring structure -/ +@[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`. +instance to_ring : ring s := +{ right_distrib := λ x y z, subtype.eq $ right_distrib x y z, + left_distrib := λ x y z, subtype.eq $ left_distrib x y z, + .. submonoid_class.to_monoid s, .. add_subgroup_class.to_add_comm_group s } + +omit hSR +/-- A subring of a `comm_ring` is a `comm_ring`. -/ +@[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`. +instance to_comm_ring {R} [comm_ring R] [set_like S R] [subring_class S R] : comm_ring s := +subtype.coe_injective.comm_ring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +/-- A subring of a domain is a domain. -/ +@[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`. +instance {R} [ring R] [is_domain R] [set_like S R] [subring_class S R] : is_domain s := +{ .. subsemiring_class.nontrivial s, .. subsemiring_class.no_zero_divisors s } + +/-- A subring of an `ordered_ring` is an `ordered_ring`. -/ +@[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`. +instance to_ordered_ring {R} [ordered_ring R] [set_like S R] [subring_class S R] : + ordered_ring s := +subtype.coe_injective.ordered_ring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +/-- A subring of an `ordered_comm_ring` is an `ordered_comm_ring`. -/ +@[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`. +instance to_ordered_comm_ring {R} [ordered_comm_ring R] [set_like S R] [subring_class S R] : + ordered_comm_ring s := +subtype.coe_injective.ordered_comm_ring coe rfl rfl + (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +/-- A subring of a `linear_ordered_ring` is a `linear_ordered_ring`. -/ +@[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`. +instance to_linear_ordered_ring {R} [linear_ordered_ring R] [set_like S R] [subring_class S R] : + linear_ordered_ring s := +subtype.coe_injective.linear_ordered_ring coe rfl rfl + (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +/-- A subring of a `linear_ordered_comm_ring` is a `linear_ordered_comm_ring`. -/ +@[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`. +instance to_linear_ordered_comm_ring {R} [linear_ordered_comm_ring R] [set_like S R] + [subring_class S R] : linear_ordered_comm_ring s := +subtype.coe_injective.linear_ordered_comm_ring coe rfl rfl + (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +include hSR + +/-- The natural ring hom from a subring of ring `R` to `R`. -/ +def subtype (s : S) : s →+* R := +{ to_fun := coe, + .. submonoid_class.subtype s, + .. add_subgroup_class.subtype s } + +@[simp] theorem coe_subtype : (subtype s : s → R) = coe := rfl +@[simp, norm_cast] lemma coe_nat_cast (n : ℕ) : ((n : s) : R) = n := +map_nat_cast (subtype s) n +@[simp, norm_cast] lemma coe_int_cast (n : ℤ) : ((n : s) : R) = n := +(subtype s : s →+* R).map_int_cast n + +end subring_class + +end subring_class + +variables [ring S] [ring T] set_option old_structure_cmd true @@ -88,7 +178,15 @@ def to_submonoid (s : subring R) : submonoid R := ..s.to_subsemiring.to_submonoid } instance : set_like (subring R) R := -⟨subring.carrier, λ p q h, by cases p; cases q; congr'⟩ +{ coe := subring.carrier, + coe_injective' := λ p q h, by cases p; cases q; congr' } + +instance : subring_class (subring R) R := +{ zero_mem := zero_mem', + add_mem := add_mem', + one_mem := one_mem', + mul_mem := mul_mem', + neg_mem := neg_mem' } @[simp] lemma mem_carrier {s : subring R} {x : R} : x ∈ s.carrier ↔ x ∈ s := iff.rfl diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean index b90fe56d0dba4..a002c626b47f5 100644 --- a/src/ring_theory/subsemiring/basic.lean +++ b/src/ring_theory/subsemiring/basic.lean @@ -23,9 +23,98 @@ open_locale big_operators universes u v w -variables {R : Type u} {S : Type v} {T : Type w} - [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring T] - (M : submonoid R) +variables {R : Type u} {S : Type v} {T : Type w} [non_assoc_semiring R] (M : submonoid R) + +section subsemiring_class + +/-- `subsemiring_class S R` states that `S` is a type of subsets `s ⊆ R` that +are both a multiplicative and an additive submonoid. -/ +class subsemiring_class (S : Type*) (R : out_param $ Type u) [non_assoc_semiring R] [set_like S R] + extends submonoid_class S R := +(add_mem : ∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) +(zero_mem : ∀ (s : S), (0 : R) ∈ s) + +@[priority 100] -- See note [lower instance priority] +instance subsemiring_class.add_submonoid_class (S : Type*) (R : out_param $ Type u) + [non_assoc_semiring R] [set_like S R] [h : subsemiring_class S R] : + add_submonoid_class S R := +{ .. h } + +variables [set_like S R] [hSR : subsemiring_class S R] (s : S) +include hSR + +open one_mem_class add_submonoid_class + +namespace subsemiring_class + +lemma coe_nat_mem (n : ℕ) : (n : R) ∈ s := +by simp only [← nsmul_one, nsmul_mem, one_mem] + +/-- A subsemiring of a `non_assoc_semiring` inherits a `non_assoc_semiring` structure -/ +@[priority 75] -- Prefer subclasses of `non_assoc_semiring` over subclasses of `subsemiring_class`. +instance to_non_assoc_semiring : non_assoc_semiring s := +subtype.coe_injective.non_assoc_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +instance nontrivial [nontrivial R] : nontrivial s := +nontrivial_of_ne 0 1 $ λ H, zero_ne_one (congr_arg subtype.val H) + +instance no_zero_divisors [no_zero_divisors R] : no_zero_divisors s := +{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y h, + or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ subtype.ext_iff.mp h) + (λ h, or.inl $ subtype.eq h) (λ h, or.inr $ subtype.eq h) } + +/-- The natural ring hom from a subsemiring of semiring `R` to `R`. -/ +def subtype : s →+* R := +{ to_fun := coe, .. submonoid_class.subtype s, .. add_submonoid_class.subtype s } + +@[simp] theorem coe_subtype : (subtype s : s → R) = coe := rfl + +omit hSR + +/-- A subsemiring of a `semiring` is a `semiring`. -/ +@[priority 75] -- Prefer subclasses of `semiring` over subclasses of `subsemiring_class`. +instance to_semiring {R} [semiring R] [set_like S R] [subsemiring_class S R] : semiring s := +subtype.coe_injective.semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +@[simp, norm_cast] lemma coe_pow {R} [semiring R] [set_like S R] [subsemiring_class S R] + (x : s) (n : ℕ) : + ((x^n : s) : R) = (x^n : R) := +begin + induction n with n ih, + { simp, }, + { simp [pow_succ, ih], }, +end + +/-- A subsemiring of a `comm_semiring` is a `comm_semiring`. -/ +instance to_comm_semiring {R} [comm_semiring R] [set_like S R] [subsemiring_class S R] : + comm_semiring s := +subtype.coe_injective.comm_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + +/-- A subsemiring of an `ordered_semiring` is an `ordered_semiring`. -/ +instance to_ordered_semiring {R} [ordered_semiring R] [set_like S R] [subsemiring_class S R] : + ordered_semiring s := +subtype.coe_injective.ordered_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) + +/-- A subsemiring of an `ordered_comm_semiring` is an `ordered_comm_semiring`. -/ +instance to_ordered_comm_semiring {R} [ordered_comm_semiring R] [set_like S R] + [subsemiring_class S R] : ordered_comm_semiring s := +subtype.coe_injective.ordered_comm_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) + +/-- A subsemiring of a `linear_ordered_semiring` is a `linear_ordered_semiring`. -/ +instance to_linear_ordered_semiring {R} [linear_ordered_semiring R] [set_like S R] + [subsemiring_class S R] : linear_ordered_semiring s := +subtype.coe_injective.linear_ordered_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) + (λ _ _, rfl) + +/-! Note: currently, there is no `linear_ordered_comm_semiring`. -/ + +end subsemiring_class + +end subsemiring_class + +variables [non_assoc_semiring S] [non_assoc_semiring T] set_option old_structure_cmd true @@ -42,7 +131,14 @@ add_decl_doc subsemiring.to_add_submonoid namespace subsemiring instance : set_like (subsemiring R) R := -⟨subsemiring.carrier, λ p q h, by cases p; cases q; congr'⟩ +{ coe := subsemiring.carrier, + coe_injective' := λ p q h, by cases p; cases q; congr' } + +instance : subsemiring_class (subsemiring R) R := +{ zero_mem := zero_mem', + add_mem := add_mem', + one_mem := one_mem', + mul_mem := mul_mem' } @[simp] lemma mem_carrier {s : subsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s := iff.rfl diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean index 1088a71b2f397..657b938183d9e 100644 --- a/src/ring_theory/trace.lean +++ b/src/ring_theory/trace.lean @@ -239,8 +239,7 @@ lemma trace_gen_eq_sum_roots (x : L) algebra_map K F (trace K K⟮x⟯ (adjoin_simple.gen K x)) = ((minpoly K x).map (algebra_map K F)).roots.sum := begin - have injKKx : function.injective (algebra_map K K⟮x⟯) := ring_hom.injective _, - have injKxL : function.injective (algebra_map K⟮x⟯ L) := ring_hom.injective _, + have injKxL := (algebra_map K⟮x⟯ L).injective, by_cases hx : is_integral K x, swap, { simp [minpoly.eq_zero hx, trace_gen_eq_zero hx], }, have hx' : is_integral K (adjoin_simple.gen K x), diff --git a/src/tactic/lint/type_classes.lean b/src/tactic/lint/type_classes.lean index c8a778dacc12f..cd945a06fdc8c 100644 --- a/src/tactic/lint/type_classes.lean +++ b/src/tactic/lint/type_classes.lean @@ -257,7 +257,7 @@ Some instances take quite some time to fail, and we seem to run against the cach https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/odd.20repeated.20type.20class.20search -/ @[linter] meta def linter.fails_quickly : linter := -{ test := fails_quickly 15000, +{ test := fails_quickly 20000, auto_decls := tt, no_errors_found := "No type-class searches timed out.", errors_found := "TYPE CLASS SEARCHES TIMED OUT.