diff --git a/src/algebra/big_operators.lean b/src/algebra/big_operators.lean index c1e8c097f7f60..4ed90bfdf05ca 100644 --- a/src/algebra/big_operators.lean +++ b/src/algebra/big_operators.lean @@ -29,23 +29,22 @@ namespace finset variables {s s₁ s₂ : finset α} {a : α} {f g : α → β} /-- `prod s f` is the product of `f x` as `x` ranges over the elements of the finite set `s`. -/ -@[to_additive finset.sum] +@[to_additive] protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := (s.1.map f).prod -attribute [to_additive finset.sum.equations._eqn_1] finset.prod.equations._eqn_1 -@[to_additive finset.sum_eq_fold] +@[to_additive] theorem prod_eq_fold [comm_monoid β] (s : finset α) (f : α → β) : s.prod f = s.fold (*) 1 f := rfl section comm_monoid variables [comm_monoid β] -@[simp, to_additive finset.sum_empty] +@[simp, to_additive] lemma prod_empty {α : Type u} {f : α → β} : (∅:finset α).prod f = 1 := rfl -@[simp, to_additive finset.sum_insert] +@[simp, to_additive] lemma prod_insert [decidable_eq α] : a ∉ s → (insert a s).prod f = f a * s.prod f := fold_insert -@[simp, to_additive finset.sum_singleton] +@[simp, to_additive] lemma prod_singleton : (singleton a).prod f = f a := eq.trans fold_singleton $ mul_one _ @@ -53,36 +52,36 @@ eq.trans fold_singleton $ mul_one _ by simp only [finset.prod, multiset.map_const, multiset.prod_repeat, one_pow] @[simp] lemma sum_const_zero {β} {s : finset α} [add_comm_monoid β] : s.sum (λx, (0 : β)) = 0 := @prod_const_one _ (multiplicative β) _ _ -attribute [to_additive finset.sum_const_zero] prod_const_one +attribute [to_additive] prod_const_one -@[simp, to_additive finset.sum_image] +@[simp, to_additive] lemma prod_image [decidable_eq α] {s : finset γ} {g : γ → α} : (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).prod f = s.prod (λx, f (g x)) := fold_image -@[simp, to_additive sum_map] +@[simp, to_additive] lemma prod_map (s : finset α) (e : α ↪ γ) (f : γ → β) : (s.map e).prod f = s.prod (λa, f (e a)) := by rw [finset.prod, finset.map_val, multiset.map_map]; refl -@[congr, to_additive finset.sum_congr] +@[congr, to_additive] lemma prod_congr (h : s₁ = s₂) : (∀x∈s₂, f x = g x) → s₁.prod f = s₂.prod g := by rw [h]; exact fold_congr attribute [congr] finset.sum_congr -@[to_additive finset.sum_union_inter] +@[to_additive] lemma prod_union_inter [decidable_eq α] : (s₁ ∪ s₂).prod f * (s₁ ∩ s₂).prod f = s₁.prod f * s₂.prod f := fold_union_inter -@[to_additive finset.sum_union] +@[to_additive] lemma prod_union [decidable_eq α] (h : s₁ ∩ s₂ = ∅) : (s₁ ∪ s₂).prod f = s₁.prod f * s₂.prod f := by rw [←prod_union_inter, h]; exact (mul_one _).symm -@[to_additive finset.sum_sdiff] +@[to_additive] lemma prod_sdiff [decidable_eq α] (h : s₁ ⊆ s₂) : (s₂ \ s₁).prod f * s₁.prod f = s₂.prod f := by rw [←prod_union (sdiff_inter_self _ _), sdiff_union_of_subset h] -@[to_additive finset.sum_bind] +@[to_additive] lemma prod_bind [decidable_eq α] {s : finset γ} {t : γ → finset α} : (∀x∈s, ∀y∈s, x ≠ y → t x ∩ t y = ∅) → (s.bind t).prod f = s.prod (λx, (t x).prod f) := by haveI := classical.dec_eq γ; exact @@ -99,7 +98,7 @@ finset.induction_on s (λ _, by simp only [bind_empty, prod_empty]) _ (mem_inter_of_mem h₁ hy₂), by simp only [bind_insert, prod_insert hxs, prod_union this, ih hd']) -@[to_additive finset.sum_product] +@[to_additive] lemma prod_product {s : finset γ} {t : finset α} {f : γ×α → β} : (s.product t).prod f = s.prod (λx, t.prod $ λy, f (x, y)) := begin @@ -109,7 +108,7 @@ begin simp only [mem_inter, mem_image], rintro ⟨_, _⟩ ⟨⟨_, _, _⟩, ⟨_, _, _⟩⟩, apply h, cc end -@[to_additive finset.sum_sigma] +@[to_additive] lemma prod_sigma {σ : α → Type*} {s : finset α} {t : Πa, finset (σ a)} {f : sigma σ → β} : (s.sigma t).prod f = s.prod (λa, (t a).prod $ λs, f ⟨a, s⟩) := @@ -123,7 +122,7 @@ calc (s.sigma t).prod f = ... = (s.prod $ λa, (t a).prod $ λs, f ⟨a, s⟩) : prod_congr rfl $ λ _ _, prod_image $ λ _ _ _ _ _, by cc -@[to_additive finset.sum_image'] +@[to_additive] lemma prod_image' [decidable_eq α] {s : finset γ} {g : γ → α} (h : γ → β) (eq : ∀c∈s, f (g c) = (s.filter (λc', g c' = g c)).prod h) : (s.image g).prod f = s.prod h := @@ -142,11 +141,11 @@ begin exact mt (congr_arg g) ne end -@[to_additive finset.sum_add_distrib] +@[to_additive] lemma prod_mul_distrib : s.prod (λx, f x * g x) = s.prod f * s.prod g := eq.trans (by rw one_mul; refl) fold_op_distrib -@[to_additive finset.sum_comm] +@[to_additive] lemma prod_comm [decidable_eq γ] {s : finset γ} {t : finset α} {f : γ → α → β} : s.prod (λx, t.prod $ f x) = t.prod (λy, s.prod $ λx, f x y) := finset.induction_on s (by simp only [prod_empty, prod_const_one]) $ @@ -155,7 +154,7 @@ finset.induction_on s (by simp only [prod_empty, prod_const_one]) $ lemma prod_hom [comm_monoid γ] (g : β → γ) [is_monoid_hom g] : s.prod (λx, g (f x)) = g (s.prod f) := eq.trans (by rw is_monoid_hom.map_one g; refl) (fold_hom $ is_monoid_hom.map_mul g) -@[to_additive finset.sum_hom_rel] +@[to_additive] lemma prod_hom_rel [comm_monoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : finset α} (h₁ : r 1 1) (h₂ : ∀a b c, r b c → r (f a * b) (g a * c)) : r (s.prod f) (s.prod g) := begin @@ -165,14 +164,14 @@ begin exact h₂ a (s.prod f) (s.prod g) ih, end -@[to_additive finset.sum_subset] +@[to_additive] lemma prod_subset (h : s₁ ⊆ s₂) (hf : ∀x∈s₂, x ∉ s₁ → f x = 1) : s₁.prod f = s₂.prod f := by haveI := classical.dec_eq α; exact have (s₂ \ s₁).prod f = (s₂ \ s₁).prod (λx, 1), from prod_congr rfl $ by simpa only [mem_sdiff, and_imp], by rw [←prod_sdiff h]; simp only [this, prod_const_one, one_mul] -@[to_additive sum_filter] +@[to_additive] lemma prod_filter (p : α → Prop) [decidable_pred p] (f : α → β) : (s.filter p).prod f = s.prod (λa, if p a then f a else 1) := calc (s.filter p).prod f = (s.filter p).prod (λa, if p a then f a else 1) : @@ -184,7 +183,7 @@ calc (s.filter p).prod f = (s.filter p).prod (λa, if p a then f a else 1) : exact if_neg (h hs) end -@[to_additive finset.sum_eq_single] +@[to_additive] lemma prod_eq_single {s : finset α} {f : α → β} (a : α) (h₀ : ∀b∈s, b ≠ a → f b = 1) (h₁ : a ∉ s → f a = 1) : s.prod f = f a := by haveI := classical.dec_eq α; @@ -201,14 +200,14 @@ from classical.by_cases (prod_congr rfl $ λ b hb, h₀ b hb $ by rintro rfl; cc).trans $ prod_const_one.trans (h₁ this).symm) -@[to_additive finset.sum_attach] +@[to_additive] lemma prod_attach {f : α → β} : s.attach.prod (λx, f x.val) = s.prod f := by haveI := classical.dec_eq α; exact calc s.attach.prod (λx, f x.val) = ((s.attach).image subtype.val).prod f : by rw [prod_image]; exact assume x _ y _, subtype.eq ... = _ : by rw [attach_image_val] -@[to_additive finset.sum_bij] +@[to_additive] lemma prod_bij {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Πa∈s, γ) (hi : ∀a ha, i a ha ∈ t) (h : ∀a ha, f a = g (i a ha)) (i_inj : ∀a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀b∈t, ∃a ha, b = i a ha) : @@ -224,7 +223,7 @@ calc s.prod f = s.attach.prod (λx, f x.val) : prod_attach.symm (assume b hb hb1, false.elim $ hb1 $ by rcases i_surj b hb with ⟨a, ha, rfl⟩; exact mem_image.2 ⟨⟨_, _⟩, mem_attach _ _, rfl⟩) -@[to_additive finset.sum_bij_ne_zero] +@[to_additive] lemma prod_bij_ne_one {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Πa∈s, f a ≠ 1 → γ) (hi₁ : ∀a h₁ h₂, i a h₁ h₂ ∈ t) (hi₂ : ∀a₁ a₂ h₁₁ h₁₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) @@ -246,7 +245,7 @@ calc s.prod f = (s.filter $ λx, f x ≠ 1).prod f : ... = t.prod g : (prod_subset (filter_subset _) $ by simp only [not_imp_comm, mem_filter]; exact λ _, and.intro) -@[to_additive finset.exists_ne_zero_of_sum_ne_zero] +@[to_additive] lemma exists_ne_one_of_prod_ne_one : s.prod f ≠ 1 → ∃a∈s, f a ≠ 1 := by haveI := classical.dec_eq α; exact finset.induction_on s (λ H, (H rfl).elim) (assume a s has ih h, @@ -257,7 +256,7 @@ finset.induction_on s (λ H, (H rfl).elim) (assume a s has ih h, (assume hna : f a ≠ 1, ⟨a, mem_insert_self _ _, hna⟩)) -@[to_additive finset.sum_range_succ] +@[to_additive] lemma prod_range_succ (f : ℕ → β) (n : ℕ) : (range (nat.succ n)).prod f = f n * (range n).prod f := by rw [range_succ, prod_insert not_mem_range_self] @@ -283,7 +282,7 @@ lemma prod_nat_pow (s : finset α) (n : ℕ) (f : α → ℕ) : by haveI := classical.dec_eq α; exact finset.induction_on s (by simp) (by simp [nat.mul_pow] {contextual := tt}) -@[to_additive finset.sum_involution] +@[to_additive] lemma prod_involution {s : finset α} {f : α → β} : ∀ (g : Π a ∈ s, α) (h₁ : ∀ a ha, f a * f (g a ha) = 1) @@ -323,32 +322,29 @@ finset.strong_induction_on s ← insert_erase (mem_erase.2 ⟨h₂ x hx hx1, h₃ x hx⟩), prod_insert (not_mem_erase _ _), ih', mul_one, h₁ x hx]) -@[to_additive finset.sum_eq_zero] +@[to_additive] lemma prod_eq_one [comm_monoid β] {f : α → β} {s : finset α} (h : ∀x∈s, f x = 1) : s.prod f = 1 := calc s.prod f = s.prod (λx, 1) : finset.prod_congr rfl h ... = 1 : finset.prod_const_one end comm_monoid -lemma sum_hom [add_comm_monoid β] [add_comm_monoid γ] (g : β → γ) [is_add_monoid_hom g] : - s.sum (λx, g (f x)) = g (s.sum f) := -eq.trans (by rw is_add_monoid_hom.map_zero g; refl) (fold_hom $ is_add_monoid_hom.map_add g) -attribute [to_additive finset.sum_hom] prod_hom +attribute [to_additive] prod_hom lemma sum_smul [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) : s.sum (λ x, add_monoid.smul n (f x)) = add_monoid.smul n (s.sum f) := @prod_pow _ (multiplicative β) _ _ _ _ -attribute [to_additive finset.sum_smul] prod_pow +attribute [to_additive sum_smul] prod_pow @[simp] lemma sum_const [add_comm_monoid β] (b : β) : s.sum (λ a, b) = add_monoid.smul s.card b := @prod_const _ (multiplicative β) _ _ _ -attribute [to_additive finset.sum_const] prod_const +attribute [to_additive] prod_const lemma sum_range_succ' [add_comm_monoid β] (f : ℕ → β) : ∀ n : ℕ, (range (nat.succ n)).sum f = (range n).sum (f ∘ nat.succ) + f 0 := @prod_range_succ' (multiplicative β) _ _ -attribute [to_additive finset.sum_range_succ'] prod_range_succ' +attribute [to_additive] prod_range_succ' lemma sum_nat_cast [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ℕ) : ↑(s.sum f) = s.sum (λa, f a : α → β) := @@ -382,7 +378,7 @@ le_sum_of_subadditive _ abs_zero abs_add s f section comm_group variables [comm_group β] -@[simp, to_additive finset.sum_neg_distrib] +@[simp, to_additive] lemma prod_inv_distrib : s.prod (λx, (f x)⁻¹) = (s.prod f)⁻¹ := prod_hom has_inv.inv @@ -653,7 +649,7 @@ section group open list variables [group α] [group β] -@[to_additive is_add_group_hom.map_sum] +@[to_additive] theorem is_group_hom.map_prod (f : α → β) [is_group_hom f] (l : list α) : f (prod l) = prod (map f l) := by induction l; simp only [*, is_mul_hom.map_mul f, is_group_hom.map_one f, prod_nil, prod_cons, map] @@ -671,12 +667,12 @@ end group section comm_group variables [comm_group α] [comm_group β] (f : α → β) [is_group_hom f] -@[to_additive is_add_group_hom.multiset_sum] +@[to_additive] lemma is_group_hom.map_multiset_prod (m : multiset α) : f m.prod = (m.map f).prod := quotient.induction_on m $ assume l, by simp [is_group_hom.map_prod f l] -@[to_additive is_add_group_hom.finset_sum] -lemma is_group_hom.finset_prod (g : γ → α) (s : finset γ) : f (s.prod g) = s.prod (f ∘ g) := +@[to_additive] +lemma is_group_hom.map_finset_prod (g : γ → α) (s : finset γ) : f (s.prod g) = s.prod (f ∘ g) := show f (s.val.map g).prod = (s.val.map (f ∘ g)).prod, by rw [is_group_hom.map_multiset_prod f]; simp end comm_group diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean index b7597f916d580..38c0348f7a1bb 100644 --- a/src/algebra/direct_limit.lean +++ b/src/algebra/direct_limit.lean @@ -123,7 +123,8 @@ lemma to_module_totalize_of_le {x : direct_sum ι G} {i j : ι} direct_sum.to_module R ι (G j) (λ k, totalize G f k j) x = f i j hij (direct_sum.to_module R ι (G i) (λ k, totalize G f k i) x) := begin - rw [← @dfinsupp.sum_single ι G _ _ _ x, dfinsupp.sum], + rw [← @dfinsupp.sum_single ι G _ _ _ x], + unfold dfinsupp.sum, simp only [linear_map.map_sum], refine finset.sum_congr rfl (λ k hk, _), rw direct_sum.single_eq_lof R k (x k), diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean index 8af05140cfd38..bcc308d64cd6d 100644 --- a/src/algebra/group/basic.lean +++ b/src/algebra/group/basic.lean @@ -10,34 +10,28 @@ import algebra.group.to_additive universe u variable {α : Type u} +@[to_additive add_monoid_to_is_left_id] instance monoid_to_is_left_id {α : Type*} [monoid α] : is_left_id α (*) 1 := ⟨ monoid.one_mul ⟩ +@[to_additive add_monoid_to_is_right_id] instance monoid_to_is_right_id {α : Type*} [monoid α] : is_right_id α (*) 1 := ⟨ monoid.mul_one ⟩ -instance add_monoid_to_is_left_id {α : Type*} [add_monoid α] -: is_left_id α (+) 0 := -⟨ add_monoid.zero_add ⟩ - -instance add_monoid_to_is_right_id {α : Type*} [add_monoid α] -: is_right_id α (+) 0 := -⟨ add_monoid.add_zero ⟩ - -@[simp, to_additive add_left_inj] +@[simp, to_additive] theorem mul_left_inj [left_cancel_semigroup α] (a : α) {b c : α} : a * b = a * c ↔ b = c := ⟨mul_left_cancel, congr_arg _⟩ -@[simp, to_additive add_right_inj] +@[simp, to_additive] theorem mul_right_inj [right_cancel_semigroup α] (a : α) {b c : α} : b * a = c * a ↔ b = c := ⟨mul_right_cancel, congr_arg _⟩ section comm_semigroup variables [comm_semigroup α] {a b c d : α} - @[to_additive add_add_add_comm] + @[to_additive] theorem mul_mul_mul_comm : (a * b) * (c * d) = (a * c) * (b * d) := by simp [mul_left_comm, mul_assoc] @@ -46,27 +40,27 @@ end comm_semigroup section group variables [group α] {a b c : α} - @[simp, to_additive neg_inj'] + @[simp, to_additive] theorem inv_inj' : a⁻¹ = b⁻¹ ↔ a = b := ⟨λ h, by rw [← inv_inv a, h, inv_inv], congr_arg _⟩ - @[to_additive eq_of_neg_eq_neg] + @[to_additive] theorem eq_of_inv_eq_inv : a⁻¹ = b⁻¹ → a = b := inv_inj'.1 - @[simp, to_additive add_self_iff_eq_zero] + @[simp, to_additive] theorem mul_self_iff_eq_one : a * a = a ↔ a = 1 := by have := @mul_left_inj _ _ a a 1; rwa mul_one at this - @[simp, to_additive neg_eq_zero] + @[simp, to_additive] theorem inv_eq_one : a⁻¹ = 1 ↔ a = 1 := by rw [← @inv_inj' _ _ a 1, one_inv] - @[simp, to_additive neg_ne_zero] + @[simp, to_additive] theorem inv_ne_one : a⁻¹ ≠ 1 ↔ a ≠ 1 := not_congr inv_eq_one - @[to_additive left_inverse_neg] + @[to_additive] theorem left_inverse_inv (α) [group α] : function.left_inverse (λ a : α, a⁻¹) (λ a, a⁻¹) := assume a, inv_inv a @@ -74,51 +68,51 @@ section group attribute [simp] mul_inv_cancel_left add_neg_cancel_left mul_inv_cancel_right add_neg_cancel_right - @[to_additive eq_neg_iff_eq_neg] + @[to_additive] theorem eq_inv_iff_eq_inv : a = b⁻¹ ↔ b = a⁻¹ := ⟨eq_inv_of_eq_inv, eq_inv_of_eq_inv⟩ - @[to_additive neg_eq_iff_neg_eq] + @[to_additive] theorem inv_eq_iff_inv_eq : a⁻¹ = b ↔ b⁻¹ = a := by rw [eq_comm, @eq_comm _ _ a, eq_inv_iff_eq_inv] - @[to_additive add_eq_zero_iff_eq_neg] + @[to_additive] theorem mul_eq_one_iff_eq_inv : a * b = 1 ↔ a = b⁻¹ := by simpa [mul_left_inv, -mul_right_inj] using @mul_right_inj _ _ b a (b⁻¹) - @[to_additive add_eq_zero_iff_neg_eq] + @[to_additive] theorem mul_eq_one_iff_inv_eq : a * b = 1 ↔ a⁻¹ = b := by rw [mul_eq_one_iff_eq_inv, eq_inv_iff_eq_inv, eq_comm] - @[to_additive eq_neg_iff_add_eq_zero] + @[to_additive] theorem eq_inv_iff_mul_eq_one : a = b⁻¹ ↔ a * b = 1 := mul_eq_one_iff_eq_inv.symm - @[to_additive neg_eq_iff_add_eq_zero] + @[to_additive] theorem inv_eq_iff_mul_eq_one : a⁻¹ = b ↔ a * b = 1 := mul_eq_one_iff_inv_eq.symm - @[to_additive eq_add_neg_iff_add_eq] + @[to_additive] theorem eq_mul_inv_iff_mul_eq : a = b * c⁻¹ ↔ a * c = b := ⟨λ h, by rw [h, inv_mul_cancel_right], λ h, by rw [← h, mul_inv_cancel_right]⟩ - @[to_additive eq_neg_add_iff_add_eq] + @[to_additive] theorem eq_inv_mul_iff_mul_eq : a = b⁻¹ * c ↔ b * a = c := ⟨λ h, by rw [h, mul_inv_cancel_left], λ h, by rw [← h, inv_mul_cancel_left]⟩ - @[to_additive neg_add_eq_iff_eq_add] + @[to_additive] theorem inv_mul_eq_iff_eq_mul : a⁻¹ * b = c ↔ b = a * c := ⟨λ h, by rw [← h, mul_inv_cancel_left], λ h, by rw [h, inv_mul_cancel_left]⟩ - @[to_additive add_neg_eq_iff_eq_add] + @[to_additive] theorem mul_inv_eq_iff_eq_mul : a * b⁻¹ = c ↔ a = c * b := ⟨λ h, by rw [← h, inv_mul_cancel_right], λ h, by rw [h, mul_inv_cancel_right]⟩ - @[to_additive add_neg_eq_zero] + @[to_additive] theorem mul_inv_eq_one {a b : α} : a * b⁻¹ = 1 ↔ a = b := by rw [mul_eq_one_iff_eq_inv, inv_inv] - @[to_additive neg_comm_of_comm] + @[to_additive] theorem inv_comm_of_comm {a b : α} (H : a * b = b * a) : a⁻¹ * b = b * a⁻¹ := begin have : a⁻¹ * (b * a) * a⁻¹ = a⁻¹ * (a * b) * a⁻¹ := diff --git a/src/algebra/group/hom.lean b/src/algebra/group/hom.lean index eb1911ee4ffa8..cd89e611d8f4b 100644 --- a/src/algebra/group/hom.lean +++ b/src/algebra/group/hom.lean @@ -46,88 +46,65 @@ is_group_hom, is_monoid_hom, monoid_hom universes u v variables {α : Type u} {β : Type v} -/-- Predicate for maps which preserve a multiplication. -/ -class is_mul_hom {α β : Type*} [has_mul α] [has_mul β] (f : α → β) : Prop := -(map_mul : ∀ x y, f (x * y) = f x * f y) - /-- Predicate for maps which preserve an addition. -/ class is_add_hom {α β : Type*} [has_add α] [has_add β] (f : α → β) : Prop := (map_add : ∀ x y, f (x + y) = f x + f y) -attribute [to_additive is_add_hom] is_mul_hom -attribute [to_additive is_add_hom.cases_on] is_mul_hom.cases_on -attribute [to_additive is_add_hom.dcases_on] is_mul_hom.dcases_on -attribute [to_additive is_add_hom.drec] is_mul_hom.drec -attribute [to_additive is_add_hom.drec_on] is_mul_hom.drec_on -attribute [to_additive is_add_hom.map_add] is_mul_hom.map_mul -attribute [to_additive is_add_hom.mk] is_mul_hom.mk -attribute [to_additive is_add_hom.rec] is_mul_hom.rec -attribute [to_additive is_add_hom.rec_on] is_mul_hom.rec_on +/-- Predicate for maps which preserve a multiplication. -/ +@[to_additive] +class is_mul_hom {α β : Type*} [has_mul α] [has_mul β] (f : α → β) : Prop := +(map_mul : ∀ x y, f (x * y) = f x * f y) namespace is_mul_hom variables [has_mul α] [has_mul β] {γ : Type*} [has_mul γ] /-- The identity map preserves multiplication. -/ -@[to_additive is_add_hom.id] +@[to_additive "The identity map preserves addition"] instance id : is_mul_hom (id : α → α) := {map_mul := λ _ _, rfl} /-- The composition of maps which preserve multiplication, also preserves multiplication. -/ -@[to_additive is_add_hom.comp] +@[to_additive "The composition of addition preserving maps also preserves addition"] instance comp (f : α → β) (g : β → γ) [is_mul_hom f] [hg : is_mul_hom g] : is_mul_hom (g ∘ f) := { map_mul := λ x y, by simp only [function.comp, map_mul f, map_mul g] } /-- A product of maps which preserve multiplication, preserves multiplication when the target is commutative. -/ -@[to_additive is_add_hom.add] +@[instance, to_additive] lemma mul {α β} [semigroup α] [comm_semigroup β] (f g : α → β) [is_mul_hom f] [is_mul_hom g] : is_mul_hom (λa, f a * g a) := { map_mul := assume a b, by simp only [map_mul f, map_mul g, mul_comm, mul_assoc, mul_left_comm] } -attribute [instance] is_mul_hom.mul is_add_hom.add - /-- The inverse of a map which preserves multiplication, preserves multiplication when the target is commutative. -/ -@[to_additive is_add_hom.neg] +@[instance, to_additive] lemma inv {α β} [has_mul α] [comm_group β] (f : α → β) [is_mul_hom f] : is_mul_hom (λa, (f a)⁻¹) := { map_mul := assume a b, (map_mul f a b).symm ▸ mul_inv _ _ } -attribute [instance] is_mul_hom.inv is_add_hom.neg - end is_mul_hom -/-- Predicate for monoid homomorphisms (deprecated -- use the bundled `monoid_hom` version). -/ -class is_monoid_hom [monoid α] [monoid β] (f : α → β) extends is_mul_hom f : Prop := -(map_one : f 1 = 1) - -/-- Predicate for add_monoid homomorphisms (deprecated -- use the bundled `monoid_hom` version. -/ +/-- Predicate for add_monoid homomorphisms (deprecated -- use the bundled `monoid_hom` version). -/ class is_add_monoid_hom [add_monoid α] [add_monoid β] (f : α → β) extends is_add_hom f : Prop := (map_zero : f 0 = 0) -attribute [to_additive is_add_monoid_hom] is_monoid_hom -attribute [to_additive is_add_monoid_hom.to_is_add_hom] is_monoid_hom.to_is_mul_hom -attribute [to_additive is_add_monoid_hom.mk] is_monoid_hom.mk -attribute [to_additive is_add_monoid_hom.cases_on] is_monoid_hom.cases_on -attribute [to_additive is_add_monoid_hom.dcases_on] is_monoid_hom.dcases_on -attribute [to_additive is_add_monoid_hom.rec] is_monoid_hom.rec -attribute [to_additive is_add_monoid_hom.drec] is_monoid_hom.drec -attribute [to_additive is_add_monoid_hom.rec_on] is_monoid_hom.rec_on -attribute [to_additive is_add_monoid_hom.drec_on] is_monoid_hom.drec_on -attribute [to_additive is_add_monoid_hom.map_zero] is_monoid_hom.map_one +/-- Predicate for monoid homomorphisms (deprecated -- use the bundled `monoid_hom` version). -/ +@[to_additive is_add_monoid_hom] +class is_monoid_hom [monoid α] [monoid β] (f : α → β) extends is_mul_hom f : Prop := +(map_one : f 1 = 1) namespace is_monoid_hom variables [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] /-- A monoid homomorphism preserves multiplication. -/ -@[to_additive is_add_monoid_hom.map_add] +@[to_additive] lemma map_mul (x y) : f (x * y) = f x * f y := is_mul_hom.map_mul f x y end is_monoid_hom /-- A map to a group preserving multiplication is a monoid homomorphism. -/ -@[to_additive is_add_monoid_hom.of_add] +@[to_additive] theorem is_monoid_hom.of_mul [monoid α] [group β] (f : α → β) [is_mul_hom f] : is_monoid_hom f := { map_one := mul_self_iff_eq_one.1 $ by rw [← is_mul_hom.map_mul f, one_mul] } @@ -136,11 +113,11 @@ namespace is_monoid_hom variables [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] /-- The identity map is a monoid homomorphism. -/ -@[to_additive is_add_monoid_hom.id] +@[to_additive] instance id : is_monoid_hom (@id α) := { map_one := rfl } /-- The composite of two monoid homomorphisms is a monoid homomorphism. -/ -@[to_additive is_add_monoid_hom.comp] +@[to_additive] instance comp {γ} [monoid γ] (g : β → γ) [is_monoid_hom g] : is_monoid_hom (g ∘ f) := { map_one := show g _ = 1, by rw [map_one f, map_one g] } @@ -161,25 +138,16 @@ instance is_add_monoid_hom_mul_right {γ : Type*} [semiring γ] (x : γ) : end is_add_monoid_hom -/-- Predicate for group homomorphisms (deprecated -- use bundled `monoid_hom`). -/ -class is_group_hom [group α] [group β] (f : α → β) extends is_mul_hom f : Prop - /-- Predicate for additive group homomorphism (deprecated -- use bundled `monoid_hom`). -/ class is_add_group_hom [add_group α] [add_group β] (f : α → β) extends is_add_hom f : Prop -attribute [to_additive is_add_group_hom] is_group_hom -attribute [to_additive is_add_group_hom.to_is_add_hom] is_group_hom.to_is_mul_hom -attribute [to_additive is_add_group_hom.cases_on] is_group_hom.cases_on -attribute [to_additive is_add_group_hom.dcases_on] is_group_hom.dcases_on -attribute [to_additive is_add_group_hom.rec] is_group_hom.rec -attribute [to_additive is_add_group_hom.drec] is_group_hom.drec -attribute [to_additive is_add_group_hom.rec_on] is_group_hom.rec_on -attribute [to_additive is_add_group_hom.drec_on] is_group_hom.drec_on -attribute [to_additive is_add_group_hom.mk] is_group_hom.mk +/-- Predicate for group homomorphisms (deprecated -- use bundled `monoid_hom`). -/ +@[to_additive is_add_group_hom] +class is_group_hom [group α] [group β] (f : α → β) extends is_mul_hom f : Prop /-- Construct `is_group_hom` from its only hypothesis. The default constructor tries to get `is_mul_hom` from class instances, and this makes some proofs fail. -/ -@[to_additive is_add_group_hom.mk'] +@[to_additive] lemma is_group_hom.mk' [group α] [group β] {f : α → β} (hf : ∀ x y, f (x * y) = f x * f y) : is_group_hom f := { map_mul := hf } @@ -189,29 +157,29 @@ variables [group α] [group β] (f : α → β) [is_group_hom f] open is_mul_hom (map_mul) /-- A group homomorphism is a monoid homomorphism. -/ -@[to_additive is_add_group_hom.to_is_add_monoid_hom] +@[to_additive to_is_add_monoid_hom] instance to_is_monoid_hom : is_monoid_hom f := is_monoid_hom.of_mul f /-- A group homomorphism sends 1 to 1. -/ -@[to_additive is_add_group_hom.map_zero] +@[to_additive] lemma map_one : f 1 = 1 := is_monoid_hom.map_one f /-- A group homomorphism sends inverses to inverses. -/ -@[to_additive is_add_group_hom.map_neg] +@[to_additive] theorem map_inv (a : α) : f a⁻¹ = (f a)⁻¹ := eq_inv_of_mul_eq_one $ by rw [← map_mul f, inv_mul_self, map_one f] /-- The identity is a group homomorphism. -/ -@[to_additive is_add_group_hom.id] +@[to_additive] instance id : is_group_hom (@id α) := { } /-- The composition of two group homomomorphisms is a group homomorphism. -/ -@[to_additive is_add_group_hom.comp] +@[to_additive] instance comp {γ} [group γ] (g : β → γ) [is_group_hom g] : is_group_hom (g ∘ f) := { } /-- A group homomorphism is injective iff its kernel is trivial. -/ -@[to_additive is_add_group_hom.injective_iff] +@[to_additive] lemma injective_iff (f : α → β) [is_group_hom f] : function.injective f ↔ (∀ a, f a = 1 → a = 1) := ⟨λ h _, by rw ← is_group_hom.map_one f; exact @h _ _, @@ -220,31 +188,25 @@ lemma injective_iff (f : α → β) [is_group_hom f] : simpa using inv_eq_of_mul_eq_one (h _ hxy)⟩ /-- The product of group homomorphisms is a group homomorphism if the target is commutative. -/ -@[to_additive is_add_group_hom.add] +@[instance, to_additive] lemma mul {α β} [group α] [comm_group β] (f g : α → β) [is_group_hom f] [is_group_hom g] : is_group_hom (λa, f a * g a) := { } -attribute [instance] is_group_hom.mul is_add_group_hom.add - /-- The inverse of a group homomorphism is a group homomorphism if the target is commutative. -/ -@[to_additive is_add_group_hom.neg] +@[instance, to_additive] lemma inv {α β} [group α] [comm_group β] (f : α → β) [is_group_hom f] : is_group_hom (λa, (f a)⁻¹) := { } -attribute [instance] is_group_hom.inv is_add_group_hom.neg - end is_group_hom /-- Inversion is a group homomorphism if the group is commutative. -/ -@[to_additive neg.is_add_group_hom] +@[instance, to_additive is_add_group_hom] lemma inv.is_group_hom [comm_group α] : is_group_hom (has_inv.inv : α → α) := { map_mul := mul_inv } -attribute [instance] inv.is_group_hom neg.is_add_group_hom - namespace is_add_group_hom variables [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] @@ -257,14 +219,22 @@ end is_add_group_hom /-- The difference of two additive group homomorphisms is an additive group homomorphism if the target is commutative. -/ +@[instance] lemma is_add_group_hom.sub {α β} [add_group α] [add_comm_group β] (f g : α → β) [is_add_group_hom f] [is_add_group_hom g] : is_add_group_hom (λa, f a - g a) := is_add_group_hom.add f (λa, - g a) -attribute [instance] is_add_group_hom.sub +/-- Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too. -/ +structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N] := +(to_fun : M → N) +(map_zero' : to_fun 0 = 0) +(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y) + +infixr ` →+ `:25 := add_monoid_hom /-- Bundled monoid homomorphisms; use this for bundled group homomorphisms too. -/ +@[to_additive add_monoid_hom] structure monoid_hom (M : Type*) (N : Type*) [monoid M] [monoid N] := (to_fun : M → N) (map_one' : to_fun 1 = 1) @@ -272,100 +242,86 @@ structure monoid_hom (M : Type*) (N : Type*) [monoid M] [monoid N] := infixr ` →* `:25 := monoid_hom +@[to_additive] instance {M : Type*} {N : Type*} [monoid M] [monoid N] : has_coe_to_fun (M →* N) := ⟨_, monoid_hom.to_fun⟩ /-- Reinterpret a map `f : M → N` as a homomorphism `M →* N` -/ +@[to_additive as_add_monoid_hom] def as_monoid_hom {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M → N) [h : is_monoid_hom f] : M →* N := { to_fun := f, map_one' := h.2, map_mul' := h.1.1 } -@[simp] lemma coe_as_monoid_hom {M : Type u} {N : Type v} [monoid M] [monoid N] +@[simp, to_additive coe_as_add_monoid_hom] +lemma coe_as_monoid_hom {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M → N) [is_monoid_hom f] : ⇑ (as_monoid_hom f) = f := rfl -/-- Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too. -/ -structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N] := -(to_fun : M → N) -(map_zero' : to_fun 0 = 0) -(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y) - -infixr ` →+ `:25 := add_monoid_hom - -instance {A : Type*} {B : Type*} [add_monoid A] [add_monoid B] : has_coe_to_fun (A →+ B) := -⟨_, add_monoid_hom.to_fun⟩ - -attribute [to_additive add_monoid_hom] monoid_hom -attribute [to_additive add_monoid_hom.has_sizeof_inst] monoid_hom.has_sizeof_inst -attribute [to_additive add_monoid_hom.map_zero'] monoid_hom.map_one' -attribute [to_additive add_monoid_hom.map_add'] monoid_hom.map_mul' -attribute [to_additive add_monoid_hom.mk] monoid_hom.mk -attribute [to_additive add_monoid_hom.mk.inj] monoid_hom.mk.inj -attribute [to_additive add_monoid_hom.mk.inj_arrow] monoid_hom.mk.inj_arrow -attribute [to_additive add_monoid_hom.mk.inj_eq] monoid_hom.mk.inj_eq -attribute [to_additive add_monoid_hom.mk.sizeof_spec] monoid_hom.mk.sizeof_spec -attribute [to_additive add_monoid_hom.no_confusion] monoid_hom.no_confusion -attribute [to_additive add_monoid_hom.no_confusion_type] monoid_hom.no_confusion_type -attribute [to_additive add_monoid_hom.rec] monoid_hom.rec -attribute [to_additive add_monoid_hom.rec_on] monoid_hom.rec_on -attribute [to_additive add_monoid_hom.sizeof] monoid_hom.sizeof -attribute [to_additive add_monoid_hom.to_fun] monoid_hom.to_fun -attribute [to_additive as_add_monoid_hom._proof_1] as_monoid_hom._proof_1 -attribute [to_additive as_add_monoid_hom] as_monoid_hom - namespace monoid_hom variables {M : Type*} {N : Type*} {P : Type*} [monoid M] [monoid N] [monoid P] variables {G : Type*} {H : Type*} [group G] [comm_group H] -@[extensionality] def ext (f g : M →* N) (h : (f : M → N) = g) : f = g := +@[extensionality, to_additive] +lemma ext (f g : M →* N) (h : (f : M → N) = g) : f = g := by cases f; cases g; cases h; refl /-- If f is a monoid homomorphism then f 1 = 1. -/ -@[simp] lemma map_one (f : M →* N) : f 1 = 1 := f.map_one' +@[simp, to_additive] +lemma map_one (f : M →* N) : f 1 = 1 := f.map_one' /-- If f is a monoid homomorphism then f (a * b) = f a * f b. -/ -@[simp] lemma map_mul (f : M →* N) (a b : M) : f (a * b) = f a * f b := f.map_mul' a b +@[simp, to_additive] +lemma map_mul (f : M →* N) (a b : M) : f (a * b) = f a * f b := f.map_mul' a b +@[to_additive is_add_monoid_hom] instance {M : Type*} {N : Type*} [monoid M] [monoid N] (f : M →* N) : is_monoid_hom (f : M → N) := { map_mul := f.map_mul, map_one := f.map_one } +@[to_additive is_add_group_hom] instance {G : Type*} {H : Type*} [group G] [group H] (f : G →* H) : is_group_hom (f : G → H) := { map_mul := f.map_mul } /-- The identity map from a monoid to itself. -/ +@[to_additive] def id (M : Type*) [monoid M] : M →* M := { to_fun := id, map_one' := rfl, map_mul' := λ _ _, rfl } /-- Composition of monoid morphisms is a monoid morphism. -/ +@[to_additive] def comp (hnp : N →* P) (hmn : M →* N) : M →* P := { to_fun := hnp ∘ hmn, map_one' := by simp, map_mul' := by simp } +@[to_additive] protected def one : M →* N := { to_fun := λ _, 1, map_one' := rfl, map_mul' := λ _ _, (one_mul 1).symm } +@[to_additive] instance : has_one (M →* N) := ⟨monoid_hom.one⟩ /-- The product of two monoid morphisms is a monoid morphism if the target is commutative. -/ +@[to_additive] protected def mul {M N} [monoid M] [comm_monoid N] (f g : M →* N) : M →* N := { to_fun := λ m, f m * g m, map_one' := show f 1 * g 1 = 1, by simp, map_mul' := begin intros, show f (x * y) * g (x * y) = f x * g x * (f y * g y), rw [f.map_mul, g.map_mul, ←mul_assoc, ←mul_assoc, mul_right_comm (f x)], end } +@[to_additive] instance {M N} [monoid M] [comm_monoid N] : has_mul (M →* N) := ⟨monoid_hom.mul⟩ /-- (M →* N) is a comm_monoid if N is commutative. -/ +@[to_additive add_comm_monoid] instance {M N} [monoid M] [comm_monoid N] : comm_monoid (M →* N) := { mul := (*), mul_assoc := by intros; ext; apply mul_assoc, @@ -375,14 +331,17 @@ instance {M N} [monoid M] [comm_monoid N] : comm_monoid (M →* N) := mul_comm := by intros; ext; apply mul_comm } /-- Group homomorphisms preserve inverse. -/ -@[simp] theorem map_inv {G H} [group G] [group H] (f : G →* H) (g : G) : f g⁻¹ = (f g)⁻¹ := +@[simp, to_additive] +theorem map_inv {G H} [group G] [group H] (f : G →* H) (g : G) : f g⁻¹ = (f g)⁻¹ := eq_inv_of_mul_eq_one $ by rw [←f.map_mul, inv_mul_self, f.map_one] /-- Group homomorphisms preserve division. -/ -@[simp] theorem map_div {G H} [group G] [group H] (f : G →* H) (g h : G) : +@[simp, to_additive] +theorem map_mul_inv {G H} [group G] [group H] (f : G →* H) (g h : G) : f (g * h⁻¹) = (f g) * (f h)⁻¹ := by rw [f.map_mul, f.map_inv] /-- Makes a group homomomorphism from a proof that the map preserves multiplication. -/ +@[to_additive] def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G := { to_fun := f, map_mul' := map_mul, @@ -390,12 +349,15 @@ def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G /-- The inverse of a monoid homomorphism is a monoid homomorphism if the target is a commutative group.-/ +@[to_additive] protected def inv {M G} [monoid M] [comm_group G] (f : M →* G) : M →* G := mk' (λ g, (f g)⁻¹) $ λ a b, by rw [←mul_inv, f.map_mul] +@[to_additive] instance {M G} [monoid M] [comm_group G] : has_inv (M →* G) := ⟨monoid_hom.inv⟩ /-- (M →* G) is a comm_group if G is a comm_group -/ +@[to_additive add_comm_group] instance {M G} [monoid M] [comm_group G] : comm_group (M →* G) := { inv := has_inv.inv, mul_left_inv := by intros; ext; apply mul_left_inv, @@ -403,130 +365,6 @@ instance {M G} [monoid M] [comm_group G] : comm_group (M →* G) := end monoid_hom -namespace add_monoid_hom -variables {A : Type*} {B : Type*} {C : Type*} [add_monoid A] [add_monoid B] [add_monoid C] -{G : Type*} [add_group G] {H : Type*} [add_group H] - -/-- two additive monoid homomorphisms with equal underlying maps are equal-/ -@[extensionality] def ext (f g : A →+ B) (h : (f : A → B) = g) : f = g := -by cases f; cases g; cases h; refl - -attribute [to_additive add_monoid_hom.ext] monoid_hom.ext -attribute [to_additive add_monoid_hom.ext.equations._eqn_1] monoid_hom.ext.equations._eqn_1 - -/-- if f is a additive monoid homomorphism then f 0 = 0-/ -@[simp] def map_zero (f : A →+ B) : f 0 = 0 := f.map_zero' - -attribute [to_additive add_monoid_hom.map_zero] monoid_hom.map_one - -/-- if f is an additive monoid homomorphism then f (a + b) = f a + f b -/ -@[simp] def map_add (f : A →+ B) : ∀ a b : A, f (a + b) = f a + f b := f.map_add' - -attribute [to_additive add_monoid_hom.map_add] monoid_hom.map_mul - -instance {A : Type*} {B : Type*} [add_monoid A] [add_monoid B] (f : A →+ B) : - is_add_monoid_hom (f : A → B) := -{ map_add := f.map_add, - map_zero := f.map_zero } - -instance {G : Type*} {H : Type*} [add_group G] [add_group H] (f : G →+ H) : - is_add_group_hom (f : G → H) := -{ map_add := f.map_add } - -/-- the identity map from an add_monoid to itself -/ -def id (A : Type*) [add_monoid A] : A →+ A := -{ to_fun := id, - map_zero' := rfl, - map_add' := λ _ _, rfl } - -attribute [to_additive add_monoid_hom.id._proof_1] monoid_hom.id._proof_1 -attribute [to_additive add_monoid_hom.id._proof_2] monoid_hom.id._proof_2 -attribute [to_additive add_monoid_hom.id.equations._eqn_1] monoid_hom.id.equations._eqn_1 - -/-- composition of additive monoid morphisms is an additive monoid morphism -/ -def comp (fbc : B →+ C) (fab : A →+ B) : A →+ C := -{ to_fun := fbc ∘ fab, - map_zero' := by simp, - map_add' := by simp } - -attribute [to_additive add_monoid_hom.comp] monoid_hom.comp -attribute [to_additive add_monoid_hom.comp._proof_1] monoid_hom.comp._proof_1 -attribute [to_additive add_monoid_hom.comp._proof_2] monoid_hom.comp._proof_2 -attribute [to_additive add_monoid_hom.comp.equations._eqn_1] monoid_hom.comp.equations._eqn_1 - -protected def zero : A →+ B := -{ to_fun := λ _, 0, - map_zero' := rfl, - map_add' := λ _ _, (zero_add 0).symm } - -attribute [to_additive add_monoid_hom.zero] monoid_hom.one -attribute [to_additive add_monoid_hom.zero._proof_1] monoid_hom.one._proof_1 -attribute [to_additive add_monoid_hom.zero._proof_2] monoid_hom.one._proof_2 -attribute [to_additive add_monoid_hom.zero.equations._eqn_1] monoid_hom.one.equations._eqn_1 - -instance : has_zero (A →+ B) := ⟨add_monoid_hom.zero⟩ - -/-- The sum of two additive monoid morphisms is an additive monoid morphism if the -target is commutative-/ -protected def add {A B} [add_monoid A] [add_comm_monoid B] (f g : A →+ B) : A →+ B := -{ to_fun := λ m, f m + g m, - map_zero' := show f 0 + g 0 = 0, by simp, - map_add' := begin intros, show f (x + y) + g (x + y) = f x + g x + (f y + g y), - rw [f.map_add, g.map_add, ←add_assoc, ←add_assoc, add_right_comm (f x)], end } - -attribute [to_additive add_monoid_hom.add] monoid_hom.mul -attribute [to_additive add_monoid_hom.add._proof_1] monoid_hom.mul._proof_1 -attribute [to_additive add_monoid_hom.add._proof_2] monoid_hom.mul._proof_2 -attribute [to_additive add_monoid_hom.add.equations._eqn_1] monoid_hom.mul.equations._eqn_1 - -instance {A B} [add_monoid A] [add_comm_monoid B] : has_add (A →+ B) := ⟨add_monoid_hom.add⟩ - -/-- (A →+ B) is an add_comm_monoid if B is commutative. -/ -instance {A B} [add_monoid A] [add_comm_monoid B] : add_comm_monoid (A →+ B) := -{ add := (+), - add_assoc := λ _ _ _, by ext; apply add_assoc, - zero := 0, - zero_add := λ _, by ext; apply zero_add, - add_zero := λ _, by ext; apply add_zero, - add_comm := λ _ _, by ext; apply add_comm } - -/-- Additive group homomorphisms preserve additive inverse. -/ -@[simp] theorem map_neg (f : G →+ H) (a : G) : f (-a) = -(f a) := -eq_neg_of_add_eq_zero $ by rw [←f.map_add, neg_add_self, f.map_zero] - -attribute [to_additive add_monoid_hom.map_neg] monoid_hom.map_inv - /-- Additive group homomorphisms preserve subtraction. -/ -@[simp] theorem map_sub {G H} [add_group G] [add_group H] (f : G →+ H) (g h : G) : - f (g - h) = (f g) - (f h) := by simp [f.map_add, f.map_neg] - -attribute [to_additive add_monoid_hom.map_sub] monoid_hom.map_div - -/-- makes an additive group homomomorphism from a proof that the map preserves addition -/ -def mk' (f : A → G) (map_add : ∀ x y : A, f (x + y) = f x + f y) : A →+ G := -{ to_fun := f, - map_add' := map_add, - map_zero' := add_self_iff_eq_zero.1 $ by rw [←map_add, add_zero] } - -attribute [to_additive add_monoid_hom.mk'] monoid_hom.mk' -attribute [to_additive add_monoid_hom.mk'._proof_1] monoid_hom.mk'._proof_1 -attribute [to_additive add_monoid_hom.mk'.equations._eqn_1] monoid_hom.mk'.equations._eqn_1 - -/-- the additive inverse of an additive group homomorphism is an additive group homomorphism if the -target is commutative-/ -def neg {A B} [add_monoid A] [add_comm_group B] (f : A →+ B) : A →+ B := -mk' (λ g, -(f g)) $ λ a b, by rw [←neg_add, f.map_add] - -attribute [to_additive add_monoid_hom.neg] monoid_hom.inv -attribute [to_additive add_monoid_hom.neg._proof_1] monoid_hom.inv._proof_1 -attribute [to_additive add_monoid_hom.neg.equations._eqn_1] monoid_hom.inv.equations._eqn_1 - -instance {A B} [add_monoid A] [add_comm_group B]: has_neg (A →+ B) := ⟨add_monoid_hom.neg⟩ - -/-- (A →* B) is an add_comm_group if B is an add_comm_group -/ -instance {A B} [add_monoid A] [add_comm_group B] : add_comm_group (A →+ B) := -{ neg := has_neg.neg, - add_left_neg := by intros; ext; apply add_left_neg, - ..add_monoid_hom.add_comm_monoid } - -end add_monoid_hom +@[simp] theorem add_monoid_hom.map_sub {G H} [add_group G] [add_group H] (f : G →+ H) (g h : G) : + f (g - h) = (f g) - (f h) := f.map_add_neg g h diff --git a/src/algebra/group/to_additive.lean b/src/algebra/group/to_additive.lean index e47e6cdd2161c..976736af71778 100644 --- a/src/algebra/group/to_additive.lean +++ b/src/algebra/group/to_additive.lean @@ -1,139 +1,257 @@ /- Copyright (c) 2017 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro. +Authors: Mario Carneiro, Yury Kudryashov. +-/ + +import tactic.basic tactic.transport tactic.algebra + +/-! +# Transport multiplicative to additive + +This file defines an attribute `to_additive` that can be used to +automatically transport theorems and definitions (but not inductive +types and structures) from multiplicative theory to additive theory. + +To use this attribute, just write + +``` +@[to_additive] +theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm +``` + +This code will generate a theorem named `add_comm'`. It is also +possible to manually specify the name of the new declaration, and +provide a documentation string. + +The transport tries to do the right thing in most cases using several +heuristics described below. However, in some cases it fails, and +requires manual intervention. + +## Implementation notes +### Handling of hidden definitions + +Before transporting the “main” declaration `src`, `to_additive` first +scans its type and value for names starting with `src`, and transports +them. This includes auxiliary definitions like `src._match_1`, +`src._proof_1`. + +After transporting the “main” declaration, `to_additive` transports +its equational lemmas. + +### Structure fields and constructors + +If `src` is a structure, then `to_additive` automatically adds +structure fields to its mapping, and similarly for constructors of +inductive types. + +For new structures this means that `to_additive` automatically handles +coercions, and for old structures it does the same, if ancestry +information is present in `@[ancestor]` attributes. + +### Name generation + +* If `@[to_additive]` is called without a `name` argument, then the + new name is autogenerated. First, it takes the longest prefix of + the source name that is already known to `to_additive`, and replaces + this prefix with its additive counterpart. Second, it takes the last + part of the name (i.e., after the last dot), and replaces common + name parts (“mul”, “one”, “inv”, “prod”) with their additive versions. + +* If `@[to_additive]` is called with a `name` argument `new_name` + /without a dot/, then `to_additive` updates the prefix as described + above, then replaces the last part of the name with `new_name`. + +* If `@[to_additive]` is called with a `name` argument + `new_namespace.new_name` /with a dot/, then `to_additive` uses this + new name as is. + +As a safety check, in the first two cases `to_additive` double checks +that the new name differs from the original one. + +### Missing features -Transport multiplicative to additive +* Automatically transport structures and other inductive types. + +* Handle `protected` attribute. Currently all new definitions are public. + +* For structures, automatically generate theorems like `group α ↔ + add_group (additive α)`. + +* Mapping of prefixes that do not correspond to any definition, see + `quotient_group`. + +* Rewrite rules for the last part of the name that work in more + cases. E.g., we can replace `monoid` with `add_monoid` etc. -/ -import tactic.basic data.option.defs +namespace to_additive +open tactic exceptional + +@[user_attribute] +meta def aux_attr : user_attribute (name_map name) name := +{ name := `to_additive_aux, + descr := "Auxiliary attribute for `to_additive`. DON'T USE IT", + cache_cfg := ⟨λ ns, + ns.mfoldl + (λ dict n', + let n := match n' with + | name.mk_string s pre := if s = "_to_additive" then pre else n' + | _ := n' + end + in dict.insert n <$> aux_attr.get_param n') + mk_name_map, []⟩, + parser := lean.parser.ident } + +meta def map_namespace (src tgt : name) : command := +do decl ← get_decl `bool, -- random choice + let n := src.mk_string "_to_additive", + let decl := decl.update_name n, + add_decl decl, + aux_attr.set n tgt tt + +@[derive has_reflect] +structure value_type := (tgt : name) (doc : option string) + +meta def tokens_dict : native.rb_map string string := +native.rb_map.of_list $ +[("mul", "add"), ("one", "zero"), ("inv", "neg"), ("prod", "sum")] + +meta def guess_name : string → string := +string.map_tokens '_' $ list.map $ +string.map_tokens ''' $ list.map $ +λ s, (tokens_dict.find s).get_or_else s -section transport -open tactic +meta def target_name (src tgt : name) (dict : name_map name) : tactic name := +(if tgt.get_prefix ≠ name.anonymous -- `tgt` is a full name + then pure tgt + else match src with + | (name.mk_string s pre) := + do let tgt_auto := guess_name s, + guard (tgt.to_string ≠ tgt_auto) + <|> trace ("`to_additive " ++ src.to_string ++ "`: remove `name` argument"), + pure $ name.mk_string + (if tgt = name.anonymous then tgt_auto else tgt.to_string) + (pre.map_prefix dict.find) + | _ := fail ("to_additive: can't transport " ++ src.to_string) + end) >>= +(λ res, + if res = src + then fail ("to_additive: can't transport " ++ src.to_string ++ " to itself") + else pure res) + +meta def parser : lean.parser value_type := +do + tgt ← optional lean.parser.ident, + e ← optional interactive.types.texpr, + doc ← match e with + | some pe := some <$> ((to_expr pe >>= eval_expr string) : tactic string) + | none := pure none + end, + return ⟨tgt.get_or_else name.anonymous, doc⟩ + +private meta def proceed_fields_aux (src tgt : name) (prio : ℕ) (f : name → tactic (list string)) : + command := +do + src_fields ← f src, + tgt_fields ← f tgt, + guard (src_fields.length = tgt_fields.length) <|> + fail ("Failed to map fields of " ++ src.to_string), + (src_fields.zip tgt_fields).mmap' $ + λ names, guard (names.fst = names.snd) <|> + aux_attr.set (src.append names.fst) (tgt.append names.snd) tt prio + +meta def proceed_fields (env : environment) (src tgt : name) (prio : ℕ) : command := +let aux := proceed_fields_aux src tgt prio in +do +aux (λ n, pure $ list.map name.to_string $ (env.structure_fields n).get_or_else []) >> +aux (λ n, (list.map (λ (x : name), "to_" ++ x.to_string) <$> + (ancestor_attr.get_param n <|> pure []))) >> +aux (λ n, (env.constructors_of n).mmap $ + λ cs, match cs with + | (name.mk_string s pre) := + (guard (pre = n) <|> fail "Bad constructor name") >> + pure s + | _ := fail "Bad constructor name" + end) @[user_attribute] -meta def to_additive_attr : user_attribute (name_map name) name := +protected meta def attr : user_attribute unit value_type := { name := `to_additive, descr := "Transport multiplicative to additive", - cache_cfg := ⟨λ ns, ns.mfoldl (λ dict n, do - val ← to_additive_attr.get_param n, - pure $ dict.insert n val) mk_name_map, []⟩, - parser := lean.parser.ident, - after_set := some $ λ src _ _, do + parser := parser, + after_set := some $ λ src prio persistent, do + guard persistent <|> fail "`to_additive` can't be used as a local attribute", env ← get_env, - dict ← to_additive_attr.get_cache, - tgt ← to_additive_attr.get_param src, - (get_decl tgt >> skip) <|> - transport_with_dict dict src tgt } - -end transport + val ← attr.get_param src, + dict ← aux_attr.get_cache, + tgt ← target_name src val.tgt dict, + aux_attr.set src tgt tt, + let dict := dict.insert src tgt, + if env.contains tgt + then proceed_fields env src tgt prio + else do + transport_with_prefix_dict dict src tgt + [`reducible, `simp, `instance, `refl, `symm, `trans, `elab_as_eliminator], + match val.doc with + | some doc := add_doc_string tgt doc + | none := skip + end } +end to_additive /- map operations -/ -attribute [to_additive has_add.add] has_mul.mul -attribute [to_additive has_zero.zero] has_one.one -attribute [to_additive has_neg.neg] has_inv.inv -attribute [to_additive has_add] has_mul -attribute [to_additive has_zero] has_one -attribute [to_additive has_neg] has_inv - -/- map constructors -/ -attribute [to_additive has_add.mk] has_mul.mk -attribute [to_additive has_zero.mk] has_one.mk -attribute [to_additive has_neg.mk] has_inv.mk +attribute [to_additive] has_mul has_one has_inv /- map structures -/ attribute [to_additive add_semigroup] semigroup -attribute [to_additive add_semigroup.mk] semigroup.mk -attribute [to_additive add_semigroup.to_has_add] semigroup.to_has_mul -attribute [to_additive add_semigroup.add_assoc] semigroup.mul_assoc -attribute [to_additive add_semigroup.add] semigroup.mul - attribute [to_additive add_comm_semigroup] comm_semigroup -attribute [to_additive add_comm_semigroup.mk] comm_semigroup.mk -attribute [to_additive add_comm_semigroup.to_add_semigroup] comm_semigroup.to_semigroup -attribute [to_additive add_comm_semigroup.add_comm] comm_semigroup.mul_comm - attribute [to_additive add_left_cancel_semigroup] left_cancel_semigroup -attribute [to_additive add_left_cancel_semigroup.mk] left_cancel_semigroup.mk -attribute [to_additive add_left_cancel_semigroup.to_add_semigroup] left_cancel_semigroup.to_semigroup -attribute [to_additive add_left_cancel_semigroup.add_left_cancel] left_cancel_semigroup.mul_left_cancel - attribute [to_additive add_right_cancel_semigroup] right_cancel_semigroup -attribute [to_additive add_right_cancel_semigroup.mk] right_cancel_semigroup.mk -attribute [to_additive add_right_cancel_semigroup.to_add_semigroup] right_cancel_semigroup.to_semigroup -attribute [to_additive add_right_cancel_semigroup.add_right_cancel] right_cancel_semigroup.mul_right_cancel attribute [to_additive add_monoid] monoid -attribute [to_additive add_monoid.mk] monoid.mk -attribute [to_additive add_monoid.to_has_zero] monoid.to_has_one -attribute [to_additive add_monoid.to_add_semigroup] monoid.to_semigroup -attribute [to_additive add_monoid.add] monoid.mul -attribute [to_additive add_monoid.add_assoc] monoid.mul_assoc -attribute [to_additive add_monoid.zero] monoid.one -attribute [to_additive add_monoid.zero_add] monoid.one_mul -attribute [to_additive add_monoid.add_zero] monoid.mul_one - attribute [to_additive add_comm_monoid] comm_monoid -attribute [to_additive add_comm_monoid.mk] comm_monoid.mk -attribute [to_additive add_comm_monoid.to_add_monoid] comm_monoid.to_monoid -attribute [to_additive add_comm_monoid.to_add_comm_semigroup] comm_monoid.to_comm_semigroup - attribute [to_additive add_group] group -attribute [to_additive add_group.mk] group.mk -attribute [to_additive add_group.to_has_neg] group.to_has_inv -attribute [to_additive add_group.to_add_monoid] group.to_monoid -attribute [to_additive add_group.add_left_neg] group.mul_left_inv -attribute [to_additive add_group.add] group.mul -attribute [to_additive add_group.add_assoc] group.mul_assoc -attribute [to_additive add_group.zero] group.one -attribute [to_additive add_group.zero_add] group.one_mul -attribute [to_additive add_group.add_zero] group.mul_one -attribute [to_additive add_group.neg] group.inv - attribute [to_additive add_comm_group] comm_group -attribute [to_additive add_comm_group.mk] comm_group.mk -attribute [to_additive add_comm_group.to_add_group] comm_group.to_group -attribute [to_additive add_comm_group.to_add_comm_monoid] comm_group.to_comm_monoid /- map theorems -/ -attribute [to_additive add_assoc] mul_assoc -attribute [to_additive add_semigroup_to_is_associative] semigroup_to_is_associative -attribute [to_additive add_comm] mul_comm -attribute [to_additive add_comm_semigroup_to_is_commutative] comm_semigroup_to_is_commutative -attribute [to_additive add_left_comm] mul_left_comm -attribute [to_additive add_right_comm] mul_right_comm -attribute [to_additive add_left_cancel] mul_left_cancel -attribute [to_additive add_right_cancel] mul_right_cancel -attribute [to_additive add_left_cancel_iff] mul_left_cancel_iff -attribute [to_additive add_right_cancel_iff] mul_right_cancel_iff -attribute [to_additive zero_add] one_mul -attribute [to_additive add_zero] mul_one -attribute [to_additive add_left_neg] mul_left_inv -attribute [to_additive neg_add_self] inv_mul_self -attribute [to_additive neg_add_cancel_left] inv_mul_cancel_left -attribute [to_additive neg_add_cancel_right] inv_mul_cancel_right -attribute [to_additive neg_eq_of_add_eq_zero] inv_eq_of_mul_eq_one +attribute [to_additive] mul_assoc +attribute [to_additive add_semigroup_to_is_eq_associative] semigroup_to_is_associative +attribute [to_additive] mul_comm +attribute [to_additive add_comm_semigroup_to_is_eq_commutative] comm_semigroup_to_is_commutative +attribute [to_additive] mul_left_comm +attribute [to_additive] mul_right_comm +attribute [to_additive] mul_left_cancel +attribute [to_additive] mul_right_cancel +attribute [to_additive] mul_left_cancel_iff +attribute [to_additive] mul_right_cancel_iff +attribute [to_additive] one_mul +attribute [to_additive] mul_one +attribute [to_additive] mul_left_inv +attribute [to_additive] inv_mul_self +attribute [to_additive] inv_mul_cancel_left +attribute [to_additive] inv_mul_cancel_right +attribute [to_additive] inv_eq_of_mul_eq_one attribute [to_additive neg_zero] one_inv -attribute [to_additive neg_neg] inv_inv -attribute [to_additive add_right_neg] mul_right_inv -attribute [to_additive add_neg_self] mul_inv_self -attribute [to_additive neg_inj] inv_inj -attribute [to_additive add_group.add_left_cancel] group.mul_left_cancel -attribute [to_additive add_group.add_right_cancel] group.mul_right_cancel -attribute [to_additive add_group.to_left_cancel_add_semigroup] group.to_left_cancel_semigroup -attribute [to_additive add_group.to_right_cancel_add_semigroup] group.to_right_cancel_semigroup -attribute [to_additive add_neg_cancel_left] mul_inv_cancel_left -attribute [to_additive add_neg_cancel_right] mul_inv_cancel_right +attribute [to_additive] inv_inv +attribute [to_additive] mul_right_inv +attribute [to_additive] mul_inv_self +attribute [to_additive] inv_inj +attribute [to_additive] group.mul_left_cancel +attribute [to_additive] group.mul_right_cancel +attribute [to_additive to_left_cancel_add_semigroup] group.to_left_cancel_semigroup +attribute [to_additive to_right_cancel_add_semigroup] group.to_right_cancel_semigroup +attribute [to_additive] mul_inv_cancel_left +attribute [to_additive] mul_inv_cancel_right attribute [to_additive neg_add_rev] mul_inv_rev -attribute [to_additive eq_neg_of_eq_neg] eq_inv_of_eq_inv -attribute [to_additive eq_neg_of_add_eq_zero] eq_inv_of_mul_eq_one -attribute [to_additive eq_add_neg_of_add_eq] eq_mul_inv_of_mul_eq -attribute [to_additive eq_neg_add_of_add_eq] eq_inv_mul_of_mul_eq -attribute [to_additive neg_add_eq_of_eq_add] inv_mul_eq_of_eq_mul -attribute [to_additive add_neg_eq_of_eq_add] mul_inv_eq_of_eq_mul -attribute [to_additive eq_add_of_add_neg_eq] eq_mul_of_mul_inv_eq -attribute [to_additive eq_add_of_neg_add_eq] eq_mul_of_inv_mul_eq -attribute [to_additive add_eq_of_eq_neg_add] mul_eq_of_eq_inv_mul -attribute [to_additive add_eq_of_eq_add_neg] mul_eq_of_eq_mul_inv +attribute [to_additive] eq_inv_of_eq_inv +attribute [to_additive] eq_inv_of_mul_eq_one +attribute [to_additive] eq_mul_inv_of_mul_eq +attribute [to_additive] eq_inv_mul_of_mul_eq +attribute [to_additive] inv_mul_eq_of_eq_mul +attribute [to_additive] mul_inv_eq_of_eq_mul +attribute [to_additive] eq_mul_of_mul_inv_eq +attribute [to_additive] eq_mul_of_inv_mul_eq +attribute [to_additive] mul_eq_of_eq_inv_mul +attribute [to_additive] mul_eq_of_eq_mul_inv attribute [to_additive neg_add] mul_inv diff --git a/src/algebra/group/with_one.lean b/src/algebra/group/with_one.lean index 03b1c620df67f..acfd7dc2e4652 100644 --- a/src/algebra/group/with_one.lean +++ b/src/algebra/group/with_one.lean @@ -10,56 +10,53 @@ import algebra.group.to_additive algebra.group.basic algebra.group.hom universes u v variable {α : Type u} -@[to_additive with_zero] +@[to_additive] def with_one (α) := option α namespace with_one -@[to_additive with_zero.monad] +@[to_additive] instance : monad with_one := option.monad -@[to_additive with_zero.has_zero] +@[to_additive] instance : has_one (with_one α) := ⟨none⟩ -@[to_additive with_zero.has_coe_t] +@[to_additive] instance : has_coe_t α (with_one α) := ⟨some⟩ -@[simp, to_additive with_zero.zero_ne_coe] +@[simp, to_additive] lemma one_ne_coe {a : α} : (1 : with_one α) ≠ a := λ h, option.no_confusion h -@[simp, to_additive with_zero.coe_ne_zero] +@[simp, to_additive] lemma coe_ne_one {a : α} : (a : with_one α) ≠ (1 : with_one α) := λ h, option.no_confusion h -@[to_additive with_zero.ne_zero_iff_exists] +@[to_additive] lemma ne_one_iff_exists : ∀ {x : with_one α}, x ≠ 1 ↔ ∃ (a : α), x = a | 1 := ⟨λ h, false.elim $ h rfl, by { rintros ⟨a,ha⟩ h, simpa using h }⟩ | (a : α) := ⟨λ h, ⟨a, rfl⟩, λ h, with_one.coe_ne_one⟩ -@[to_additive with_zero.coe_inj] +@[to_additive] lemma coe_inj {a b : α} : (a : with_one α) = b ↔ a = b := option.some_inj -@[elab_as_eliminator, to_additive with_zero.cases_on] +@[elab_as_eliminator, to_additive] protected lemma cases_on {P : with_one α → Prop} : ∀ (x : with_one α), P 1 → (∀ a : α, P a) → P x := option.cases_on -attribute [to_additive with_zero.has_zero.equations._eqn_1] with_one.has_one.equations._eqn_1 - -@[to_additive with_zero.has_add] +@[to_additive] instance [has_mul α] : has_mul (with_one α) := { mul := option.lift_or_get (*) } -@[simp, to_additive with_zero.add_coe] +@[simp, to_additive] lemma mul_coe [has_mul α] (a b : α) : (a : with_one α) * b = (a * b : α) := rfl -@[to_additive with_zero.coe_is_add_hom] +@[to_additive] instance coe_is_mul_hom [has_mul α] : is_mul_hom (coe : α → with_one α) := { map_mul := λ a b, rfl } -attribute [to_additive with_zero.has_add.equations._eqn_1] with_one.has_mul.equations._eqn_1 - +@[to_additive add_monoid] instance [semigroup α] : monoid (with_one α) := { mul_assoc := (option.lift_or_get_assoc _).1, one_mul := (option.lift_or_get_is_left_id _).1, @@ -67,36 +64,25 @@ instance [semigroup α] : monoid (with_one α) := ..with_one.has_one, ..with_one.has_mul } -attribute [to_additive with_zero.add_monoid._proof_1] with_one.monoid._proof_1 -attribute [to_additive with_zero.add_monoid._proof_2] with_one.monoid._proof_2 -attribute [to_additive with_zero.add_monoid._proof_3] with_one.monoid._proof_3 -attribute [to_additive with_zero.add_monoid] with_one.monoid -attribute [to_additive with_zero.add_monoid.equations._eqn_1] with_one.monoid.equations._eqn_1 - +@[to_additive add_comm_monoid] instance [comm_semigroup α] : comm_monoid (with_one α) := { mul_comm := (option.lift_or_get_comm _).1, ..with_one.monoid } -attribute [to_additive with_zero.add_comm_monoid._proof_1] with_one.comm_monoid._proof_1 -attribute [to_additive with_zero.add_comm_monoid._proof_2] with_one.comm_monoid._proof_2 -attribute [to_additive with_zero.add_comm_monoid._proof_3] with_one.comm_monoid._proof_3 -attribute [to_additive with_zero.add_comm_monoid._proof_4] with_one.comm_monoid._proof_4 -attribute [to_additive with_zero.add_comm_monoid] with_one.comm_monoid - section lift -@[to_additive with_zero.lift] +@[to_additive] def lift {β : Type v} [has_one β] (f : α → β) : (with_one α) → β := λ x, option.cases_on x 1 f variables [semigroup α] {β : Type v} [monoid β] (f : α → β) -@[simp, to_additive with_zero.lift_coe] +@[simp, to_additive] lemma lift_coe (x : α) : lift f x = f x := rfl -@[simp, to_additive with_zero.lift_zero] +@[simp, to_additive] lemma lift_one : lift f 1 = 1 := rfl -@[to_additive with_zero.lift_is_add_monoid_hom] +@[to_additive lift_is_add_monoid_hom] instance lift_is_monoid_hom [hf : is_mul_hom f] : is_monoid_hom (lift f) := { map_one := lift_one f, map_mul := λ x y, @@ -104,7 +90,7 @@ instance lift_is_monoid_hom [hf : is_mul_hom f] : is_monoid_hom (lift f) := with_one.cases_on y (by rw [mul_one, lift_one, mul_one]) $ λ y, @is_mul_hom.map_mul α β _ _ f hf x y } -@[to_additive with_zero.lift_unique] +@[to_additive] theorem lift_unique (f : with_one α → β) (hf : f 1 = 1) : f = lift (f ∘ coe) := funext $ λ x, with_one.cases_on x hf $ λ x, rfl @@ -113,18 +99,18 @@ end lift section map -@[to_additive with_zero.map] +@[to_additive] def map {β : Type v} (f : α → β) : with_one α → with_one β := option.map f variables [semigroup α] {β : Type v} [semigroup β] (f : α → β) -@[to_additive with_zero.map_eq] +@[to_additive] lemma map_eq [semigroup α] {β : Type v} [semigroup β] (f : α → β) : map f = lift (coe ∘ f) := funext $ assume x, @with_one.cases_on α (λ x, map f x = lift (coe ∘ f) x) x rfl (λ a, rfl) -@[to_additive with_zero.map_is_add_monoid_hom] +@[to_additive map_is_add_monoid_hom] instance map_is_monoid_hom [is_mul_hom f] : is_monoid_hom (map f) := by rw map_eq; apply with_one.lift_is_monoid_hom diff --git a/src/algebra/group_power.lean b/src/algebra/group_power.lean index 739c204097650..bafe98b2a2250 100644 --- a/src/algebra/group_power.lean +++ b/src/algebra/group_power.lean @@ -41,15 +41,12 @@ variables [monoid α] {β : Type u} [add_monoid β] @[simp] theorem pow_zero (a : α) : a^0 = 1 := rfl @[simp] theorem add_monoid.zero_smul (a : β) : 0 • a = 0 := rfl -attribute [to_additive add_monoid.zero_smul] pow_zero theorem pow_succ (a : α) (n : ℕ) : a^(n+1) = a * a^n := rfl theorem succ_smul (a : β) (n : ℕ) : (n+1)•a = a + n•a := rfl -attribute [to_additive succ_smul] pow_succ @[simp] theorem pow_one (a : α) : a^1 = a := mul_one _ @[simp] theorem add_monoid.one_smul (a : β) : 1•a = a := add_zero _ -attribute [to_additive add_monoid.one_smul] pow_one theorem pow_mul_comm' (a : α) (n : ℕ) : a^n * a = a * a^n := by induction n with n ih; [rw [pow_zero, one_mul, mul_one], @@ -61,63 +58,53 @@ theorem pow_succ' (a : α) (n : ℕ) : a^(n+1) = a^n * a := by rw [pow_succ, pow_mul_comm'] theorem succ_smul' (a : β) (n : ℕ) : (n+1)•a = n•a + a := by rw [succ_smul, smul_add_comm'] -attribute [to_additive succ_smul'] pow_succ' theorem pow_two (a : α) : a^2 = a * a := show a*(a*1)=a*a, by rw mul_one theorem two_smul (a : β) : 2•a = a + a := show a+(a+0)=a+a, by rw add_zero -attribute [to_additive two_smul] pow_two theorem pow_add (a : α) (m n : ℕ) : a^(m + n) = a^m * a^n := by induction n with n ih; [rw [add_zero, pow_zero, mul_one], rw [pow_succ, ← pow_mul_comm', ← mul_assoc, ← ih, ← pow_succ']]; refl theorem add_monoid.add_smul : ∀ (a : β) (m n : ℕ), (m + n)•a = m•a + n•a := @pow_add (multiplicative β) _ -attribute [to_additive add_monoid.add_smul] pow_add @[simp] theorem one_pow (n : ℕ) : (1 : α)^n = (1:α) := by induction n with n ih; [refl, rw [pow_succ, ih, one_mul]] @[simp] theorem add_monoid.smul_zero (n : ℕ) : n•(0 : β) = (0:β) := by induction n with n ih; [refl, rw [succ_smul, ih, zero_add]] -attribute [to_additive add_monoid.smul_zero] one_pow theorem pow_mul (a : α) (m n : ℕ) : a^(m * n) = (a^m)^n := by induction n with n ih; [rw mul_zero, rw [nat.mul_succ, pow_add, pow_succ', ih]]; refl theorem add_monoid.mul_smul' : ∀ (a : β) (m n : ℕ), m * n • a = n•(m•a) := @pow_mul (multiplicative β) _ -attribute [to_additive add_monoid.mul_smul'] pow_mul theorem pow_mul' (a : α) (m n : ℕ) : a^(m * n) = (a^n)^m := by rw [mul_comm, pow_mul] theorem add_monoid.mul_smul (a : β) (m n : ℕ) : m * n • a = m•(n•a) := by rw [mul_comm, add_monoid.mul_smul'] -attribute [to_additive add_monoid.mul_smul] pow_mul' @[simp] theorem add_monoid.smul_one [has_one β] : ∀ n : ℕ, n • (1 : β) = n := nat.eq_cast _ (add_monoid.zero_smul _) (add_monoid.one_smul _) (add_monoid.add_smul _) theorem pow_bit0 (a : α) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _ theorem bit0_smul (a : β) (n : ℕ) : bit0 n • a = n•a + n•a := add_monoid.add_smul _ _ _ -attribute [to_additive bit0_smul] pow_bit0 theorem pow_bit1 (a : α) (n : ℕ) : a ^ bit1 n = a^n * a^n * a := by rw [bit1, pow_succ', pow_bit0] theorem bit1_smul : ∀ (a : β) (n : ℕ), bit1 n • a = n•a + n•a + a := @pow_bit1 (multiplicative β) _ -attribute [to_additive bit1_smul] pow_bit1 theorem pow_mul_comm (a : α) (m n : ℕ) : a^m * a^n = a^n * a^m := by rw [←pow_add, ←pow_add, add_comm] theorem smul_add_comm : ∀ (a : β) (m n : ℕ), m•a + n•a = n•a + m•a := @pow_mul_comm (multiplicative β) _ -attribute [to_additive smul_add_comm] pow_mul_comm @[simp] theorem list.prod_repeat (a : α) (n : ℕ) : (list.repeat a n).prod = a ^ n := by induction n with n ih; [refl, rw [list.repeat_succ, list.prod_cons, ih]]; refl @[simp] theorem list.sum_repeat : ∀ (a : β) (n : ℕ), (list.repeat a n).sum = n • a := @list.prod_repeat (multiplicative β) _ -attribute [to_additive list.sum_repeat] list.prod_repeat @[simp] lemma units.coe_pow (u : units α) (n : ℕ) : ((u ^ n : units α) : α) = u ^ n := by induction n; simp [*, pow_succ] @@ -142,8 +129,6 @@ theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a) end is_add_monoid_hom -attribute [to_additive is_add_monoid_hom.map_smul] is_monoid_hom.map_pow - @[simp] theorem nat.pow_eq_pow (p q : ℕ) : @has_pow.pow _ _ monoid.has_pow p q = p ^ q := by induction q with q ih; [refl, rw [nat.pow_succ, pow_succ, mul_comm, ih]] @@ -162,7 +147,6 @@ by induction n with n ih; [exact (mul_one _).symm, simp only [pow_succ, ih, mul_assoc, mul_left_comm]] theorem add_monoid.smul_add : ∀ (a b : β) (n : ℕ), n•(a + b) = n•a + n•b := @mul_pow (multiplicative β) _ -attribute [to_additive add_monoid.add_smul] mul_pow instance pow.is_monoid_hom (n : ℕ) : is_monoid_hom ((^ n) : α → α) := { map_mul := λ _ _, mul_pow _ _ _, map_one := one_pow _ } @@ -170,8 +154,6 @@ instance pow.is_monoid_hom (n : ℕ) : is_monoid_hom ((^ n) : α → α) := instance add_monoid.smul.is_add_monoid_hom (n : ℕ) : is_add_monoid_hom (add_monoid.smul n : β → β) := { map_add := λ _ _, add_monoid.smul_add _ _ _, map_zero := add_monoid.smul_zero _ } -attribute [to_additive add_monoid.smul.is_add_monoid_hom] pow.is_monoid_hom - end comm_monoid section group @@ -184,7 +166,6 @@ by induction n with n ih; [exact one_inv.symm, rw [pow_succ', pow_succ, ih, mul_inv_rev]] @[simp] theorem add_monoid.neg_smul : ∀ (a : β) (n : ℕ), n•(-a) = -(n•a) := @inv_pow (multiplicative β) _ -attribute [to_additive add_monoid.neg_smul] inv_pow theorem pow_sub (a : α) {m n : ℕ} (h : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ := have h1 : m - n + n = m, from nat.sub_add_cancel h, @@ -192,13 +173,11 @@ have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1], eq_mul_inv_of_mul_eq h2 theorem add_monoid.smul_sub : ∀ (a : β) {m n : ℕ}, m ≥ n → (m - n)•a = m•a - n•a := @pow_sub (multiplicative β) _ -attribute [to_additive add_monoid.smul_sub] inv_pow theorem pow_inv_comm (a : α) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m := by rw inv_pow; exact inv_comm_of_comm (pow_mul_comm _ _ _) theorem add_monoid.smul_neg_comm : ∀ (a : β) (m n : ℕ), m•(-a) + n•a = n•a + m•(-a) := @pow_inv_comm (multiplicative β) _ -attribute [to_additive add_monoid.smul_neg_comm] pow_inv_comm end nat open int @@ -221,33 +200,27 @@ local infix ` •ℕ `:70 := add_monoid.smul @[simp] theorem gpow_coe_nat (a : α) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl @[simp] theorem gsmul_coe_nat (a : β) (n : ℕ) : (n:ℤ) • a = n •ℕ a := rfl -attribute [to_additive gsmul_coe_nat] gpow_coe_nat @[simp] theorem gpow_of_nat (a : α) (n : ℕ) : a ^ of_nat n = a ^ n := rfl @[simp] theorem gsmul_of_nat (a : β) (n : ℕ) : of_nat n • a = n •ℕ a := rfl -attribute [to_additive gsmul_of_nat] gpow_of_nat @[simp] theorem gpow_neg_succ (a : α) (n : ℕ) : a ^ -[1+n] = (a ^ n.succ)⁻¹ := rfl @[simp] theorem gsmul_neg_succ (a : β) (n : ℕ) : -[1+n] • a = - (n.succ •ℕ a) := rfl -attribute [to_additive gsmul_neg_succ] gpow_neg_succ local attribute [ematch] le_of_lt open nat @[simp] theorem gpow_zero (a : α) : a ^ (0:ℤ) = 1 := rfl @[simp] theorem zero_gsmul (a : β) : (0:ℤ) • a = 0 := rfl -attribute [to_additive zero_gsmul] gpow_zero @[simp] theorem gpow_one (a : α) : a ^ (1:ℤ) = a := mul_one _ @[simp] theorem one_gsmul (a : β) : (1:ℤ) • a = a := add_zero _ -attribute [to_additive one_gsmul] gpow_one @[simp] theorem one_gpow : ∀ (n : ℤ), (1 : α) ^ n = 1 | (n : ℕ) := one_pow _ | -[1+ n] := show _⁻¹=(1:α), by rw [_root_.one_pow, one_inv] @[simp] theorem gsmul_zero : ∀ (n : ℤ), n • (0 : β) = 0 := @one_gpow (multiplicative β) _ -attribute [to_additive gsmul_zero] one_gpow @[simp] theorem gpow_neg (a : α) : ∀ (n : ℤ), a ^ -n = (a ^ n)⁻¹ | (n+1:ℕ) := rfl @@ -256,11 +229,9 @@ attribute [to_additive gsmul_zero] one_gpow @[simp] theorem neg_gsmul : ∀ (a : β) (n : ℤ), -n • a = -(n • a) := @gpow_neg (multiplicative β) _ -attribute [to_additive neg_gsmul] gpow_neg theorem gpow_neg_one (x : α) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $ pow_one x theorem neg_one_gsmul (x : β) : (-1:ℤ) • x = -x := congr_arg has_neg.neg $ add_monoid.one_smul x -attribute [to_additive neg_one_gsmul] gpow_neg_one theorem inv_gpow (a : α) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹ | (n : ℕ) := inv_pow a n @@ -297,19 +268,16 @@ theorem gpow_add_one (a : α) (i : ℤ) : a ^ (i + 1) = a ^ i * a := by rw [gpow_add, gpow_one] theorem add_one_gsmul : ∀ (a : β) (i : ℤ), (i + 1) • a = i • a + a := @gpow_add_one (multiplicative β) _ -attribute [to_additive add_one_gsmul] gpow_add_one theorem gpow_one_add (a : α) (i : ℤ) : a ^ (1 + i) = a * a ^ i := by rw [gpow_add, gpow_one] theorem one_add_gsmul : ∀ (a : β) (i : ℤ), (1 + i) • a = a + i • a := @gpow_one_add (multiplicative β) _ -attribute [to_additive one_add_gsmul] gpow_one_add theorem gpow_mul_comm (a : α) (i j : ℤ) : a ^ i * a ^ j = a ^ j * a ^ i := by rw [← gpow_add, ← gpow_add, add_comm] theorem gsmul_add_comm : ∀ (a : β) (i j), i • a + j • a = j • a + i • a := @gpow_mul_comm (multiplicative β) _ -attribute [to_additive gsmul_add_comm] gpow_mul_comm theorem gpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n | (m : ℕ) (n : ℕ) := pow_mul _ _ _ @@ -321,23 +289,19 @@ theorem gpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n show _ = (_⁻¹^_)⁻¹, by rw [inv_pow, inv_inv] theorem gsmul_mul' : ∀ (a : β) (m n : ℤ), m * n • a = n • (m • a) := @gpow_mul (multiplicative β) _ -attribute [to_additive gsmul_mul'] gpow_mul theorem gpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m := by rw [mul_comm, gpow_mul] theorem gsmul_mul (a : β) (m n : ℤ) : m * n • a = m • (n • a) := by rw [mul_comm, gsmul_mul'] -attribute [to_additive gsmul_mul] gpow_mul' theorem gpow_bit0 (a : α) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := gpow_add _ _ _ theorem bit0_gsmul (a : β) (n : ℤ) : bit0 n • a = n • a + n • a := gpow_add _ _ _ -attribute [to_additive bit0_gsmul] gpow_bit0 theorem gpow_bit1 (a : α) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a := by rw [bit1, gpow_add]; simp [gpow_bit0] theorem bit1_gsmul : ∀ (a : β) (n : ℤ), bit1 n • a = n • a + n • a + a := @gpow_bit1 (multiplicative β) _ -attribute [to_additive bit1_gsmul] gpow_bit1 theorem gsmul_neg (a : β) (n : ℤ) : gsmul n (- a) = - gsmul n a := begin @@ -347,7 +311,6 @@ begin { rw [sub_eq_add_neg, add_comm] {occs := occurrences.pos [1]}, simp [ih, add_gsmul, neg_gsmul, -add_comm] } end -attribute [to_additive gsmul_neg] gpow_neg end group @@ -384,7 +347,6 @@ theorem mul_gpow (a b : α) : ∀ n:ℤ, (a * b)^n = a^n * b^n | -[1+ n] := show _⁻¹=_⁻¹*_⁻¹, by rw [mul_pow, mul_inv_rev, mul_comm] theorem gsmul_add : ∀ (a b : β) (n : ℤ), n •ℤ (a + b) = n •ℤ a + n •ℤ b := @mul_gpow (multiplicative β) _ -attribute [to_additive gsmul_add] mul_gpow theorem gsmul_sub : ∀ (a b : β) (n : ℤ), gsmul n (a - b) = gsmul n a - gsmul n b := by simp [gsmul_add, gsmul_neg] @@ -395,8 +357,6 @@ instance gpow.is_group_hom (n : ℤ) : is_group_hom ((^ n) : α → α) := instance gsmul.is_add_group_hom (n : ℤ) : is_add_group_hom (gsmul n : β → β) := { map_add := λ _ _, gsmul_add _ _ n } -attribute [to_additive gsmul.is_add_group_hom] gpow.is_group_hom - end comm_monoid section group diff --git a/src/algebra/pi_instances.lean b/src/algebra/pi_instances.lean index d5acb86557147..6fd375338c3b2 100644 --- a/src/algebra/pi_instances.lean +++ b/src/algebra/pi_instances.lean @@ -23,8 +23,8 @@ instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) := ⟨λ i, instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ i, 1⟩ @[simp] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl -attribute [to_additive pi.has_zero] pi.has_one -attribute [to_additive pi.zero_apply] pi.one_apply +attribute [to_additive] pi.has_one +attribute [to_additive] pi.one_apply instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ x y, λ i, x i + y i⟩ @[simp] lemma add_apply [∀ i, has_add $ f i] : (x + y) i = x i + y i := rfl @@ -32,8 +32,8 @@ instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ x y, instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ x y, λ i, x i * y i⟩ @[simp] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl -attribute [to_additive pi.has_add] pi.has_mul -attribute [to_additive pi.add_apply] pi.mul_apply +attribute [to_additive] pi.has_mul +attribute [to_additive] pi.mul_apply instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ x, λ i, (x i)⁻¹⟩ @[simp] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl @@ -41,8 +41,8 @@ instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ x, λ instance has_neg [∀ i, has_neg $ f i] : has_neg (Π i : I, f i) := ⟨λ x, λ i, -(x i)⟩ @[simp] lemma neg_apply [∀ i, has_neg $ f i] : (-x) i = -x i := rfl -attribute [to_additive pi.has_neg] pi.has_inv -attribute [to_additive pi.neg_apply] pi.inv_apply +attribute [to_additive] pi.has_inv +attribute [to_additive] pi.inv_apply instance has_scalar {α : Type*} [∀ i, has_scalar α $ f i] : has_scalar α (Π i : I, f i) := ⟨λ s x, λ i, s • (x i)⟩ @[simp] lemma smul_apply {α : Type*} [∀ i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl @@ -107,27 +107,27 @@ instance ordered_comm_group [∀ i, ordered_comm_group $ f i] : ordered_comm_gro ..pi.add_comm_group, ..pi.partial_order } -attribute [to_additive pi.add_semigroup] pi.semigroup -attribute [to_additive pi.add_comm_semigroup] pi.comm_semigroup -attribute [to_additive pi.add_monoid] pi.monoid -attribute [to_additive pi.add_comm_monoid] pi.comm_monoid -attribute [to_additive pi.add_group] pi.group -attribute [to_additive pi.add_comm_group] pi.comm_group -attribute [to_additive pi.add_left_cancel_semigroup] pi.left_cancel_semigroup -attribute [to_additive pi.add_right_cancel_semigroup] pi.right_cancel_semigroup +attribute [to_additive add_semigroup] pi.semigroup +attribute [to_additive add_comm_semigroup] pi.comm_semigroup +attribute [to_additive add_monoid] pi.monoid +attribute [to_additive add_comm_monoid] pi.comm_monoid +attribute [to_additive add_group] pi.group +attribute [to_additive add_comm_group] pi.comm_group +attribute [to_additive add_left_cancel_semigroup] pi.left_cancel_semigroup +attribute [to_additive add_right_cancel_semigroup] pi.right_cancel_semigroup -@[to_additive pi.list_sum_apply] +@[to_additive] lemma list_prod_apply {α : Type*} {β : α → Type*} [∀a, monoid (β a)] (a : α) : ∀ (l : list (Πa, β a)), l.prod a = (l.map (λf:Πa, β a, f a)).prod | [] := rfl | (f :: l) := by simp [mul_apply f l.prod a, list_prod_apply l] -@[to_additive pi.multiset_sum_apply] +@[to_additive] lemma multiset_prod_apply {α : Type*} {β : α → Type*} [∀a, comm_monoid (β a)] (a : α) (s : multiset (Πa, β a)) : s.prod a = (s.map (λf:Πa, β a, f a)).prod := quotient.induction_on s $ assume l, begin simp [list_prod_apply a l] end -@[to_additive pi.finset_sum_apply] +@[to_additive] lemma finset_prod_apply {α : Type*} {β : α → Type*} {γ} [∀a, comm_monoid (β a)] (a : α) (s : finset γ) (g : γ → Πa, β a) : s.prod g a = s.prod (λc, g c a) := show (s.val.map g).prod a = (s.val.map (λc, g c a)).prod, @@ -154,44 +154,44 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {p q : α × β} instance [has_add α] [has_add β] : has_add (α × β) := ⟨λp q, (p.1 + q.1, p.2 + q.2)⟩ -@[to_additive prod.has_add] +@[to_additive] instance [has_mul α] [has_mul β] : has_mul (α × β) := ⟨λp q, (p.1 * q.1, p.2 * q.2)⟩ -@[simp, to_additive prod.fst_add] +@[simp, to_additive] lemma fst_mul [has_mul α] [has_mul β] : (p * q).1 = p.1 * q.1 := rfl -@[simp, to_additive prod.snd_add] +@[simp, to_additive] lemma snd_mul [has_mul α] [has_mul β] : (p * q).2 = p.2 * q.2 := rfl -@[simp, to_additive prod.mk_add_mk] +@[simp, to_additive] lemma mk_mul_mk [has_mul α] [has_mul β] (a₁ a₂ : α) (b₁ b₂ : β) : (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂) := rfl instance [has_zero α] [has_zero β] : has_zero (α × β) := ⟨(0, 0)⟩ -@[to_additive prod.has_zero] +@[to_additive] instance [has_one α] [has_one β] : has_one (α × β) := ⟨(1, 1)⟩ -@[simp, to_additive prod.fst_zero] +@[simp, to_additive] lemma fst_one [has_one α] [has_one β] : (1 : α × β).1 = 1 := rfl -@[simp, to_additive prod.snd_zero] +@[simp, to_additive] lemma snd_one [has_one α] [has_one β] : (1 : α × β).2 = 1 := rfl -@[to_additive prod.zero_eq_mk] +@[to_additive] lemma one_eq_mk [has_one α] [has_one β] : (1 : α × β) = (1, 1) := rfl instance [has_neg α] [has_neg β] : has_neg (α × β) := ⟨λp, (- p.1, - p.2)⟩ -@[to_additive prod.has_neg] +@[to_additive] instance [has_inv α] [has_inv β] : has_inv (α × β) := ⟨λp, (p.1⁻¹, p.2⁻¹)⟩ -@[simp, to_additive prod.fst_neg] +@[simp, to_additive] lemma fst_inv [has_inv α] [has_inv β] : (p⁻¹).1 = (p.1)⁻¹ := rfl -@[simp, to_additive prod.snd_neg] +@[simp, to_additive] lemma snd_inv [has_inv α] [has_inv β] : (p⁻¹).2 = (p.2)⁻¹ := rfl -@[to_additive prod.neg_mk] +@[to_additive] lemma inv_mk [has_inv α] [has_inv β] (a : α) (b : β) : (a, b)⁻¹ = (a⁻¹, b⁻¹) := rfl instance [add_semigroup α] [add_semigroup β] : add_semigroup (α × β) := { add_assoc := assume a b c, mk.inj_iff.mpr ⟨add_assoc _ _ _, add_assoc _ _ _⟩, .. prod.has_add } -@[to_additive prod.add_semigroup] +@[to_additive add_semigroup] instance [semigroup α] [semigroup β] : semigroup (α × β) := { mul_assoc := assume a b c, mk.inj_iff.mpr ⟨mul_assoc _ _ _, mul_assoc _ _ _⟩, .. prod.has_mul } @@ -200,7 +200,7 @@ instance [add_monoid α] [add_monoid β] : add_monoid (α × β) := { zero_add := assume a, prod.rec_on a $ λa b, mk.inj_iff.mpr ⟨zero_add _, zero_add _⟩, add_zero := assume a, prod.rec_on a $ λa b, mk.inj_iff.mpr ⟨add_zero _, add_zero _⟩, .. prod.add_semigroup, .. prod.has_zero } -@[to_additive prod.add_monoid] +@[to_additive add_monoid] instance [monoid α] [monoid β] : monoid (α × β) := { one_mul := assume a, prod.rec_on a $ λa b, mk.inj_iff.mpr ⟨one_mul _, one_mul _⟩, mul_one := assume a, prod.rec_on a $ λa b, mk.inj_iff.mpr ⟨mul_one _, mul_one _⟩, @@ -209,7 +209,7 @@ instance [monoid α] [monoid β] : monoid (α × β) := instance [add_group α] [add_group β] : add_group (α × β) := { add_left_neg := assume a, mk.inj_iff.mpr ⟨add_left_neg _, add_left_neg _⟩, .. prod.add_monoid, .. prod.has_neg } -@[to_additive prod.add_group] +@[to_additive add_group] instance [group α] [group β] : group (α × β) := { mul_left_inv := assume a, mk.inj_iff.mpr ⟨mul_left_inv _, mul_left_inv _⟩, .. prod.monoid, .. prod.has_inv } @@ -217,46 +217,46 @@ instance [group α] [group β] : group (α × β) := instance [add_comm_semigroup α] [add_comm_semigroup β] : add_comm_semigroup (α × β) := { add_comm := assume a b, mk.inj_iff.mpr ⟨add_comm _ _, add_comm _ _⟩, .. prod.add_semigroup } -@[to_additive prod.add_comm_semigroup] +@[to_additive add_comm_semigroup] instance [comm_semigroup α] [comm_semigroup β] : comm_semigroup (α × β) := { mul_comm := assume a b, mk.inj_iff.mpr ⟨mul_comm _ _, mul_comm _ _⟩, .. prod.semigroup } instance [add_comm_monoid α] [add_comm_monoid β] : add_comm_monoid (α × β) := { .. prod.add_comm_semigroup, .. prod.add_monoid } -@[to_additive prod.add_comm_monoid] +@[to_additive add_comm_monoid] instance [comm_monoid α] [comm_monoid β] : comm_monoid (α × β) := { .. prod.comm_semigroup, .. prod.monoid } instance [add_comm_group α] [add_comm_group β] : add_comm_group (α × β) := { .. prod.add_comm_semigroup, .. prod.add_group } -@[to_additive prod.add_comm_group] +@[to_additive add_comm_group] instance [comm_group α] [comm_group β] : comm_group (α × β) := { .. prod.comm_semigroup, .. prod.group } -@[to_additive fst.is_add_monoid_hom] +@[to_additive is_add_monoid_hom] lemma fst.is_monoid_hom [monoid α] [monoid β] : is_monoid_hom (prod.fst : α × β → α) := { map_mul := λ _ _, rfl, map_one := rfl } -@[to_additive snd.is_add_monoid_hom] +@[to_additive is_add_monoid_hom] lemma snd.is_monoid_hom [monoid α] [monoid β] : is_monoid_hom (prod.snd : α × β → β) := { map_mul := λ _ _, rfl, map_one := rfl } -@[to_additive fst.is_add_group_hom] +@[to_additive is_add_group_hom] lemma fst.is_group_hom [group α] [group β] : is_group_hom (prod.fst : α × β → α) := { map_mul := λ _ _, rfl } -@[to_additive snd.is_add_group_hom] +@[to_additive is_add_group_hom] lemma snd.is_group_hom [group α] [group β] : is_group_hom (prod.snd : α × β → β) := { map_mul := λ _ _, rfl } attribute [instance] fst.is_monoid_hom fst.is_add_monoid_hom snd.is_monoid_hom snd.is_add_monoid_hom fst.is_group_hom fst.is_add_group_hom snd.is_group_hom snd.is_add_group_hom -@[to_additive prod.fst_sum] +@[to_additive] lemma fst_prod [comm_monoid α] [comm_monoid β] {t : finset γ} {f : γ → α × β} : (t.prod f).1 = t.prod (λc, (f c).1) := (finset.prod_hom prod.fst).symm -@[to_additive prod.snd_sum] +@[to_additive] lemma snd_prod [comm_monoid α] [comm_monoid β] {t : finset γ} {f : γ → α × β} : (t.prod f).2 = t.prod (λc, (f c).2) := (finset.prod_hom prod.snd).symm @@ -350,13 +350,13 @@ instance {r : discrete_field α} [add_comm_group β] [add_comm_group γ] section substructures variables (s : set α) (t : set β) -@[to_additive prod.is_add_submonoid] +@[to_additive is_add_submonoid] instance [monoid α] [monoid β] [is_submonoid s] [is_submonoid t] : is_submonoid (s.prod t) := { one_mem := by rw set.mem_prod; split; apply is_submonoid.one_mem, mul_mem := by intros; rw set.mem_prod at *; split; apply is_submonoid.mul_mem; tauto } -@[to_additive prod.is_add_subgroup] +@[to_additive prod.is_add_subgroup.prod] instance is_subgroup.prod [group α] [group β] [is_subgroup s] [is_subgroup t] : is_subgroup (s.prod t) := { inv_mem := by intros; rw set.mem_prod at *; split; apply is_subgroup.inv_mem; tauto, @@ -364,7 +364,7 @@ instance is_subgroup.prod [group α] [group β] [is_subgroup s] [is_subgroup t] instance is_subring.prod [ring α] [ring β] [is_subring s] [is_subring t] : is_subring (s.prod t) := -{ .. prod.is_submonoid s t, .. prod.is_add_subgroup s t } +{ .. prod.is_submonoid s t, .. prod.is_add_subgroup.prod s t } end substructures @@ -372,7 +372,7 @@ end prod namespace finset -@[to_additive finset.prod_mk_sum] +@[to_additive prod_mk_sum] lemma prod_mk_prod {α β γ : Type*} [comm_monoid α] [comm_monoid β] (s : finset γ) (f : γ → α) (g : γ → β) : (s.prod f, s.prod g) = s.prod (λ x, (f x, g x)) := by haveI := classical.dec_eq γ; exact diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean index 6a039c4813002..0838e3cc55eaa 100644 --- a/src/algebra/pointwise.lean +++ b/src/algebra/pointwise.lean @@ -13,42 +13,43 @@ open function variables {α : Type*} {β : Type*} (f : α → β) -@[to_additive set.pointwise_zero] +@[to_additive] def pointwise_one [has_one α] : has_one (set α) := ⟨{1}⟩ local attribute [instance] pointwise_one -@[simp, to_additive set.mem_pointwise_zero] +@[simp, to_additive] lemma mem_pointwise_one [has_one α] (a : α) : a ∈ (1 : set α) ↔ a = 1 := mem_singleton_iff -@[to_additive set.pointwise_add] +@[to_additive] def pointwise_mul [has_mul α] : has_mul (set α) := ⟨λ s t, {a | ∃ x ∈ s, ∃ y ∈ t, a = x * y}⟩ local attribute [instance] pointwise_one pointwise_mul pointwise_add -@[to_additive set.mem_pointwise_add] +@[to_additive] lemma mem_pointwise_mul [has_mul α] {s t : set α} {a : α} : a ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, a = x * y := iff.rfl -@[to_additive set.add_mem_pointwise_add] +@[to_additive] lemma mul_mem_pointwise_mul [has_mul α] {s t : set α} {a b : α} (ha : a ∈ s) (hb : b ∈ t) : a * b ∈ s * t := ⟨_, ha, _, hb, rfl⟩ -@[to_additive set.pointwise_add_eq_image] +@[to_additive] lemma pointwise_mul_eq_image [has_mul α] {s t : set α} : s * t = (λ x : α × α, x.fst * x.snd) '' s.prod t := set.ext $ λ a, ⟨ by { rintros ⟨_, _, _, _, rfl⟩, exact ⟨(_, _), mem_prod.mpr ⟨‹_›, ‹_›⟩, rfl⟩ }, by { rintros ⟨_, _, rfl⟩, exact ⟨_, (mem_prod.mp ‹_›).1, _, (mem_prod.mp ‹_›).2, rfl⟩ }⟩ -@[to_additive set.pointwise_add_finite] +@[to_additive] lemma pointwise_mul_finite [has_mul α] {s t : set α} (hs : finite s) (ht : finite t) : finite (s * t) := by { rw pointwise_mul_eq_image, apply set.finite_image, exact set.finite_prod hs ht } +@[to_additive pointwise_add_add_semigroup] def pointwise_mul_semigroup [semigroup α] : semigroup (set α) := { mul_assoc := λ _ _ _, set.ext $ λ _, begin @@ -60,20 +61,7 @@ def pointwise_mul_semigroup [semigroup α] : semigroup (set α) := end, ..pointwise_mul } -def pointwise_add_add_semigroup [add_semigroup α] : add_semigroup (set α) := -{ add_assoc := λ _ _ _, set.ext $ λ _, - begin - split, - { rintros ⟨_, ⟨_, _, _, _, rfl⟩, _, _, rfl⟩, - exact ⟨_, ‹_›, _, ⟨_, ‹_›, _, ‹_›, rfl⟩, add_assoc _ _ _⟩ }, - { rintros ⟨_, _, _, ⟨_, _, _, _, rfl⟩, rfl⟩, - exact ⟨_, ⟨_, ‹_›, _, ‹_›, rfl⟩, _, ‹_›, (add_assoc _ _ _).symm⟩ } - end, - ..pointwise_add } - -attribute [to_additive set.pointwise_add_add_semigroup._proof_1] pointwise_mul_semigroup._proof_1 -attribute [to_additive set.pointwise_add_add_semigroup] pointwise_mul_semigroup - +@[to_additive pointwise_add_add_monoid] def pointwise_mul_monoid [monoid α] : monoid (set α) := { one_mul := λ s, set.ext $ λ a, ⟨by {rintros ⟨_, _, _, _, rfl⟩, simp * at *}, @@ -84,51 +72,36 @@ def pointwise_mul_monoid [monoid α] : monoid (set α) := ..pointwise_mul_semigroup, ..pointwise_one } -def pointwise_add_add_monoid [add_monoid α] : add_monoid (set α) := -{ zero_add := λ s, set.ext $ λ a, - ⟨by {rintros ⟨_, _, _, _, rfl⟩, simp * at *}, - λ h, ⟨0, mem_singleton 0, a, h, (zero_add a).symm⟩⟩, - add_zero := λ s, set.ext $ λ a, - ⟨by {rintros ⟨_, _, _, _, rfl⟩, simp * at *}, - λ h, ⟨a, h, 0, mem_singleton 0, (add_zero a).symm⟩⟩, - ..pointwise_add_add_semigroup, - ..pointwise_zero } - -attribute [to_additive set.pointwise_add_add_monoid._proof_1] pointwise_mul_monoid._proof_1 -attribute [to_additive set.pointwise_add_add_monoid._proof_2] pointwise_mul_monoid._proof_2 -attribute [to_additive set.pointwise_add_add_monoid._proof_3] pointwise_mul_monoid._proof_3 -attribute [to_additive set.pointwise_add_add_monoid] pointwise_mul_monoid - local attribute [instance] pointwise_mul_monoid -@[to_additive set.singleton.is_add_hom] +@[to_additive] def singleton.is_mul_hom [has_mul α] : is_mul_hom (singleton : α → set α) := { map_mul := λ x y, set.ext $ λ a, by simp [mem_singleton_iff, mem_pointwise_mul] } -@[to_additive set.singleton.is_add_monoid_hom] +@[to_additive is_add_monoid_hom] def singleton.is_monoid_hom [monoid α] : is_monoid_hom (singleton : α → set α) := { map_one := rfl, ..singleton.is_mul_hom } -@[to_additive set.pointwise_neg] +@[to_additive] def pointwise_inv [has_inv α] : has_inv (set α) := ⟨λ s, {a | a⁻¹ ∈ s}⟩ -@[simp, to_additive set.pointwise_add_empty] +@[simp, to_additive] lemma pointwise_mul_empty [has_mul α] (s : set α) : s * ∅ = ∅ := set.ext $ λ a, ⟨by {rintros ⟨_, _, _, _, rfl⟩, tauto}, false.elim⟩ -@[simp, to_additive set.empty_pointwise_add] +@[simp, to_additive] lemma empty_pointwise_mul [has_mul α] (s : set α) : ∅ * s = ∅ := set.ext $ λ a, ⟨by {rintros ⟨_, _, _, _, rfl⟩, tauto}, false.elim⟩ -@[to_additive set.pointwise_add_subset_add] +@[to_additive] lemma pointwise_mul_subset_mul [has_mul α] {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ * s₂ ⊆ t₁ * t₂ := by {rintros _ ⟨_, _, _, _, rfl⟩, exact ⟨_, h₁ ‹_›, _, h₂ ‹_›, rfl⟩ } -@[to_additive set.pointwise_add_union] +@[to_additive] lemma pointwise_mul_union [has_mul α] (s t u : set α) : s * (t ∪ u) = (s * t) ∪ (s * u) := begin @@ -143,7 +116,7 @@ begin simp * } } end -@[to_additive set.union_pointwise_add] +@[to_additive] lemma union_pointwise_mul [has_mul α] (s t u : set α) : (s ∪ t) * u = (s * u) ∪ (t * u) := begin @@ -158,15 +131,15 @@ begin simp * } } end -@[to_additive set.pointwise_add_eq_Union_add_left] +@[to_additive] lemma pointwise_mul_eq_Union_mul_left [has_mul α] {s t : set α} : s * t = ⋃a∈s, (λx, a * x) '' t := by { ext y; split; simp only [mem_Union]; rintros ⟨a, ha, x, hx, ax⟩; exact ⟨a, ha, x, hx, ax.symm⟩ } -@[to_additive set.pointwise_add_eq_Union_add_right] +@[to_additive] lemma pointwise_mul_eq_Union_mul_right [has_mul α] {s t : set α} : s * t = ⋃a∈t, (λx, x * a) '' s := by { ext y; split; simp only [mem_Union]; rintros ⟨a, ha, x, hx, ax⟩; exact ⟨x, hx, a, ha, ax.symm⟩ } -@[to_additive set.pointwise_add_ne_empty] +@[to_additive] lemma pointwise_mul_ne_empty [has_mul α] {s t : set α} : s ≠ ∅ → t ≠ ∅ → s * t ≠ ∅ := begin simp only [ne_empty_iff_exists_mem], @@ -174,7 +147,7 @@ begin exact ⟨x * y, mul_mem_pointwise_mul hx hy⟩ end -@[simp, to_additive univ_add_univ] +@[simp, to_additive] lemma univ_pointwise_mul_univ [monoid α] : (univ : set α) * univ = univ := begin have : ∀x, ∃a b : α, x = a * b := λx, ⟨x, ⟨1, (mul_one x).symm⟩⟩, @@ -188,7 +161,7 @@ def pointwise_mul_fintype [has_mul α] [decidable_eq α] (s t : set α) [hs : fi def pointwise_add_fintype [has_add α] [decidable_eq α] (s t : set α) [hs : fintype s] [ht : fintype t] : fintype (s + t : set α) := by { rw pointwise_add_eq_image, apply set.fintype_image } -attribute [to_additive set.pointwise_add_fintype] set.pointwise_mul_fintype +attribute [to_additive] set.pointwise_mul_fintype section monoid @@ -217,7 +190,7 @@ open is_mul_hom variables [has_mul α] [has_mul β] (m : α → β) [is_mul_hom m] -@[to_additive is_add_hom.image_add] +@[to_additive] lemma image_pointwise_mul (s t : set α) : m '' (s * t) = m '' s * m '' t := set.ext $ assume y, begin @@ -228,7 +201,7 @@ begin refine ⟨_, ⟨_, ‹_›, _, ‹_›, rfl⟩, map_mul _ _ _⟩ } end -@[to_additive is_add_hom.preimage_add_preimage_subset] +@[to_additive] lemma preimage_pointwise_mul_preimage_subset (s t : set β) : m ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t) := begin rintros _ ⟨_, _, _, _, rfl⟩, diff --git a/src/algebra/punit_instances.lean b/src/algebra/punit_instances.lean index ab74fe62f48bb..37d194c6977c9 100644 --- a/src/algebra/punit_instances.lean +++ b/src/algebra/punit_instances.lean @@ -70,14 +70,11 @@ by refine intros; exact subsingleton.elim _ _ @[simp] lemma zero_eq : (0 : punit) = star := rfl -@[simp] lemma one_eq : (1 : punit) = star := rfl -attribute [to_additive punit.zero_eq] punit.one_eq +@[simp, to_additive] lemma one_eq : (1 : punit) = star := rfl @[simp] lemma add_eq : x + y = star := rfl -@[simp] lemma mul_eq : x * y = star := rfl -attribute [to_additive punit.add_eq] punit.mul_eq +@[simp, to_additive] lemma mul_eq : x * y = star := rfl @[simp] lemma neg_eq : -x = star := rfl -@[simp] lemma inv_eq : x⁻¹ = star := rfl -attribute [to_additive punit.neg_eq] punit.inv_eq +@[simp, to_additive] lemma inv_eq : x⁻¹ = star := rfl @[simp] lemma smul_eq : x • y = star := rfl @[simp] lemma top_eq : (⊤ : punit) = star := rfl @[simp] lemma bot_eq : (⊥ : punit) = star := rfl diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean index 1f75924873883..771cc4f59b191 100644 --- a/src/data/dfinsupp.lean +++ b/src/data/dfinsupp.lean @@ -579,20 +579,19 @@ section prod_and_sum variables {γ : Type w} --- [to_additive dfinsupp.sum] for dfinsupp.prod doesn't work, the equation lemmas are not generated +-- [to_additive sum] for dfinsupp.prod doesn't work, the equation lemmas are not generated /-- `sum f g` is the sum of `g i (f i)` over the support of `f`. -/ def sum [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [add_comm_monoid γ] (f : Π₀ i, β i) (g : Π i, β i → γ) : γ := f.support.sum (λi, g i (f i)) /-- `prod f g` is the product of `g i (f i)` over the support of `f`. -/ -@[to_additive dfinsupp.sum] +@[to_additive] def prod [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ] (f : Π₀ i, β i) (g : Π i, β i → γ) : γ := f.support.prod (λi, g i (f i)) -attribute [to_additive dfinsupp.sum.equations._eqn_1] dfinsupp.prod.equations._eqn_1 -@[to_additive dfinsupp.sum_map_range_index] +@[to_additive] lemma prod_map_range_index {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)] [Π i, decidable_pred (eq (0 : β₁ i))] [Π i, decidable_pred (eq (0 : β₂ i))] [comm_monoid γ] @@ -609,12 +608,12 @@ begin simp [h1] } end -@[to_additive dfinsupp.sum_zero_index] +@[to_additive] lemma prod_zero_index [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ] {h : Π i, β i → γ} : (0 : Π₀ i, β i).prod h = 1 := rfl -@[to_additive dfinsupp.sum_single_index] +@[to_additive] lemma prod_single_index [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ] {i : ι} {b : β i} {h : Π i, β i → γ} (h_zero : h i 0 = 1) : (single i b).prod h = h i b := @@ -624,7 +623,7 @@ begin { simp [dfinsupp.prod, support_single_ne_zero h] } end -@[to_additive dfinsupp.sum_neg_index] +@[to_additive] lemma prod_neg_index [Π i, add_group (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ] {g : Π₀ i, β i} {h : Π i, β i → γ} (h0 : ∀i, h i 0 = 1) : (-g).prod h = g.prod (λi b, h i (- b)) := @@ -664,7 +663,7 @@ finset.sum_add_distrib f.sum (λi b, - h i b) = - f.sum h := finset.sum_hom (@has_neg.neg γ _) -@[to_additive dfinsupp.sum_add_index] +@[to_additive] lemma prod_add_index [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ] {f g : Π₀ i, β i} {h : Π i, β i → γ} (h_zero : ∀i, h i 0 = 1) (h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) : @@ -704,7 +703,7 @@ by simp [@sum_add_index ι β _ γ _ _ _ f (-g) h h_zero h_add]; simp [@sum_neg_index ι β _ γ _ _ _ g h h_zero, h_neg]; simp [@sum_neg ι β _ γ _ _ _ g h] -@[to_additive dfinsupp.sum_finset_sum_index] +@[to_additive] lemma prod_finset_sum_index {γ : Type w} {α : Type x} [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ] [decidable_eq α] @@ -715,7 +714,7 @@ finset.induction_on s (by simp [prod_zero_index]) (by simp [prod_add_index, h_zero, h_add] {contextual := tt}) -@[to_additive dfinsupp.sum_sum_index] +@[to_additive] lemma prod_sum_index {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁} [Π i₁, has_zero (β₁ i₁)] [Π i, decidable_pred (eq (0 : β₁ i))] [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] @@ -735,7 +734,7 @@ begin all_goals { intros, simp } end -@[to_additive dfinsupp.sum_subtype_domain_index] +@[to_additive] lemma prod_subtype_domain_index [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ] {v : Π₀ i, β i} {p : ι → Prop} [decidable_pred p] {h : Π i, β i → γ} (hp : ∀x∈v.support, p x) : diff --git a/src/data/equiv/algebra.lean b/src/data/equiv/algebra.lean index 8d9c61a1a21ae..024ae2c43fdaa 100644 --- a/src/data/equiv/algebra.lean +++ b/src/data/equiv/algebra.lean @@ -44,36 +44,27 @@ namespace equiv section group variables [group α] +@[to_additive] protected def mul_left (a : α) : α ≃ α := { to_fun := λx, a * x, inv_fun := λx, a⁻¹ * x, left_inv := assume x, show a⁻¹ * (a * x) = x, from inv_mul_cancel_left a x, right_inv := assume x, show a * (a⁻¹ * x) = x, from mul_inv_cancel_left a x } -attribute [to_additive equiv.add_left._proof_1] equiv.mul_left._proof_1 -attribute [to_additive equiv.add_left._proof_2] equiv.mul_left._proof_2 -attribute [to_additive equiv.add_left] equiv.mul_left - +@[to_additive] protected def mul_right (a : α) : α ≃ α := { to_fun := λx, x * a, inv_fun := λx, x * a⁻¹, left_inv := assume x, show (x * a) * a⁻¹ = x, from mul_inv_cancel_right x a, right_inv := assume x, show (x * a⁻¹) * a = x, from inv_mul_cancel_right x a } -attribute [to_additive equiv.add_right._proof_1] equiv.mul_right._proof_1 -attribute [to_additive equiv.add_right._proof_2] equiv.mul_right._proof_2 -attribute [to_additive equiv.add_right] equiv.mul_right - +@[to_additive] protected def inv (α) [group α] : α ≃ α := { to_fun := λa, a⁻¹, inv_fun := λa, a⁻¹, left_inv := assume a, inv_inv a, right_inv := assume a, inv_inv a } -attribute [to_additive equiv.neg._proof_1] equiv.inv._proof_1 -attribute [to_additive equiv.neg._proof_2] equiv.inv._proof_2 -attribute [to_additive equiv.neg] equiv.inv - def units_equiv_ne_zero (α : Type*) [field α] : units α ≃ {a : α | a ≠ 0} := ⟨λ a, ⟨a.1, units.ne_zero _⟩, λ a, units.mk0 _ a.2, λ ⟨_, _, _, _⟩, units.ext rfl, λ ⟨_, _⟩, rfl⟩ @@ -223,57 +214,42 @@ end equiv set_option old_structure_cmd true -/-- mul_equiv α β is the type of an equiv α ≃ β which preserves multiplication. -/ -structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β := -(map_mul' : ∀ x y : α, to_fun (x * y) = to_fun x * to_fun y) - /-- add_equiv α β is the type of an equiv α ≃ β which preserves addition. -/ structure add_equiv (α β : Type*) [has_add α] [has_add β] extends α ≃ β := (map_add' : ∀ x y : α, to_fun (x + y) = to_fun x + to_fun y) -attribute [to_additive add_equiv] mul_equiv -attribute [to_additive add_equiv.cases_on] mul_equiv.cases_on -attribute [to_additive add_equiv.has_sizeof_inst] mul_equiv.has_sizeof_inst -attribute [to_additive add_equiv.inv_fun] mul_equiv.inv_fun -attribute [to_additive add_equiv.left_inv] mul_equiv.left_inv -attribute [to_additive add_equiv.mk] mul_equiv.mk -attribute [to_additive add_equiv.mk.inj] mul_equiv.mk.inj -attribute [to_additive add_equiv.mk.inj_arrow] mul_equiv.mk.inj_arrow -attribute [to_additive add_equiv.mk.inj_eq] mul_equiv.mk.inj_eq -attribute [to_additive add_equiv.mk.sizeof_spec] mul_equiv.mk.sizeof_spec -attribute [to_additive add_equiv.map_add'] mul_equiv.map_mul' -attribute [to_additive add_equiv.no_confusion] mul_equiv.no_confusion -attribute [to_additive add_equiv.no_confusion_type] mul_equiv.no_confusion_type -attribute [to_additive add_equiv.rec] mul_equiv.rec -attribute [to_additive add_equiv.rec_on] mul_equiv.rec_on -attribute [to_additive add_equiv.right_inv] mul_equiv.right_inv -attribute [to_additive add_equiv.sizeof] mul_equiv.sizeof -attribute [to_additive add_equiv.to_equiv] mul_equiv.to_equiv -attribute [to_additive add_equiv.to_fun] mul_equiv.to_fun +/-- mul_equiv α β is the type of an equiv α ≃ β which preserves multiplication. -/ +@[to_additive] +structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β := +(map_mul' : ∀ x y : α, to_fun (x * y) = to_fun x * to_fun y) infix ` ≃* `:25 := mul_equiv infix ` ≃+ `:25 := add_equiv namespace mul_equiv -@[to_additive add_equiv.has_coe_to_fun] +@[to_additive] instance {α β} [has_mul α] [has_mul β] : has_coe_to_fun (α ≃* β) := ⟨_, mul_equiv.to_fun⟩ variables [has_mul α] [has_mul β] [has_mul γ] /-- A multiplicative isomorphism preserves multiplication (canonical form). -/ +@[to_additive] def map_mul (f : α ≃* β) : ∀ x y : α, f (x * y) = f x * f y := f.map_mul' /-- A multiplicative isomorphism preserves multiplication (deprecated). -/ +@[to_additive] instance (h : α ≃* β) : is_mul_hom h := ⟨h.map_mul⟩ /-- The identity map is a multiplicative isomorphism. -/ -@[refl] def refl (α : Type*) [has_mul α] : α ≃* α := +@[refl, to_additive] +def refl (α : Type*) [has_mul α] : α ≃* α := { map_mul' := λ _ _,rfl, ..equiv.refl _} /-- The inverse of an isomorphism is an isomorphism. -/ -@[symm] def symm (h : α ≃* β) : β ≃* α := +@[symm, to_additive] +def symm (h : α ≃* β) : β ≃* α := { map_mul' := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin show h.to_equiv (h.to_equiv.symm (n₁ * n₂)) = h ((h.to_equiv.symm n₁) * (h.to_equiv.symm n₂)), @@ -282,27 +258,33 @@ instance (h : α ≃* β) : is_mul_hom h := ⟨h.map_mul⟩ rw [h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply], end, ..h.to_equiv.symm} -@[simp] theorem to_equiv_symm (f : α ≃* β) : f.symm.to_equiv = f.to_equiv.symm := rfl +@[simp, to_additive] +theorem to_equiv_symm (f : α ≃* β) : f.symm.to_equiv = f.to_equiv.symm := rfl /-- Transitivity of multiplication-preserving isomorphisms -/ -@[trans] def trans (h1 : α ≃* β) (h2 : β ≃* γ) : (α ≃* γ) := +@[trans, to_additive] +def trans (h1 : α ≃* β) (h2 : β ≃* γ) : (α ≃* γ) := { map_mul' := λ x y, show h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y), by rw [h1.map_mul, h2.map_mul], ..h1.to_equiv.trans h2.to_equiv } /-- e.right_inv in canonical form -/ -@[simp] def apply_symm_apply (e : α ≃* β) : ∀ (y : β), e (e.symm y) = y := -equiv.apply_symm_apply (e.to_equiv) +@[simp, to_additive] +def apply_symm_apply (e : α ≃* β) : ∀ (y : β), e (e.symm y) = y := +e.to_equiv.apply_symm_apply /-- e.left_inv in canonical form -/ -@[simp] def symm_apply_apply (e : α ≃* β) : ∀ (x : α), e.symm (e x) = x := +@[simp, to_additive] +def symm_apply_apply (e : α ≃* β) : ∀ (x : α), e.symm (e x) = x := equiv.symm_apply_apply (e.to_equiv) /-- a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism) -/ -@[simp] def map_one {α β} [monoid α] [monoid β] (h : α ≃* β) : h 1 = 1 := +@[simp, to_additive] +def map_one {α β} [monoid α] [monoid β] (h : α ≃* β) : h 1 = 1 := by rw [←mul_one (h 1), ←h.apply_symm_apply 1, ←h.map_mul, one_mul] /-- A multiplicative bijection between two monoids is an isomorphism. -/ +@[to_additive to_add_monoid_hom] def to_monoid_hom {α β} [monoid α] [monoid β] (h : α ≃* β) : (α →* β) := { to_fun := h, map_mul' := h.map_mul, @@ -310,124 +292,18 @@ def to_monoid_hom {α β} [monoid α] [monoid β] (h : α ≃* β) : (α →* β /-- A multiplicative bijection between two monoids is a monoid hom (deprecated -- use to_monoid_hom). -/ +@[to_additive is_add_monoid_hom] instance is_monoid_hom {α β} [monoid α] [monoid β] (h : α ≃* β) : is_monoid_hom h := ⟨h.map_one⟩ /-- A multiplicative bijection between two groups is a group hom (deprecated -- use to_monoid_hom). -/ +@[to_additive is_add_group_hom] instance is_group_hom {α β} [group α] [group β] (h : α ≃* β) : is_group_hom h := { map_mul := h.map_mul } end mul_equiv -namespace add_equiv - -variables [has_add α] [has_add β] [has_add γ] - -/-- An additive isomorphism preserves addition (canonical form). -/ -def map_add (f : α ≃+ β) : ∀ x y : α, f (x + y) = f x + f y := f.map_add' - -attribute [to_additive add_equiv.map_add] mul_equiv.map_mul -attribute [to_additive add_equiv.map_add.equations._eqn_1] mul_equiv.map_mul.equations._eqn_1 - -/-- A additive isomorphism preserves multiplication (deprecated). -/ -instance (h : α ≃+ β) : is_add_hom h := ⟨h.map_add⟩ - -/-- The identity map is an additive isomorphism. -/ -@[refl] def refl (α : Type*) [has_add α] : α ≃+ α := -{ map_add' := λ _ _,rfl, -..equiv.refl _} - -attribute [to_additive add_equiv.refl] mul_equiv.refl -attribute [to_additive add_equiv.refl._proof_1] mul_equiv.refl._proof_1 -attribute [to_additive add_equiv.refl._proof_2] mul_equiv.refl._proof_2 -attribute [to_additive add_equiv.refl._proof_3] mul_equiv.refl._proof_3 -attribute [to_additive add_equiv.refl.equations._eqn_1] mul_equiv.refl.equations._eqn_1 - -/-- The inverse of an isomorphism is an isomorphism. -/ -@[symm] def symm (h : α ≃+ β) : β ≃+ α := -{ map_add' := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin - show h.to_equiv (h.to_equiv.symm (n₁ + n₂)) = - h ((h.to_equiv.symm n₁) + (h.to_equiv.symm n₂)), - rw h.map_add, - show _ = h.to_equiv (_) + h.to_equiv (_), - rw [h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply], end, - ..h.to_equiv.symm} - -attribute [to_additive add_equiv.symm] mul_equiv.symm -attribute [to_additive add_equiv.symm._proof_1] mul_equiv.symm._proof_1 -attribute [to_additive add_equiv.symm._proof_2] mul_equiv.symm._proof_2 -attribute [to_additive add_equiv.symm._proof_3] mul_equiv.symm._proof_3 -attribute [to_additive add_equiv.symm.equations._eqn_1] mul_equiv.symm.equations._eqn_1 - -@[simp] theorem to_equiv_symm (f : α ≃+ β) : f.symm.to_equiv = f.to_equiv.symm := rfl - -attribute [to_additive add_equiv.to_equiv_symm] mul_equiv.to_equiv_symm - -/-- Transitivity of addition-preserving isomorphisms -/ -@[trans] def trans (h1 : α ≃+ β) (h2 : β ≃+ γ) : (α ≃+ γ) := -{ map_add' := λ x y, show h2 (h1 (x + y)) = h2 (h1 x) + h2 (h1 y), - by rw [h1.map_add, h2.map_add], - ..h1.to_equiv.trans h2.to_equiv } - -attribute [to_additive add_equiv.trans] mul_equiv.trans -attribute [to_additive add_equiv.trans._proof_1] mul_equiv.trans._proof_1 -attribute [to_additive add_equiv.trans._proof_2] mul_equiv.trans._proof_2 -attribute [to_additive add_equiv.trans._proof_3] mul_equiv.trans._proof_3 -attribute [to_additive add_equiv.trans.equations._eqn_1] mul_equiv.trans.equations._eqn_1 - -/-- e.right_inv in canonical form -/ -def apply_symm_apply (e : α ≃+ β) : ∀ (y : β), e (e.symm y) = y := -equiv.apply_symm_apply (e.to_equiv) - -attribute [to_additive add_equiv.apply_symm_apply] mul_equiv.apply_symm_apply -attribute [to_additive add_equiv.apply_symm_apply.equations._eqn_1] mul_equiv.apply_symm_apply.equations._eqn_1 - -/-- e.left_inv in canonical form -/ -def symm_apply_apply (e : α ≃+ β) : ∀ (x : α), e.symm (e x) = x := -equiv.symm_apply_apply (e.to_equiv) - -attribute [to_additive add_equiv.symm_apply_apply] mul_equiv.symm_apply_apply -attribute [to_additive add_equiv.symm_apply_apply.equations._eqn_1] mul_equiv.symm_apply_apply.equations._eqn_1 - -/-- an additive equiv of monoids sends 0 to 0 (and is hence an `add_monoid` isomorphism) -/ -def map_zero {α β} [add_monoid α] [add_monoid β] (h : α ≃+ β) : h 0 = 0 := -by rw [←add_zero (h 0), ←h.apply_symm_apply 0, ←h.map_add, zero_add] - -attribute [to_additive add_equiv.map_zero] mul_equiv.map_one -attribute [to_additive add_equiv.map_zero.equations._eqn_1] mul_equiv.map_one.equations._eqn_1 - -/-- An additive bijection between two add_monoids is an isomorphism. -/ -def to_add_monoid_hom {α β} [add_monoid α] [add_monoid β] (h : α ≃+ β) : (α →+ β) := -{ to_fun := h, - map_add' := h.map_add, - map_zero' := h.map_zero } - -attribute [to_additive add_equiv.to_add_monoid_hom] mul_equiv.to_monoid_hom -attribute [to_additive add_equiv.to_add_monoid_hom._proof_1] mul_equiv.to_monoid_hom._proof_1 -attribute [to_additive add_equiv.to_add_monoid_hom.equations._eqn_1] - mul_equiv.to_monoid_hom.equations._eqn_1 - -/-- an additive bijection between two add_monoids is an add_monoid hom -(deprecated -- use to_add_monoid_hom) -/ -instance is_add_monoid_hom {α β} [add_monoid α] [add_monoid β] (h : α ≃+ β) : is_add_monoid_hom h := -⟨h.map_zero⟩ - -attribute [to_additive add_equiv.is_add_monoid_hom] mul_equiv.is_monoid_hom -attribute [to_additive add_equiv.is_add_monoid_hom.equations._eqn_1] - mul_equiv.is_monoid_hom.equations._eqn_1 - -/-- An additive bijection between two add_groups is an add_group hom - (deprecated -- use to_monoid_hom). -/ -instance is_add_group_hom {α β} [add_group α] [add_group β] (h : α ≃+ β) : - is_add_group_hom h := { map_add := h.map_add } - -attribute [to_additive add_equiv.is_add_group_hom] mul_equiv.is_group_hom -attribute [to_additive add_equiv.is_add_group_hom.equations._eqn_1] - mul_equiv.is_group_hom.equations._eqn_1 - -end add_equiv - namespace units variables [monoid α] [monoid β] [monoid γ] diff --git a/src/data/finsupp.lean b/src/data/finsupp.lean index dfe7323bb4021..99c9c11b82e81 100644 --- a/src/data/finsupp.lean +++ b/src/data/finsupp.lean @@ -358,25 +358,24 @@ if_neg h end erase --- [to_additive finsupp.sum] for finsupp.prod doesn't work, the equation lemmas are not generated +-- [to_additive sum] for finsupp.prod doesn't work, the equation lemmas are not generated /-- `sum f g` is the sum of `g a (f a)` over the support of `f`. -/ def sum [has_zero β] [add_comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ := f.support.sum (λa, g a (f a)) /-- `prod f g` is the product of `g a (f a)` over the support of `f`. -/ -@[to_additive finsupp.sum] +@[to_additive] def prod [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ := f.support.prod (λa, g a (f a)) -attribute [to_additive finsupp.sum.equations._eqn_1] finsupp.prod.equations._eqn_1 -@[to_additive finsupp.sum_map_range_index] +@[to_additive] lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ] [decidable_eq β₂] {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {h : α → β₂ → γ} (h0 : ∀a, h a 0 = 1) : (map_range f hf g).prod h = g.prod (λa b, h a (f b)) := finset.prod_subset support_map_range $ λ _ _ H, by rw [not_mem_support_iff.1 H, h0] -@[to_additive finsupp.sum_zero_index] +@[to_additive] lemma prod_zero_index [add_comm_monoid β] [comm_monoid γ] {h : α → β → γ} : (0 : α →₀ β).prod h = 1 := rfl @@ -393,7 +392,7 @@ end nat_sub section add_monoid variables [add_monoid β] -@[to_additive finsupp.sum_single_index] +@[to_additive] lemma prod_single_index [comm_monoid γ] {a : α} {b : β} {h : α → β → γ} (h_zero : h a 0 = 1) : (single a b).prod h = h a b := begin @@ -517,7 +516,7 @@ lemma single_sum [has_zero γ] [add_comm_monoid β] [decidable_eq α] [decidable single_finset_sum _ _ _ -@[to_additive finsupp.sum_neg_index] +@[to_additive] lemma prod_neg_index [add_group β] [comm_monoid γ] {g : α →₀ β} {h : α → β → γ} (h0 : ∀a, h a 0 = 1) : (-g).prod h = g.prod (λa b, h a (- b)) := @@ -589,7 +588,7 @@ end, ext $ assume a, by simp only [sum_apply, single_apply, this, insert_empty_eq_singleton, sum_singleton, if_pos] -@[to_additive finsupp.sum_add_index] +@[to_additive] lemma prod_add_index [add_comm_monoid β] [comm_monoid γ] {f g : α →₀ β} {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) : (f + g).prod h = f.prod h * g.prod h := @@ -627,7 +626,7 @@ calc (f - g).sum h = (f + - g).sum h : rfl ... = f.sum h + - g.sum h : by simp only [sum_add_index h_zero h_add, sum_neg_index h_zero, h_neg, sum_neg] ... = f.sum h - g.sum h : rfl -@[to_additive finsupp.sum_finset_sum_index] +@[to_additive] lemma prod_finset_sum_index [add_comm_monoid β] [comm_monoid γ] [decidable_eq ι] {s : finset ι} {g : ι → α →₀ β} {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) : @@ -635,7 +634,7 @@ lemma prod_finset_sum_index [add_comm_monoid β] [comm_monoid γ] [decidable_eq finset.induction_on s rfl $ λ a s has ih, by rw [prod_insert has, ih, sum_insert has, prod_add_index h_zero h_add] -@[to_additive finsupp.sum_sum_index] +@[to_additive] lemma prod_sum_index [decidable_eq α₁] [add_comm_monoid β₁] [add_comm_monoid β] [comm_monoid γ] {f : α₁ →₀ β₁} {g : α₁ → β₁ → α →₀ β} @@ -745,7 +744,7 @@ finset.subset.trans support_sum $ finset.subset.trans (finset.bind_mono $ assume a ha, support_single_subset) $ by rw [finset.bind_singleton]; exact subset.refl _ -@[to_additive finsupp.sum_map_domain_index] +@[to_additive] lemma prod_map_domain_index [comm_monoid γ] {f : α → α₂} {s : α →₀ β} {h : α₂ → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) : (s.map_domain f).prod h = s.prod (λa b, h (f a) b) := @@ -947,7 +946,7 @@ rfl @[simp] lemma subtype_domain_zero : subtype_domain p (0 : α →₀ β) = 0 := rfl -@[to_additive finsupp.sum_subtype_domain_index] +@[to_additive] lemma prod_subtype_domain_index [comm_monoid γ] {v : α →₀ β} {h : α → β → γ} (hp : ∀x∈v.support, p x) : (v.subtype_domain p).prod (λa b, h a.1 b) = v.prod h := diff --git a/src/data/fintype.lean b/src/data/fintype.lean index d27ebeebe22a0..9d0e9a90a76b0 100644 --- a/src/data/fintype.lean +++ b/src/data/fintype.lean @@ -519,7 +519,7 @@ begin simp [this], exact setoid.refl _ end -@[simp, to_additive finset.sum_attach_univ] +@[simp, to_additive] lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) : univ.attach.prod (λ x, f x) = univ.prod (λ x, f ⟨x, (mem_univ _)⟩) := prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩) diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index 3d290549d8d3c..20813378b8e10 100644 --- a/src/data/list/basic.lean +++ b/src/data/list/basic.lean @@ -1374,32 +1374,31 @@ end mfoldl_mfoldr /- sum -/ -attribute [to_additive list.sum] list.prod -attribute [to_additive list.sum.equations._eqn_1] list.prod.equations._eqn_1 +attribute [to_additive] list.prod section monoid variables [monoid α] {l l₁ l₂ : list α} {a : α} -@[simp, to_additive list.sum_nil] +@[simp, to_additive] theorem prod_nil : ([] : list α).prod = 1 := rfl -@[simp, to_additive list.sum_cons] +@[simp, to_additive] theorem prod_cons : (a::l).prod = a * l.prod := calc (a::l).prod = foldl (*) (a * 1) l : by simp only [list.prod, foldl_cons, one_mul, mul_one] ... = _ : foldl_assoc -@[simp, to_additive list.sum_append] +@[simp, to_additive] theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list.prod] ... = l₁.prod * l₂.prod : foldl_assoc -@[simp, to_additive list.sum_join] +@[simp, to_additive] theorem prod_join {l : list (list α)} : l.join.prod = (l.map list.prod).prod := by induction l; [refl, simp only [*, list.join, map, prod_append, prod_cons]] end monoid -@[simp, to_additive list.sum_erase] +@[simp, to_additive] theorem prod_erase [decidable_eq α] [comm_monoid α] {a} : Π {l : list α}, a ∈ l → a * (l.erase a).prod = l.prod | (b::l) h := @@ -2645,7 +2644,7 @@ lemma rel_filter_map {f : α → option γ} {q : β → option δ} : | _, _, option.rel.some h := forall₂.cons h (rel_filter_map @hfg h₂) end -@[to_additive list.rel_sum] +@[to_additive] lemma rel_prod [monoid α] [monoid β] (h : r 1 1) (hf : (r ⇒ r ⇒ r) (*) (*)) : (forall₂ r ⇒ r) prod prod := assume a b, rel_foldl (assume a b, hf) h @@ -4321,7 +4320,7 @@ nodup_pmap (λ _ _ _ _, fin.veq_of_eq) (nodup_range _) @[simp] lemma length_fin_range (n : ℕ) : (fin_range n).length = n := by rw [fin_range, length_pmap, length_range] -@[to_additive list.sum_range_succ] +@[to_additive] theorem prod_range_succ {α : Type u} [monoid α] (f : ℕ → α) (n : ℕ) : ((range n.succ).map f).prod = ((range n).map f).prod * f n := by rw [range_concat, map_append, map_singleton, diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean index 2145735c14b96..501340baddafd 100644 --- a/src/data/list/perm.lean +++ b/src/data/list/perm.lean @@ -374,11 +374,11 @@ section comm_monoid open list variable [comm_monoid α] -@[to_additive list.sum_eq_of_perm] +@[to_additive] lemma prod_eq_of_perm {l₁ l₂ : list α} (h : perm l₁ l₂) : prod l₁ = prod l₂ := by induction h; simp [*, mul_left_comm] -@[to_additive list.sum_reverse] +@[to_additive] lemma prod_reverse (l : list α) : prod l.reverse = prod l := prod_eq_of_perm $ reverse_perm l diff --git a/src/data/multiset.lean b/src/data/multiset.lean index f29031abdd4e3..f6e6b09e9ef76 100644 --- a/src/data/multiset.lean +++ b/src/data/multiset.lean @@ -702,35 +702,34 @@ theorem foldl_swap (f : β → α → β) (H : right_commutative f) (b : β) (s /-- Product of a multiset given a commutative monoid structure on `α`. `prod {a, b, c} = a * b * c` -/ +@[to_additive] def prod [comm_monoid α] : multiset α → α := foldr (*) (λ x y z, by simp [mul_left_comm]) 1 -attribute [to_additive multiset.sum._proof_1] prod._proof_1 -attribute [to_additive multiset.sum] prod -@[to_additive multiset.sum_eq_foldr] +@[to_additive] theorem prod_eq_foldr [comm_monoid α] (s : multiset α) : prod s = foldr (*) (λ x y z, by simp [mul_left_comm]) 1 s := rfl -@[to_additive multiset.sum_eq_foldl] +@[to_additive] theorem prod_eq_foldl [comm_monoid α] (s : multiset α) : prod s = foldl (*) (λ x y z, by simp [mul_right_comm]) 1 s := (foldr_swap _ _ _ _).trans (by simp [mul_comm]) -@[simp, to_additive multiset.coe_sum] +@[simp, to_additive] theorem coe_prod [comm_monoid α] (l : list α) : prod ↑l = l.prod := prod_eq_foldl _ -@[simp, to_additive multiset.sum_zero] +@[simp, to_additive] theorem prod_zero [comm_monoid α] : @prod α _ 0 = 1 := rfl -@[simp, to_additive multiset.sum_cons] +@[simp, to_additive] theorem prod_cons [comm_monoid α] (a : α) (s) : prod (a :: s) = a * prod s := foldr_cons _ _ _ _ _ -@[to_additive multiset.sum_singleton] +@[to_additive] theorem prod_singleton [comm_monoid α] (a : α) : prod (a :: 0) = a := by simp -@[simp, to_additive multiset.sum_add] +@[simp, to_additive] theorem prod_add [comm_monoid α] (s t : multiset α) : prod (s + t) = prod s * prod t := quotient.induction_on₂ s t $ λ l₁ l₂, by simp @@ -747,7 +746,7 @@ lemma prod_smul {α : Type*} [comm_monoid α] (m : multiset α) : by simp [repeat, list.prod_repeat] @[simp] theorem sum_repeat [add_comm_monoid α] : ∀ (a : α) (n : ℕ), sum (multiset.repeat a n) = n • a := @prod_repeat (multiplicative α) _ -attribute [to_additive multiset.sum_repeat] prod_repeat +attribute [to_additive] prod_repeat @[simp] lemma prod_map_one [comm_monoid γ] {m : multiset α} : prod (m.map (λa, (1 : γ))) = (1 : γ) := @@ -755,9 +754,9 @@ multiset.induction_on m (by simp) (by simp) @[simp] lemma sum_map_zero [add_comm_monoid γ] {m : multiset α} : sum (m.map (λa, (0 : γ))) = (0 : γ) := multiset.induction_on m (by simp) (by simp) -attribute [to_additive multiset.sum_map_zero] prod_map_one +attribute [to_additive] prod_map_one -@[simp, to_additive multiset.sum_map_add] +@[simp, to_additive] lemma prod_map_mul [comm_monoid γ] {m : multiset α} {f g : α → γ} : prod (m.map $ λa, f a * g a) = prod (m.map f) * prod (m.map g) := multiset.induction_on m (by simp) (assume a m ih, by simp [ih]; cc) @@ -769,7 +768,7 @@ multiset.induction_on m (by simp) (assume a m ih, by simp [ih]) lemma sum_map_sum_map [add_comm_monoid γ] : ∀ (m : multiset α) (n : multiset β) {f : α → β → γ}, sum (m.map $ λa, sum $ n.map $ λb, f a b) = sum (n.map $ λb, sum $ m.map $ λa, f a b) := @prod_map_prod_map _ _ (multiplicative γ) _ -attribute [to_additive multiset.sum_map_sum_map] prod_map_prod_map +attribute [to_additive] prod_map_prod_map lemma sum_map_mul_left [semiring β] {b : β} {s : multiset α} {f : α → β} : sum (s.map (λa, b * f a)) = b * sum (s.map f) := @@ -791,7 +790,7 @@ lemma sum_hom [add_comm_monoid α] [add_comm_monoid β] (f : α → β) [is_add_ (s.map f).sum = f s.sum := multiset.induction_on s (by simp [is_add_monoid_hom.map_zero f]) (by simp [is_add_monoid_hom.map_add f] {contextual := tt}) -attribute [to_additive multiset.sum_hom] multiset.prod_hom +attribute [to_additive] multiset.prod_hom lemma le_sum_of_subadditive [add_comm_monoid α] [ordered_comm_monoid β] (f : α → β) (h_zero : f 0 = 0) (h_add : ∀x y, f (x + y) ≤ f x + f y) (s : multiset α) : @@ -896,7 +895,7 @@ lemma bind_map_comm (m : multiset α) (n : multiset β) {f : α → β → γ} : (bind m $ λa, n.map $ λb, f a b) = (bind n $ λb, m.map $ λa, f a b) := multiset.induction_on m (by simp) (by simp {contextual := tt}) -@[simp, to_additive multiset.sum_bind] +@[simp, to_additive] lemma prod_bind [comm_monoid β] (s : multiset α) (t : α → multiset β) : prod (bind s t) = prod (s.map $ λa, prod (t a)) := multiset.induction_on s (by simp) (assume a s ih, by simp [ih, cons_bind]) diff --git a/src/data/mv_polynomial.lean b/src/data/mv_polynomial.lean index 968658559c2c9..d8b8fd44bf88f 100644 --- a/src/data/mv_polynomial.lean +++ b/src/data/mv_polynomial.lean @@ -362,7 +362,7 @@ end eval₂ f g (s.sum p) = s.sum (λ x, eval₂ f g $ p x) := (finset.sum_hom _).symm -attribute [to_additive mv_polynomial.eval₂_sum] eval₂_prod +attribute [to_additive] eval₂_prod lemma eval₂_assoc [decidable_eq γ] (q : γ → mv_polynomial σ α) (p : mv_polynomial γ α) : eval₂ f (λ t, eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p) := diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean index 5e9d3cb3fe935..5c6623bc191ab 100644 --- a/src/data/set/finite.lean +++ b/src/data/set/finite.lean @@ -478,7 +478,7 @@ suffices f '' (f ⁻¹' ↑s) = ↑s, by simpa, end preimage -@[to_additive finset.sum_preimage] +@[to_additive] lemma prod_preimage [comm_monoid β] (f : α → γ) (s : finset γ) (hf : set.bij_on f (f ⁻¹' ↑s) ↑s) (g : γ → β) : (preimage s (set.inj_on_of_bij_on hf)).prod (g ∘ f) = s.prod g := diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean index e23ab6f7a6ec9..5a9fb7b1c9091 100644 --- a/src/group_theory/coset.lean +++ b/src/group_theory/coset.lean @@ -10,11 +10,9 @@ variable {α : Type*} @[to_additive left_add_coset] def left_coset [has_mul α] (a : α) (s : set α) : set α := (λ x, a * x) '' s -attribute [to_additive left_add_coset.equations._eqn_1] left_coset.equations._eqn_1 @[to_additive right_add_coset] def right_coset [has_mul α] (s : set α) (a : α) : set α := (λ x, x * a) '' s -attribute [to_additive right_add_coset.equations._eqn_1] right_coset.equations._eqn_1 local infix ` *l `:70 := left_coset local infix ` +l `:70 := left_add_coset @@ -140,8 +138,11 @@ theorem normal_iff_eq_cosets : normal_subgroup s ↔ ∀ g, g *l s = s *r g := end coset_subgroup +run_cmd to_additive.map_namespace `quotient_group `quotient_add_group + namespace quotient_group +@[to_additive] def left_rel [group α] (s : set α) [is_subgroup s] : setoid α := ⟨λ x y, x⁻¹ * y ∈ s, assume x, by simp [is_submonoid.one_mem], @@ -151,49 +152,40 @@ def left_rel [group α] (s : set α) [is_subgroup s] : setoid α := assume x y z hxy hyz, have x⁻¹ * y * (y⁻¹ * z) ∈ s, from is_submonoid.mul_mem hxy hyz, by simpa [mul_assoc] using this⟩ -attribute [to_additive quotient_add_group.left_rel._proof_1] left_rel._proof_1 -attribute [to_additive quotient_add_group.left_rel] left_rel -attribute [to_additive quotient_add_group.left_rel.equations._eqn_1] left_rel.equations._eqn_1 /-- `quotient s` is the quotient type representing the left cosets of `s`. If `s` is a normal subgroup, `quotient s` is a group -/ +@[to_additive] def quotient [group α] (s : set α) [is_subgroup s] : Type* := quotient (left_rel s) -attribute [to_additive quotient_add_group.quotient] quotient -attribute [to_additive quotient_add_group.quotient.equations._eqn_1] quotient.equations._eqn_1 variables [group α] {s : set α} [is_subgroup s] -@[to_additive quotient_add_group.mk] +@[to_additive] def mk (a : α) : quotient s := quotient.mk' a -attribute [to_additive quotient_add_group.mk.equations._eqn_1] mk.equations._eqn_1 -@[elab_as_eliminator, to_additive quotient_add_group.induction_on] +@[elab_as_eliminator, to_additive] lemma induction_on {C : quotient s → Prop} (x : quotient s) (H : ∀ z, C (quotient_group.mk z)) : C x := quotient.induction_on' x H -attribute [elab_as_eliminator] quotient_add_group.induction_on -@[to_additive quotient_add_group.has_coe] +@[to_additive] instance : has_coe α (quotient s) := ⟨mk⟩ -attribute [to_additive quotient_add_group.has_coe.equations._eqn_1] has_coe.equations._eqn_1 -@[elab_as_eliminator, to_additive quotient_add_group.induction_on'] +@[elab_as_eliminator, to_additive] lemma induction_on' {C : quotient s → Prop} (x : quotient s) (H : ∀ z : α, C z) : C x := quotient.induction_on' x H -attribute [elab_as_eliminator] quotient_add_group.induction_on' -@[to_additive quotient_add_group.inhabited] +@[to_additive] instance [group α] (s : set α) [is_subgroup s] : inhabited (quotient s) := ⟨((1 : α) : quotient s)⟩ -attribute [to_additive quotient_add_group.inhabited.equations._eqn_1] inhabited.equations._eqn_1 @[to_additive quotient_add_group.eq] protected lemma eq {a b : α} : (a : quotient s) = b ↔ a⁻¹ * b ∈ s := quotient.eq' -@[to_additive quotient_add_group.eq_class_eq_left_coset] +@[to_additive] lemma eq_class_eq_left_coset [group α] (s : set α) [is_subgroup s] (g : α) : {x : α | (x : quotient s) = g} = left_coset g s := set.ext $ λ z, by rw [mem_left_coset_iff, set.mem_set_of_eq, eq_comm, quotient_group.eq] @@ -204,22 +196,14 @@ namespace is_subgroup open quotient_group variables [group α] {s : set α} +@[to_additive] def left_coset_equiv_subgroup (g : α) : left_coset g s ≃ s := ⟨λ x, ⟨g⁻¹ * x.1, (mem_left_coset_iff _).1 x.2⟩, λ x, ⟨g * x.1, x.1, x.2, rfl⟩, λ ⟨x, hx⟩, subtype.eq $ by simp, λ ⟨g, hg⟩, subtype.eq $ by simp⟩ -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_2] left_coset_equiv_subgroup._match_2 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_1] left_coset_equiv_subgroup._match_1 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_4] left_coset_equiv_subgroup._proof_4 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_3] left_coset_equiv_subgroup._proof_3 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_2] left_coset_equiv_subgroup._proof_2 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_1] left_coset_equiv_subgroup._proof_1 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup] left_coset_equiv_subgroup -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup.equations._eqn_1] left_coset_equiv_subgroup.equations._eqn_1 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_1.equations._eqn_1] left_coset_equiv_subgroup._match_1.equations._eqn_1 -attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_2.equations._eqn_1] left_coset_equiv_subgroup._match_2.equations._eqn_1 +@[to_additive] noncomputable def group_equiv_quotient_times_subgroup (hs : is_subgroup s) : α ≃ quotient s × s := calc α ≃ Σ L : quotient s, {x : α // (x : quotient s)= L} : @@ -234,10 +218,6 @@ calc α ≃ Σ L : quotient s, {x : α // (x : quotient s)= L} : equiv.sigma_congr_right (λ L, left_coset_equiv_subgroup _) ... ≃ quotient s × s : equiv.sigma_equiv_prod _ _ -attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup._proof_2] group_equiv_quotient_times_subgroup._proof_2 -attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup._proof_1] group_equiv_quotient_times_subgroup._proof_1 -attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup] group_equiv_quotient_times_subgroup -attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup.equations._eqn_1] group_equiv_quotient_times_subgroup.equations._eqn_1 end is_subgroup diff --git a/src/group_theory/perm/sign.lean b/src/group_theory/perm/sign.lean index e469926511817..9220d4f48909c 100644 --- a/src/group_theory/perm/sign.lean +++ b/src/group_theory/perm/sign.lean @@ -707,4 +707,4 @@ lemma finset.sum_univ_perm [fintype α] [add_comm_monoid β] {f : α → β} (σ (univ : finset α).sum f = univ.sum (λ z, f (σ z)) := @finset.prod_univ_perm _ (multiplicative β) _ _ f σ -attribute [to_additive finset.sum_univ_perm] finset.prod_univ_perm +attribute [to_additive] finset.prod_univ_perm diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean index 20576959715b5..2e44d8241c74f 100644 --- a/src/group_theory/quotient_group.lean +++ b/src/group_theory/quotient_group.lean @@ -13,6 +13,7 @@ namespace quotient_group variables {G : Type u} [group G] (N : set G) [normal_subgroup N] {H : Type v} [group H] +@[to_additive quotient_add_group.add_group] instance : group (quotient N) := { one := (1 : G), mul := λ a b, quotient.lift_on₂' a b @@ -37,21 +38,12 @@ instance : group (quotient N) := end), mul_left_inv := λ a, quotient.induction_on' a (λ a, congr_arg mk (mul_left_inv a)) } -attribute [to_additive quotient_add_group.add_group._proof_6] quotient_group.group._proof_6 -attribute [to_additive quotient_add_group.add_group._proof_5] quotient_group.group._proof_5 -attribute [to_additive quotient_add_group.add_group._proof_4] quotient_group.group._proof_4 -attribute [to_additive quotient_add_group.add_group._proof_3] quotient_group.group._proof_3 -attribute [to_additive quotient_add_group.add_group._proof_2] quotient_group.group._proof_2 -attribute [to_additive quotient_add_group.add_group._proof_1] quotient_group.group._proof_1 -attribute [to_additive quotient_add_group.add_group] quotient_group.group -attribute [to_additive quotient_add_group.quotient.equations._eqn_1] quotient_group.quotient.equations._eqn_1 -attribute [to_additive quotient_add_group.add_group.equations._eqn_1] quotient_group.group.equations._eqn_1 +@[to_additive quotient_add_group.is_add_group_hom] instance : is_group_hom (mk : G → quotient N) := { map_mul := λ _ _, rfl } -attribute [to_additive quotient_add_group.is_add_group_hom] quotient_group.is_group_hom -attribute [to_additive quotient_add_group.is_add_group_hom.equations._eqn_1] quotient_group.is_group_hom.equations._eqn_1 -@[simp] lemma ker_mk : +@[simp, to_additive quotient_add_group.ker_mk] +lemma ker_mk : is_group_hom.ker (quotient_group.mk : G → quotient_group.quotient N) = N := begin ext g, @@ -59,54 +51,47 @@ begin show (((1 : G) : quotient_group.quotient N)) = g ↔ _, rw [quotient_group.eq, one_inv, one_mul], end -attribute [to_additive quotient_add_group.ker_mk] quotient_group.ker_mk +@[to_additive quotient_add_group.add_comm_group] instance {G : Type*} [comm_group G] (s : set G) [is_subgroup s] : comm_group (quotient s) := { mul_comm := λ a b, quotient.induction_on₂' a b (λ a b, congr_arg mk (mul_comm a b)), ..@quotient_group.group _ _ s (normal_subgroup_of_comm_group s) } -attribute [to_additive quotient_add_group.add_comm_group._proof_6] quotient_group.comm_group._proof_6 -attribute [to_additive quotient_add_group.add_comm_group._proof_5] quotient_group.comm_group._proof_5 -attribute [to_additive quotient_add_group.add_comm_group._proof_4] quotient_group.comm_group._proof_4 -attribute [to_additive quotient_add_group.add_comm_group._proof_3] quotient_group.comm_group._proof_3 -attribute [to_additive quotient_add_group.add_comm_group._proof_2] quotient_group.comm_group._proof_2 -attribute [to_additive quotient_add_group.add_comm_group._proof_1] quotient_group.comm_group._proof_1 -attribute [to_additive quotient_add_group.add_comm_group] quotient_group.comm_group -attribute [to_additive quotient_add_group.add_comm_group.equations._eqn_1] quotient_group.comm_group.equations._eqn_1 - -@[simp] lemma coe_one : ((1 : G) : quotient N) = 1 := rfl -@[simp] lemma coe_mul (a b : G) : ((a * b : G) : quotient N) = a * b := rfl -@[simp] lemma coe_inv (a : G) : ((a⁻¹ : G) : quotient N) = a⁻¹ := rfl + +@[simp, to_additive quotient_add_group.coe_zero] +lemma coe_one : ((1 : G) : quotient N) = 1 := rfl + +@[simp, to_additive quotient_add_group.coe_add] +lemma coe_mul (a b : G) : ((a * b : G) : quotient N) = a * b := rfl + +@[simp, to_additive quotient_add_group.coe_neg] +lemma coe_inv (a : G) : ((a⁻¹ : G) : quotient N) = a⁻¹ := rfl + @[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : quotient N) = a ^ n := @is_group_hom.map_pow _ _ _ _ mk _ a n -attribute [to_additive quotient_add_group.coe_zero] coe_one -attribute [to_additive quotient_add_group.coe_add] coe_mul -attribute [to_additive quotient_add_group.coe_neg] coe_inv - @[simp] lemma coe_gpow (a : G) (n : ℤ) : ((a ^ n : G) : quotient N) = a ^ n := @is_group_hom.map_gpow _ _ _ _ mk _ a n local notation ` Q ` := quotient N +@[to_additive quotient_add_group.lift] def lift (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (q : Q) : H := q.lift_on' φ $ assume a b (hab : a⁻¹ * b ∈ N), (calc φ a = φ a * 1 : (mul_one _).symm ... = φ a * φ (a⁻¹ * b) : HN (a⁻¹ * b) hab ▸ rfl ... = φ (a * (a⁻¹ * b)) : (is_mul_hom.map_mul φ a (a⁻¹ * b)).symm ... = φ b : by rw mul_inv_cancel_left) -attribute [to_additive quotient_add_group.lift._proof_1] lift._proof_1 -attribute [to_additive quotient_add_group.lift] lift -attribute [to_additive quotient_add_group.lift.equations._eqn_1] lift.equations._eqn_1 -@[simp] lemma lift_mk {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) : +@[simp, to_additive quotient_add_group.lift_mk] +lemma lift_mk {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) : lift N φ HN (g : Q) = φ g := rfl -attribute [to_additive quotient_add_group.lift_mk] lift_mk -@[simp] lemma lift_mk' {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) : +@[simp, to_additive quotient_add_group.lift_mk'] +lemma lift_mk' {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) : lift N φ HN (mk g : Q) = φ g := rfl -attribute [to_additive quotient_add_group.lift_mk'] lift_mk' +@[to_additive quotient_add_group.map] def map (M : set H) [normal_subgroup M] (f : G → H) [is_group_hom f] (h : N ⊆ f ⁻¹' M) : quotient N → quotient M := begin @@ -118,17 +103,12 @@ begin exact h hx, end -attribute [to_additive quotient_add_group.map._proof_1] map._proof_1 -attribute [to_additive quotient_add_group.map._proof_2] map._proof_2 -attribute [to_additive quotient_add_group.map] map - variables (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1) +@[to_additive quotient_add_group.is_add_group_hom_quotient_lift] instance is_group_hom_quotient_lift : is_group_hom (lift N φ HN) := { map_mul := λ q r, quotient.induction_on₂' q r $ is_mul_hom.map_mul φ } -attribute [to_additive quotient_add_group.is_add_group_hom_quotient_lift] quotient_group.is_group_hom_quotient_lift -attribute [to_additive quotient_add_group.is_add_group_hom_quotient_lift.equations._eqn_1] quotient_group.is_group_hom_quotient_lift.equations._eqn_1 @[to_additive quotient_add_group.map_is_add_group_hom] instance map_is_group_hom (M : set H) [normal_subgroup M] @@ -138,14 +118,10 @@ quotient_group.is_group_hom_quotient_lift _ _ _ open function is_group_hom /-- The induced map from the quotient by the kernel to the codomain. -/ +@[to_additive quotient_add_group.ker_lift] def ker_lift : quotient (ker φ) → H := lift _ φ $ λ g, (mem_ker φ).mp -attribute [to_additive quotient_add_group.ker_lift._proof_1] quotient_group.ker_lift._proof_1 -attribute [to_additive quotient_add_group.ker_lift._proof_2] quotient_group.ker_lift._proof_2 -attribute [to_additive quotient_add_group.ker_lift] quotient_group.ker_lift -attribute [to_additive quotient_add_group.ker_lift.equations._eqn_1] quotient_group.ker_lift.equations._eqn_1 - @[simp, to_additive quotient_add_group.ker_lift_mk] lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g := lift_mk _ _ _ diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean index f6a5f4983f6b0..77a9fccc8fe1d 100644 --- a/src/group_theory/subgroup.lean +++ b/src/group_theory/subgroup.lean @@ -12,23 +12,20 @@ variables {α : Type*} {β : Type*} {a a₁ a₂ b c: α} section group variables [group α] [add_group β] -@[to_additive injective_add] +@[to_additive] lemma injective_mul {a : α} : injective ((*) a) := assume a₁ a₂ h, have a⁻¹ * a * a₁ = a⁻¹ * a * a₂, by rw [mul_assoc, mul_assoc, h], by rwa [inv_mul_self, one_mul, one_mul] at this -/-- `s` is a subgroup: a set containing 1 and closed under multiplication and inverse. -/ -class is_subgroup (s : set α) extends is_submonoid s : Prop := -(inv_mem {a} : a ∈ s → a⁻¹ ∈ s) - /-- `s` is an additive subgroup: a set containing 0 and closed under addition and negation. -/ class is_add_subgroup (s : set β) extends is_add_submonoid s : Prop := (neg_mem {a} : a ∈ s → -a ∈ s) -attribute [to_additive is_add_subgroup] is_subgroup -attribute [to_additive is_add_subgroup.to_is_add_submonoid] is_subgroup.to_is_submonoid -attribute [to_additive is_add_subgroup.neg_mem] is_subgroup.inv_mem -attribute [to_additive is_add_subgroup.mk] is_subgroup.mk + +/-- `s` is a subgroup: a set containing 1 and closed under multiplication and inverse. -/ +@[to_additive is_add_subgroup] +class is_subgroup (s : set α) extends is_submonoid s : Prop := +(inv_mem {a} : a ∈ s → a⁻¹ ∈ s) instance additive.is_add_subgroup (s : set α) [is_subgroup s] : @is_add_subgroup (additive α) _ s := @@ -48,27 +45,15 @@ theorem multiplicative.is_subgroup_iff ⟨by rintro ⟨⟨h₁, h₂⟩, h₃⟩; exact @is_add_subgroup.mk β _ _ ⟨h₁, @h₂⟩ @h₃, λ h, by resetI; apply_instance⟩ +@[to_additive add_group] instance subtype.group {s : set α} [is_subgroup s] : group s := by subtype_instance -instance subtype.add_group {s : set β} [is_add_subgroup s] : add_group s := -by subtype_instance -attribute [to_additive subtype.add_group] subtype.group -attribute [to_additive subtype.add_group._proof_1] subtype.group._proof_1 -attribute [to_additive subtype.add_group._proof_2] subtype.group._proof_2 -attribute [to_additive subtype.add_group._proof_3] subtype.group._proof_3 -attribute [to_additive subtype.add_group._proof_4] subtype.group._proof_4 -attribute [to_additive subtype.add_group._proof_5] subtype.group._proof_5 -attribute [to_additive subtype.add_group.equations._eqn_1] subtype.group.equations._eqn_1 - +@[to_additive add_comm_group] instance subtype.comm_group {α : Type*} [comm_group α] {s : set α} [is_subgroup s] : comm_group s := by subtype_instance -instance subtype.add_comm_group {α : Type*} [add_comm_group α] {s : set α} [is_add_subgroup s] : - add_comm_group s := by subtype_instance -attribute [to_additive subtype.add_comm_group] subtype.comm_group - -@[simp, to_additive is_add_subgroup.coe_neg] +@[simp, to_additive] lemma is_subgroup.coe_inv {s : set α} [is_subgroup s] (a : s) : ((a⁻¹ : s) : α) = a⁻¹ := rfl @[simp] lemma is_subgroup.coe_gpow {s : set α} [is_subgroup s] (a : s) (n : ℤ) : ((a ^ n : s) : α) = a ^ n := @@ -77,8 +62,9 @@ by induction n; simp [is_submonoid.coe_pow a] @[simp] lemma is_add_subgroup.gsmul_coe {β : Type*} [add_group β] {s : set β} [is_add_subgroup s] (a : s) (n : ℤ) : ((gsmul n a : s) : β) = gsmul n a := by induction n; simp [is_add_submonoid.smul_coe a] -attribute [to_additive is_add_subgroup.gsmul_coe] is_subgroup.coe_gpow +attribute [to_additive gsmul_coe] is_subgroup.coe_gpow +@[to_additive of_add_neg] theorem is_subgroup.of_div (s : set α) (one_mem : (1:α) ∈ s) (div_mem : ∀{a b:α}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s) : is_subgroup s := @@ -95,10 +81,9 @@ have inv_mem : ∀a, a ∈ s → a⁻¹ ∈ s, from theorem is_add_subgroup.of_sub (s : set β) (zero_mem : (0:β) ∈ s) (sub_mem : ∀{a b:β}, a ∈ s → b ∈ s → a - b ∈ s) : is_add_subgroup s := -multiplicative.is_subgroup_iff.1 $ -@is_subgroup.of_div (multiplicative β) _ _ zero_mem @sub_mem +is_add_subgroup.of_add_neg s zero_mem (λ x y hx hy, sub_mem hx hy) -@[to_additive is_add_subgroup.inter] +@[to_additive] instance is_subgroup.inter (s₁ s₂ : set α) [is_subgroup s₁] [is_subgroup s₂] : is_subgroup (s₁ ∩ s₂) := { inv_mem := λ x hx, ⟨is_subgroup.inv_mem hx.1, is_subgroup.inv_mem hx.2⟩, @@ -125,7 +110,7 @@ instance gpowers.is_subgroup (x : α) : is_subgroup (gpowers x) := instance gmultiples.is_add_subgroup (x : β) : is_add_subgroup (gmultiples x) := multiplicative.is_subgroup_iff.1 $ gpowers.is_subgroup _ -attribute [to_additive gmultiples.is_add_subgroup] gpowers.is_subgroup +attribute [to_additive is_add_subgroup] gpowers.is_subgroup lemma is_subgroup.gpow_mem {a : α} {s : set α} [is_subgroup s] (h : a ∈ s) : ∀{i:ℤ}, a ^ i ∈ s | (n : ℕ) := is_submonoid.pow_mem h @@ -134,6 +119,14 @@ lemma is_subgroup.gpow_mem {a : α} {s : set α} [is_subgroup s] (h : a ∈ s) : lemma is_add_subgroup.gsmul_mem {a : β} {s : set β} [is_add_subgroup s] : a ∈ s → ∀{i:ℤ}, gsmul i a ∈ s := @is_subgroup.gpow_mem (multiplicative β) _ _ _ _ +lemma gpowers_subset {a : α} {s : set α} [is_subgroup s] (h : a ∈ s) : gpowers a ⊆ s := +λ x hx, match x, hx with _, ⟨i, rfl⟩ := is_subgroup.gpow_mem h end + +lemma gmultiples_subset {a : β} {s : set β} [is_add_subgroup s] (h : a ∈ s) : gmultiples a ⊆ s := +@gpowers_subset (multiplicative β) _ _ _ _ h + +attribute [to_additive gmultiples_subset] gpowers_subset + lemma mem_gpowers {a : α} : a ∈ gpowers a := ⟨1, by simp⟩ lemma mem_gmultiples {a : β} : a ∈ gmultiples a := ⟨1, by simp⟩ attribute [to_additive mem_gmultiples] mem_gpowers @@ -144,15 +137,15 @@ namespace is_subgroup open is_submonoid variables [group α] (s : set α) [is_subgroup s] -@[to_additive is_add_subgroup.neg_mem_iff] +@[to_additive] lemma inv_mem_iff : a⁻¹ ∈ s ↔ a ∈ s := ⟨λ h, by simpa using inv_mem h, inv_mem⟩ -@[to_additive is_add_subgroup.add_mem_cancel_left] +@[to_additive] lemma mul_mem_cancel_left (h : a ∈ s) : b * a ∈ s ↔ b ∈ s := ⟨λ hba, by simpa using mul_mem hba (inv_mem h), λ hb, mul_mem hb h⟩ -@[to_additive is_add_subgroup.add_mem_cancel_right] +@[to_additive] lemma mul_mem_cancel_right (h : a ∈ s) : a * b ∈ s ↔ b ∈ s := ⟨λ hab, by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩ @@ -162,14 +155,12 @@ theorem is_add_subgroup.sub_mem {α} [add_group α] (s : set α) [is_add_subgrou (ha : a ∈ s) (hb : b ∈ s) : a - b ∈ s := is_add_submonoid.add_mem ha (is_add_subgroup.neg_mem hb) -class normal_subgroup [group α] (s : set α) extends is_subgroup s : Prop := -(normal : ∀ n ∈ s, ∀ g : α, g * n * g⁻¹ ∈ s) class normal_add_subgroup [add_group α] (s : set α) extends is_add_subgroup s : Prop := (normal : ∀ n ∈ s, ∀ g : α, g + n - g ∈ s) -attribute [to_additive normal_add_subgroup] normal_subgroup -attribute [to_additive normal_add_subgroup.to_is_add_subgroup] normal_subgroup.to_is_subgroup -attribute [to_additive normal_add_subgroup.normal] normal_subgroup.normal -attribute [to_additive normal_add_subgroup.mk] normal_subgroup.mk + +@[to_additive normal_add_subgroup] +class normal_subgroup [group α] (s : set α) extends is_subgroup s : Prop := +(normal : ∀ n ∈ s, ∀ g : α, g * n * g⁻¹ ∈ s) @[to_additive normal_add_subgroup_of_add_comm_group] lemma normal_subgroup_of_comm_group [comm_group α] (s : set α) [hs : is_subgroup s] : @@ -201,34 +192,44 @@ namespace is_subgroup variable [group α] -- Normal subgroup properties +@[to_additive] lemma mem_norm_comm {s : set α} [normal_subgroup s] {a b : α} (hab : a * b ∈ s) : b * a ∈ s := have h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ s, from normal_subgroup.normal (a * b) hab a⁻¹, by simp at h; exact h +@[to_additive] lemma mem_norm_comm_iff {s : set α} [normal_subgroup s] {a b : α} : a * b ∈ s ↔ b * a ∈ s := ⟨mem_norm_comm, mem_norm_comm⟩ /-- The trivial subgroup -/ +@[to_additive] def trivial (α : Type*) [group α] : set α := {1} -@[simp] lemma mem_trivial [group α] {g : α} : g ∈ trivial α ↔ g = 1 := +@[simp, to_additive] +lemma mem_trivial [group α] {g : α} : g ∈ trivial α ↔ g = 1 := mem_singleton_iff +@[to_additive] instance trivial_normal : normal_subgroup (trivial α) := by refine {..}; simp [trivial] {contextual := tt} +@[to_additive] lemma eq_trivial_iff {H : set α} [is_subgroup H] : H = trivial α ↔ (∀ x ∈ H, x = (1 : α)) := by simp only [set.ext_iff, is_subgroup.mem_trivial]; exact ⟨λ h x, (h x).1, λ h x, ⟨h x, λ hx, hx.symm ▸ is_submonoid.one_mem H⟩⟩ +@[to_additive] instance univ_subgroup : normal_subgroup (@univ α) := by refine {..}; simp +@[to_additive add_center] def center (α : Type*) [group α] : set α := {z | ∀ g, g * z = z * g} +@[to_additive mem_add_center] lemma mem_center {a : α} : a ∈ center α ↔ ∀g, g * a = a * g := iff.rfl +@[to_additive add_center_normal] instance center_normal : normal_subgroup (center α) := { one_mem := by simp [center], mul_mem := assume a b ha hb g, @@ -243,10 +244,12 @@ instance center_normal : normal_subgroup (center α) := ... = g * g⁻¹ * n * h : by rw ha h; simp ... = g * n * g⁻¹ * h : by rw [mul_assoc g, ha g⁻¹, ←mul_assoc] } +@[to_additive add_normalizer] def normalizer (s : set α) : set α := {g : α | ∀ n, n ∈ s ↔ g * n * g⁻¹ ∈ s} -instance (s : set α) [is_subgroup s] : is_subgroup (normalizer s) := +@[to_additive normalizer_is_add_subgroup] +instance normalizer_is_subgroup (s : set α) [is_subgroup s] : is_subgroup (normalizer s) := { one_mem := by simp [normalizer], mul_mem := λ a b (ha : ∀ n, n ∈ s ↔ a * n * a⁻¹ ∈ s) (hb : ∀ n, n ∈ s ↔ b * n * b⁻¹ ∈ s) n, @@ -255,11 +258,16 @@ instance (s : set α) [is_subgroup s] : is_subgroup (normalizer s) := by rw [ha (a⁻¹ * n * a⁻¹⁻¹)]; simp [mul_assoc] } +@[to_additive subset_add_normalizer] lemma subset_normalizer (s : set α) [is_subgroup s] : s ⊆ normalizer s := λ g hg n, by rw [is_subgroup.mul_mem_cancel_left _ ((is_subgroup.inv_mem_iff _).2 hg), is_subgroup.mul_mem_cancel_right _ hg] -instance (s : set α) [is_subgroup s] : normal_subgroup (subtype.val ⁻¹' s : set (normalizer s)) := + +/-- Every subgroup is a normal subgroup of its normalizer -/ +@[to_additive add_normal_in_add_normalizer] +instance normal_in_normalizer (s : set α) [is_subgroup s] : + normal_subgroup (subtype.val ⁻¹' s : set (normalizer s)) := { one_mem := show (1 : α) ∈ s, from is_submonoid.one_mem _, mul_mem := λ a b ha hb, show (a * b : α) ∈ s, from is_submonoid.mul_mem ha hb, inv_mem := λ a ha, show (a⁻¹ : α) ∈ s, from is_subgroup.inv_mem ha, @@ -267,61 +275,27 @@ instance (s : set α) [is_subgroup s] : normal_subgroup (subtype.val ⁻¹' s : end is_subgroup -namespace is_add_subgroup -variable [add_group α] - -attribute [to_additive is_add_subgroup.mem_norm_comm] is_subgroup.mem_norm_comm -attribute [to_additive is_add_subgroup.mem_norm_comm_iff] is_subgroup.mem_norm_comm_iff - -/-- The trivial subgroup -/ -def trivial (α : Type*) [add_group α] : set α := {0} -attribute [to_additive is_add_subgroup.trivial] is_subgroup.trivial -attribute [to_additive is_add_subgroup.trivial.equations._eqn_1] is_subgroup.trivial.equations._eqn_1 - -attribute [to_additive is_add_subgroup.mem_trivial] is_subgroup.mem_trivial - -instance trivial_normal : normal_add_subgroup (trivial α) := -multiplicative.normal_subgroup_iff.1 is_subgroup.trivial_normal -attribute [to_additive is_add_subgroup.trivial_normal] is_subgroup.trivial_normal - -attribute [to_additive is_add_subgroup.eq_trivial_iff] is_subgroup.eq_trivial_iff - -instance univ_add_subgroup : normal_add_subgroup (@univ α) := -multiplicative.normal_subgroup_iff.1 is_subgroup.univ_subgroup -attribute [to_additive is_add_subgroup.univ_add_subgroup] is_subgroup.univ_subgroup - -def center (α : Type*) [add_group α] : set α := {z | ∀ g, g + z = z + g} -attribute [to_additive is_add_subgroup.center] is_subgroup.center - -attribute [to_additive is_add_subgroup.mem_center] is_subgroup.mem_center - -instance center_normal : normal_add_subgroup (center α) := -multiplicative.normal_subgroup_iff.1 is_subgroup.center_normal - -end is_add_subgroup - -- Homomorphism subgroups namespace is_group_hom open is_submonoid is_subgroup open is_mul_hom (map_mul) variables [group α] [group β] -@[to_additive is_add_group_hom.ker] +@[to_additive] def ker (f : α → β) [is_group_hom f] : set α := preimage f (trivial β) -attribute [to_additive is_add_group_hom.ker.equations._eqn_1] ker.equations._eqn_1 -@[to_additive is_add_group_hom.mem_ker] +@[to_additive] lemma mem_ker (f : α → β) [is_group_hom f] {x : α} : x ∈ ker f ↔ f x = 1 := mem_trivial -@[to_additive is_add_group_hom.zero_ker_neg] +@[to_additive] lemma one_ker_inv (f : α → β) [is_group_hom f] {a b : α} (h : f (a * b⁻¹) = 1) : f a = f b := begin rw [map_mul f, map_inv f] at h, rw [←inv_inv (f b), eq_inv_of_mul_eq_one h] end -@[to_additive is_add_group_hom.zero_ker_neg'] +@[to_additive] lemma one_ker_inv' (f : α → β) [is_group_hom f] {a b : α} (h : f (a⁻¹ * b) = 1) : f a = f b := begin rw [map_mul f, map_inv f] at h, @@ -329,72 +303,61 @@ begin rw eq_inv_of_mul_eq_one h end -@[to_additive is_add_group_hom.neg_ker_zero] +@[to_additive] lemma inv_ker_one (f : α → β) [is_group_hom f] {a b : α} (h : f a = f b) : f (a * b⁻¹) = 1 := have f a * (f b)⁻¹ = 1, by rw [h, mul_right_inv], by rwa [←map_inv f, ←map_mul f] at this -@[to_additive is_add_group_hom.neg_ker_zero'] +@[to_additive] lemma inv_ker_one' (f : α → β) [is_group_hom f] {a b : α} (h : f a = f b) : f (a⁻¹ * b) = 1 := have (f a)⁻¹ * f b = 1, by rw [h, mul_left_inv], by rwa [←map_inv f, ←map_mul f] at this -@[to_additive is_add_group_hom.zero_iff_ker_neg] +@[to_additive] lemma one_iff_ker_inv (f : α → β) [is_group_hom f] (a b : α) : f a = f b ↔ f (a * b⁻¹) = 1 := ⟨inv_ker_one f, one_ker_inv f⟩ -@[to_additive is_add_group_hom.zero_iff_ker_neg'] +@[to_additive] lemma one_iff_ker_inv' (f : α → β) [is_group_hom f] (a b : α) : f a = f b ↔ f (a⁻¹ * b) = 1 := ⟨inv_ker_one' f, one_ker_inv' f⟩ -@[to_additive is_add_group_hom.neg_iff_ker] +@[to_additive] lemma inv_iff_ker (f : α → β) [w : is_group_hom f] (a b : α) : f a = f b ↔ a * b⁻¹ ∈ ker f := by rw [mem_ker]; exact one_iff_ker_inv _ _ _ -@[to_additive is_add_group_hom.neg_iff_ker'] +@[to_additive] lemma inv_iff_ker' (f : α → β) [w : is_group_hom f] (a b : α) : f a = f b ↔ a⁻¹ * b ∈ ker f := by rw [mem_ker]; exact one_iff_ker_inv' _ _ _ +@[to_additive image_add_subgroup] instance image_subgroup (f : α → β) [is_group_hom f] (s : set α) [is_subgroup s] : is_subgroup (f '' s) := { mul_mem := assume a₁ a₂ ⟨b₁, hb₁, eq₁⟩ ⟨b₂, hb₂, eq₂⟩, ⟨b₁ * b₂, mul_mem hb₁ hb₂, by simp [eq₁, eq₂, map_mul f]⟩, one_mem := ⟨1, one_mem s, map_one f⟩, inv_mem := assume a ⟨b, hb, eq⟩, ⟨b⁻¹, inv_mem hb, by rw map_inv f; simp *⟩ } -attribute [to_additive is_add_group_hom.image_add_subgroup._match_1] is_group_hom.image_subgroup._match_1 -attribute [to_additive is_add_group_hom.image_add_subgroup._match_2] is_group_hom.image_subgroup._match_2 -attribute [to_additive is_add_group_hom.image_add_subgroup._match_3] is_group_hom.image_subgroup._match_3 -attribute [to_additive is_add_group_hom.image_add_subgroup] is_group_hom.image_subgroup -attribute [to_additive is_add_group_hom.image_add_subgroup._match_1.equations._eqn_1] is_group_hom.image_subgroup._match_1.equations._eqn_1 -attribute [to_additive is_add_group_hom.image_add_subgroup._match_2.equations._eqn_1] is_group_hom.image_subgroup._match_2.equations._eqn_1 -attribute [to_additive is_add_group_hom.image_add_subgroup._match_3.equations._eqn_1] is_group_hom.image_subgroup._match_3.equations._eqn_1 -attribute [to_additive is_add_group_hom.image_add_subgroup.equations._eqn_1] is_group_hom.image_subgroup.equations._eqn_1 +@[to_additive range_add_subgroup] instance range_subgroup (f : α → β) [is_group_hom f] : is_subgroup (set.range f) := @set.image_univ _ _ f ▸ is_group_hom.image_subgroup f set.univ -attribute [to_additive is_add_group_hom.range_add_subgroup] is_group_hom.range_subgroup -attribute [to_additive is_add_group_hom.range_add_subgroup.equations._eqn_1] is_group_hom.range_subgroup.equations._eqn_1 local attribute [simp] one_mem inv_mem mul_mem normal_subgroup.normal +@[to_additive] instance preimage (f : α → β) [is_group_hom f] (s : set β) [is_subgroup s] : is_subgroup (f ⁻¹' s) := by refine {..}; simp [map_mul f, map_one f, map_inv f, @inv_mem β _ s] {contextual:=tt} -attribute [to_additive is_add_group_hom.preimage] is_group_hom.preimage -attribute [to_additive is_add_group_hom.preimage.equations._eqn_1] is_group_hom.preimage.equations._eqn_1 +@[to_additive] instance preimage_normal (f : α → β) [is_group_hom f] (s : set β) [normal_subgroup s] : normal_subgroup (f ⁻¹' s) := ⟨by simp [map_mul f, map_inv f] {contextual:=tt}⟩ -attribute [to_additive is_add_group_hom.preimage_normal] is_group_hom.preimage_normal -attribute [to_additive is_add_group_hom.preimage_normal.equations._eqn_1] is_group_hom.preimage_normal.equations._eqn_1 +@[to_additive] instance normal_subgroup_ker (f : α → β) [is_group_hom f] : normal_subgroup (ker f) := is_group_hom.preimage_normal f (trivial β) -attribute [to_additive is_add_group_hom.normal_subgroup_ker] is_group_hom.normal_subgroup_ker -attribute [to_additive is_add_group_hom.normal_subgroup_ker.equations._eqn_1] is_group_hom.normal_subgroup_ker.equations._eqn_1 -@[to_additive is_add_group_hom.inj_of_trivial_ker] +@[to_additive] lemma inj_of_trivial_ker (f : α → β) [is_group_hom f] (h : ker f = trivial α) : function.injective f := begin @@ -404,7 +367,7 @@ begin rw [eq_inv_of_mul_eq_one ha, inv_inv a₂] end -@[to_additive is_add_group_hom.trivial_ker_of_inj] +@[to_additive] lemma trivial_ker_of_inj (f : α → β) [is_group_hom f] (h : function.injective f) : ker f = trivial α := set.ext $ assume x, iff.intro @@ -413,12 +376,12 @@ set.ext $ assume x, iff.intro by simp [map_one f]; rwa [mem_ker] at hx) (by simp [mem_ker, is_group_hom.map_one f] {contextual := tt}) -@[to_additive is_add_group_hom.inj_iff_trivial_ker] +@[to_additive] lemma inj_iff_trivial_ker (f : α → β) [is_group_hom f] : function.injective f ↔ ker f = trivial α := ⟨trivial_ker_of_inj f, inj_of_trivial_ker f⟩ -@[to_additive is_add_group_hom.trivial_ker_iff_eq_zero] +@[to_additive] lemma trivial_ker_iff_eq_one (f : α → β) [is_group_hom f] : ker f = trivial α ↔ ∀ x, f x = 1 → x = 1 := by rw set.ext_iff; simp [ker]; exact @@ -426,45 +389,42 @@ by rw set.ext_iff; simp [ker]; exact end is_group_hom +@[to_additive is_add_group_hom] instance subtype_val.is_group_hom [group α] {s : set α} [is_subgroup s] : is_group_hom (subtype.val : s → α) := { ..subtype_val.is_monoid_hom } -instance subtype_val.is_add_group_hom [add_group α] {s : set α} [is_add_subgroup s] : - is_add_group_hom (subtype.val : s → α) := { ..subtype_val.is_add_monoid_hom } -attribute [to_additive subtype_val.is_group_hom] subtype_val.is_add_group_hom - +@[to_additive is_add_group_hom] instance coe.is_group_hom [group α] {s : set α} [is_subgroup s] : is_group_hom (coe : s → α) := { ..subtype_val.is_monoid_hom } -instance coe.is_add_group_hom [add_group α] {s : set α} [is_add_subgroup s] : - is_add_group_hom (coe : s → α) := -{ ..subtype_val.is_add_monoid_hom } -attribute [to_additive coe.is_group_hom] coe.is_add_group_hom - +@[to_additive is_add_group_hom] instance subtype_mk.is_group_hom [group α] [group β] {s : set α} [is_subgroup s] (f : β → α) [is_group_hom f] (h : ∀ x, f x ∈ s) : is_group_hom (λ x, (⟨f x, h x⟩ : s)) := { ..subtype_mk.is_monoid_hom f h } -instance subtype_mk.is_add_group_hom [add_group α] [add_group β] {s : set α} - [is_add_subgroup s] (f : β → α) [is_add_group_hom f] (h : ∀ x, f x ∈ s) : - is_add_group_hom (λ x, (⟨f x, h x⟩ : s)) := -{ ..subtype_mk.is_add_monoid_hom f h } -attribute [to_additive subtype_mk.is_group_hom] subtype_mk.is_add_group_hom - +@[to_additive is_add_group_hom] instance set_inclusion.is_group_hom [group α] {s t : set α} [is_subgroup s] [is_subgroup t] (h : s ⊆ t) : is_group_hom (set.inclusion h) := subtype_mk.is_group_hom _ _ -instance set_inclusion.is_add_group_hom [add_group α] {s t : set α} - [is_add_subgroup s] [is_add_subgroup t] (h : s ⊆ t) : is_add_group_hom (set.inclusion h) := -subtype_mk.is_add_group_hom _ _ -attribute [to_additive set_inclusion.is_group_hom] set_inclusion.is_add_group_hom +namespace add_group + +variables [add_group α] + +inductive in_closure (s : set α) : α → Prop +| basic {a : α} : a ∈ s → in_closure a +| zero : in_closure 0 +| neg {a : α} : in_closure a → in_closure (-a) +| add {a b : α} : in_closure a → in_closure b → in_closure (a + b) + +end add_group namespace group open is_submonoid is_subgroup variables [group α] {s : set α} +@[to_additive] inductive in_closure (s : set α) : α → Prop | basic {a : α} : a ∈ s → in_closure a | one : in_closure 1 @@ -472,27 +432,36 @@ inductive in_closure (s : set α) : α → Prop | mul {a b : α} : in_closure a → in_closure b → in_closure (a * b) /-- `group.closure s` is the subgroup closed over `s`, i.e. the smallest subgroup containg s. -/ +@[to_additive] def closure (s : set α) : set α := {a | in_closure s a } +@[to_additive] lemma mem_closure {a : α} : a ∈ s → a ∈ closure s := in_closure.basic +@[to_additive is_add_subgroup] instance closure.is_subgroup (s : set α) : is_subgroup (closure s) := { one_mem := in_closure.one s, mul_mem := assume a b, in_closure.mul, inv_mem := assume a, in_closure.inv } +@[to_additive] theorem subset_closure {s : set α} : s ⊆ closure s := λ a, mem_closure +@[to_additive] theorem closure_subset {s t : set α} [is_subgroup t] (h : s ⊆ t) : closure s ⊆ t := assume a ha, by induction ha; simp [h _, *, one_mem, mul_mem, inv_mem_iff] +@[to_additive] lemma closure_subset_iff (s t : set α) [is_subgroup t] : closure s ⊆ t ↔ s ⊆ t := ⟨assume h b ha, h (mem_closure ha), assume h b ha, closure_subset h ha⟩ +@[to_additive] theorem closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t := closure_subset $ set.subset.trans h subset_closure -@[simp] lemma closure_subgroup (s : set α) [is_subgroup s] : closure s = s := +@[simp, to_additive closure_add_subgroup] +lemma closure_subgroup (s : set α) [is_subgroup s] : closure s = s := set.subset.antisymm (closure_subset $ set.subset.refl s) subset_closure +@[to_additive] theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a ∈ closure s) : (∃l:list α, (∀x∈l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = a) := in_closure.rec_on h @@ -507,6 +476,7 @@ in_closure.rec_on h (λ x y hx hy ⟨L1, HL1, HL2⟩ ⟨L2, HL3, HL4⟩, ⟨L1 ++ L2, list.forall_mem_append.2 ⟨HL1, HL3⟩, by rw [list.prod_append, HL2, HL4]⟩) +@[to_additive] lemma image_closure [group β] (f : α → β) [is_group_hom f] (s : set α) : f '' closure s = closure (f '' s) := le_antisymm @@ -520,12 +490,15 @@ le_antisymm end (closure_subset $ set.image_subset _ subset_closure) +@[to_additive] theorem mclosure_subset {s : set α} : monoid.closure s ⊆ closure s := monoid.closure_subset $ subset_closure +@[to_additive] theorem mclosure_inv_subset {s : set α} : monoid.closure (has_inv.inv ⁻¹' s) ⊆ closure s := monoid.closure_subset $ λ x hx, inv_inv x ▸ (is_subgroup.inv_mem $ subset_closure hx) +@[to_additive] theorem closure_eq_mclosure {s : set α} : closure s = monoid.closure (s ∪ has_inv.inv ⁻¹' s) := set.subset.antisymm (@closure_subset _ _ _ (monoid.closure (s ∪ has_inv.inv ⁻¹' s)) @@ -537,6 +510,7 @@ set.subset.antisymm (set.subset.trans (set.subset_union_left _ _) monoid.subset_closure)) (monoid.closure_subset $ set.union_subset subset_closure $ λ x hx, inv_inv x ▸ (is_subgroup.inv_mem $ subset_closure hx)) +@[to_additive] theorem mem_closure_union_iff {α : Type*} [comm_group α] {s t : set α} {x : α} : x ∈ closure (s ∪ t) ↔ ∃ y ∈ closure s, ∃ z ∈ closure t, y * z = x := begin @@ -549,93 +523,22 @@ begin rw [mul_assoc, mul_assoc, mul_left_comm yt], refl } end +@[to_additive gmultiples_eq_closure] theorem gpowers_eq_closure {a : α} : gpowers a = closure {a} := subset.antisymm - (assume x h, match x, h with _, ⟨i, rfl⟩ := gpow_mem (mem_closure $ by simp) end) + (gpowers_subset $ mem_closure $ by simp) (closure_subset $ by simp [mem_gpowers]) end group -namespace add_group -open is_add_submonoid is_add_subgroup - -variables [add_group α] {s : set α} - -/-- `add_group.closure s` is the additive subgroup closed over `s`, i.e. the smallest subgroup containg s. -/ -def closure (s : set α) : set α := @group.closure (multiplicative α) _ s -attribute [to_additive add_group.closure] group.closure - -lemma mem_closure {a : α} : a ∈ s → a ∈ closure s := group.mem_closure -attribute [to_additive add_group.mem_closure] group.mem_closure - -instance closure.is_add_subgroup (s : set α) : is_add_subgroup (closure s) := -multiplicative.is_subgroup_iff.1 $ group.closure.is_subgroup _ -attribute [to_additive add_group.closure.is_add_subgroup] group.closure.is_subgroup - -attribute [to_additive add_group.subset_closure] group.subset_closure - -theorem closure_subset {s t : set α} [is_add_subgroup t] : s ⊆ t → closure s ⊆ t := -group.closure_subset - -attribute [to_additive add_group.closure_subset] group.closure_subset -attribute [to_additive add_group.closure_subset_iff] group.closure_subset_iff - -theorem gmultiples_eq_closure {a : α} : gmultiples a = closure {a} := -group.gpowers_eq_closure -attribute [to_additive add_group.gmultiples_eq_closure] group.gpowers_eq_closure - -@[elab_as_eliminator] -theorem in_closure.rec_on {C : α → Prop} - {a : α} (H : a ∈ closure s) - (H1 : ∀ {a : α}, a ∈ s → C a) (H2 : C 0) (H3 : ∀ {a : α}, a ∈ closure s → C a → C (-a)) - (H4 : ∀ {a b : α}, a ∈ closure s → b ∈ closure s → C a → C b → C (a + b)) : - C a := -group.in_closure.rec_on H (λ _, H1) H2 (λ _, H3) (λ _ _, H4) -attribute [to_additive add_group.in_closure.rec_on] group.in_closure.rec_on - -lemma image_closure [add_group β] (f : α → β) [is_add_group_hom f] (s : set α) : - f '' closure s = closure (f '' s) := -le_antisymm - begin - rintros _ ⟨x, hx, rfl⟩, - apply in_closure.rec_on hx; intros, - { solve_by_elim [subset_closure, set.mem_image_of_mem] }, - { rw [is_add_monoid_hom.map_zero f], apply is_add_submonoid.zero_mem }, - { rw [is_add_group_hom.map_neg f], apply is_add_subgroup.neg_mem, assumption }, - { rw [is_add_monoid_hom.map_add f], solve_by_elim [is_add_submonoid.add_mem] } - end - (closure_subset $ set.image_subset _ subset_closure) -attribute [to_additive add_group.image_closure] group.image_closure - -theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a ∈ closure s) : - (∃l:list α, (∀x∈l, x ∈ s ∨ -x ∈ s) ∧ l.sum = a) := -group.exists_list_of_mem_closure h -attribute [to_additive add_group.exists_list_of_mem_closure] group.exists_list_of_mem_closure - -attribute [to_additive add_group.closure_mono] group.closure_mono -attribute [to_additive add_group.closure_add_subgroup] group.closure_subgroup -attribute [to_additive add_group.mclosure_subset] group.mclosure_subset -attribute [to_additive add_group.mclosure_inv_subset] group.mclosure_inv_subset - -theorem closure_eq_mclosure {s : set α} : closure s = add_monoid.closure (s ∪ has_neg.neg ⁻¹' s) := -group.closure_eq_mclosure -attribute [to_additive add_group.closure_eq_mclosure] group.closure_eq_mclosure - -theorem mem_closure_union_iff {α : Type*} [add_comm_group α] {s t : set α} {x : α} : - x ∈ closure (s ∪ t) ↔ ∃ y ∈ closure s, ∃ z ∈ closure t, y + z = x := -group.mem_closure_union_iff -attribute [to_additive add_group.mem_closure_union_iff] group.mem_closure_union_iff - -end add_group - namespace is_subgroup variable [group α] +@[to_additive] lemma trivial_eq_closure : trivial α = group.closure ∅ := subset.antisymm (by simp [set.subset_def, is_submonoid.one_mem]) (group.closure_subset $ by simp) -attribute [to_additive is_add_subgroup.trivial_eq_closure] is_subgroup.trivial_eq_closure end is_subgroup diff --git a/src/group_theory/submonoid.lean b/src/group_theory/submonoid.lean index 8db5103a45445..04eefdf6f3097 100644 --- a/src/group_theory/submonoid.lean +++ b/src/group_theory/submonoid.lean @@ -10,20 +10,16 @@ import tactic.subtype_instance variables {α : Type*} [monoid α] {s : set α} variables {β : Type*} [add_monoid β] {t : set β} -/-- `s` is a submonoid: a set containing 1 and closed under multiplication. -/ -class is_submonoid (s : set α) : Prop := -(one_mem : (1:α) ∈ s) -(mul_mem {a b} : a ∈ s → b ∈ s → a * b ∈ s) - /-- `s` is an additive submonoid: a set containing 0 and closed under addition. -/ class is_add_submonoid (s : set β) : Prop := (zero_mem : (0:β) ∈ s) (add_mem {a b} : a ∈ s → b ∈ s → a + b ∈ s) -attribute [to_additive is_add_submonoid] is_submonoid -attribute [to_additive is_add_submonoid.zero_mem] is_submonoid.one_mem -attribute [to_additive is_add_submonoid.add_mem] is_submonoid.mul_mem -attribute [to_additive is_add_submonoid.mk] is_submonoid.mk +/-- `s` is a submonoid: a set containing 1 and closed under multiplication. -/ +@[to_additive is_add_submonoid] +class is_submonoid (s : set α) : Prop := +(one_mem : (1:α) ∈ s) +(mul_mem {a b} : a ∈ s → b ∈ s → a * b ∈ s) instance additive.is_add_submonoid (s : set α) : ∀ [is_submonoid s], @is_add_submonoid (additive α) _ s @@ -41,13 +37,14 @@ theorem multiplicative.is_submonoid_iff {s : set β} : @is_submonoid (multiplicative β) _ s ↔ is_add_submonoid s := ⟨λ ⟨h₁, h₂⟩, ⟨h₁, @h₂⟩, λ h, by resetI; apply_instance⟩ -@[to_additive is_add_submonoid.inter] +@[to_additive] lemma is_submonoid.inter (s₁ s₂ : set α) [is_submonoid s₁] [is_submonoid s₂] : is_submonoid (s₁ ∩ s₂) := { one_mem := ⟨is_submonoid.one_mem _, is_submonoid.one_mem _⟩, mul_mem := λ x y hx hy, ⟨is_submonoid.mul_mem hx.1 hy.1, is_submonoid.mul_mem hx.2 hy.2⟩ } +@[to_additive is_add_submonoid_Union_of_directed] lemma is_submonoid_Union_of_directed {ι : Type*} [hι : nonempty ι] (s : ι → set α) [∀ i, is_submonoid (s i)] (directed : ∀ i j, ∃ k, s i ⊆ s k ∧ s j ⊆ s k) : @@ -59,14 +56,6 @@ lemma is_submonoid_Union_of_directed {ι : Type*} [hι : nonempty ι] let ⟨k, hk⟩ := directed i j in set.mem_Union.2 ⟨k, is_submonoid.mul_mem (hk.1 hi) (hk.2 hj)⟩ } -lemma is_add_submonoid_Union_of_directed {ι : Type*} [hι : nonempty ι] - (s : ι → set β) [∀ i, is_add_submonoid (s i)] - (directed : ∀ i j, ∃ k, s i ⊆ s k ∧ s j ⊆ s k) : - is_add_submonoid (⋃i, s i) := -multiplicative.is_submonoid_iff.1 $ - @is_submonoid_Union_of_directed (multiplicative β) _ _ _ s _ directed -attribute [to_additive is_add_submonoid_Union_of_directed] is_submonoid_Union_of_directed - section powers def powers (x : α) : set α := {y | ∃ n:ℕ, x^n = y} @@ -76,38 +65,43 @@ attribute [to_additive multiples] powers lemma powers.one_mem {x : α} : (1 : α) ∈ powers x := ⟨0, pow_zero _⟩ lemma multiples.zero_mem {x : β} : (0 : β) ∈ multiples x := ⟨0, add_monoid.zero_smul _⟩ -attribute [to_additive multiples.zero_mem] powers.one_mem +attribute [to_additive] powers.one_mem lemma powers.self_mem {x : α} : x ∈ powers x := ⟨1, pow_one _⟩ lemma multiples.self_mem {x : β} : x ∈ multiples x := ⟨1, add_monoid.one_smul _⟩ -attribute [to_additive multiples.self_mem] powers.self_mem +attribute [to_additive] powers.self_mem -instance powers.is_submonoid (x : α) : is_submonoid (powers x) := -{ one_mem := ⟨0, by simp⟩, - mul_mem := λ x₁ x₂ ⟨n₁, hn₁⟩ ⟨n₂, hn₂⟩, ⟨n₁ + n₂, by simp [pow_add, *]⟩ } +lemma powers.mul_mem {x y z: α} : (y ∈ powers x) → (z ∈ powers x) → (y * z ∈ powers x) := +λ ⟨n₁, h₁⟩ ⟨n₂, h₂⟩, ⟨n₁ + n₂, by simp only [pow_add, *]⟩ -instance multiples.is_add_submonoid (x : β) : is_add_submonoid (multiples x) := -multiplicative.is_submonoid_iff.1 $ powers.is_submonoid _ -attribute [to_additive multiples.is_add_submonoid] powers.is_submonoid +lemma multiples.add_mem {x y z: β} : (y ∈ multiples x) → (z ∈ multiples x) → (y + z ∈ multiples x) := +@powers.mul_mem (multiplicative β) _ _ _ _ +attribute [to_additive] powers.mul_mem -@[to_additive univ.is_add_submonoid] +@[to_additive is_add_submonoid] +instance powers.is_submonoid (x : α) : is_submonoid (powers x) := +{ one_mem := powers.one_mem, + mul_mem := λ y z, powers.mul_mem } + +@[to_additive is_add_submonoid] instance univ.is_submonoid : is_submonoid (@set.univ α) := by split; simp -@[to_additive preimage.is_add_submonoid] +@[to_additive is_add_submonoid] instance preimage.is_submonoid {γ : Type*} [monoid γ] (f : α → γ) [is_monoid_hom f] (s : set γ) [is_submonoid s] : is_submonoid (f ⁻¹' s) := { one_mem := show f 1 ∈ s, by rw is_monoid_hom.map_one f; exact is_submonoid.one_mem s, mul_mem := λ a b (ha : f a ∈ s) (hb : f b ∈ s), show f (a * b) ∈ s, by rw is_monoid_hom.map_mul f; exact is_submonoid.mul_mem ha hb } -@[instance, to_additive image.is_add_submonoid] +@[instance, to_additive is_add_submonoid] lemma image.is_submonoid {γ : Type*} [monoid γ] (f : α → γ) [is_monoid_hom f] (s : set α) [is_submonoid s] : is_submonoid (f '' s) := { one_mem := ⟨1, is_submonoid.one_mem s, is_monoid_hom.map_one f⟩, mul_mem := λ a b ⟨x, hx⟩ ⟨y, hy⟩, ⟨x * y, is_submonoid.mul_mem hx.1 hy.1, by rw [is_monoid_hom.map_mul f, hx.2, hy.2]⟩ } +@[to_additive is_add_submonoid] instance range.is_submonoid {γ : Type*} [monoid γ] (f : α → γ) [is_monoid_hom f] : is_submonoid (set.range f) := by rw ← set.image_univ; apply_instance @@ -119,7 +113,7 @@ lemma is_submonoid.pow_mem {a : α} [is_submonoid s] (h : a ∈ s) : ∀ {n : lemma is_add_submonoid.smul_mem {a : β} [is_add_submonoid t] : ∀ (h : a ∈ t) {n : ℕ}, add_monoid.smul n a ∈ t := @is_submonoid.pow_mem (multiplicative β) _ _ _ _ -attribute [to_additive is_add_submonoid.smul_mem] is_submonoid.pow_mem +attribute [to_additive smul_mem] is_submonoid.pow_mem lemma is_submonoid.power_subset {a : α} [is_submonoid s] (h : a ∈ s) : powers a ⊆ s := assume x ⟨n, hx⟩, hx ▸ is_submonoid.pow_mem h @@ -127,13 +121,13 @@ assume x ⟨n, hx⟩, hx ▸ is_submonoid.pow_mem h lemma is_add_submonoid.multiple_subset {a : β} [is_add_submonoid t] : a ∈ t → multiples a ⊆ t := @is_submonoid.power_subset (multiplicative β) _ _ _ _ -attribute [to_additive is_add_submonoid.multiple_subset] is_add_submonoid.multiple_subset +attribute [to_additive multiple_subset] is_submonoid.power_subset end powers namespace is_submonoid -@[to_additive is_add_submonoid.list_sum_mem] +@[to_additive] lemma list_prod_mem [is_submonoid s] : ∀{l : list α}, (∀x∈l, x ∈ s) → l.prod ∈ s | [] h := one_mem s | (a::l) h := @@ -141,7 +135,7 @@ lemma list_prod_mem [is_submonoid s] : ∀{l : list α}, (∀x∈l, x ∈ s) → have a ∈ s ∧ (∀x∈l, x ∈ s), by simpa using h, is_submonoid.mul_mem this.1 (list_prod_mem this.2) -@[to_additive is_add_submonoid.multiset_sum_mem] +@[to_additive] lemma multiset_prod_mem {α} [comm_monoid α] (s : set α) [is_submonoid s] (m : multiset α) : (∀a∈m, a ∈ s) → m.prod ∈ s := begin @@ -150,7 +144,7 @@ begin exact list_prod_mem hl end -@[to_additive is_add_submonoid.finset_sum_mem] +@[to_additive] lemma finset_prod_mem {α β} [comm_monoid α] (s : set α) [is_submonoid s] (f : β → α) : ∀(t : finset β), (∀b∈t, f b ∈ s) → t.prod f ∈ s | ⟨m, hm⟩ hs := @@ -163,20 +157,14 @@ lemma finset_prod_mem {α β} [comm_monoid α] (s : set α) [is_submonoid s] (f end is_submonoid +@[to_additive add_monoid] instance subtype.monoid {s : set α} [is_submonoid s] : monoid s := by subtype_instance -attribute [to_additive subtype.add_monoid._proof_1] subtype.monoid._proof_1 -attribute [to_additive subtype.add_monoid._proof_2] subtype.monoid._proof_2 -attribute [to_additive subtype.add_monoid._proof_3] subtype.monoid._proof_3 -attribute [to_additive subtype.add_monoid._proof_4] subtype.monoid._proof_4 -attribute [to_additive subtype.add_monoid._proof_5] subtype.monoid._proof_5 -attribute [to_additive subtype.add_monoid] subtype.monoid - -@[simp, to_additive is_add_submonoid.coe_zero] +@[simp, to_additive] lemma is_submonoid.coe_one [is_submonoid s] : ((1 : s) : α) = 1 := rfl -@[simp, to_additive is_add_submonoid.coe_add] +@[simp, to_additive] lemma is_submonoid.coe_mul [is_submonoid s] (a b : s) : ((a * b : s) : α) = a * b := rfl @[simp] lemma is_submonoid.coe_pow [is_submonoid s] (a : s) (n : ℕ) : ((a ^ n : s) : α) = a ^ n := @@ -185,27 +173,36 @@ by induction n; simp [*, pow_succ] @[simp] lemma is_add_submonoid.smul_coe {β : Type*} [add_monoid β] {s : set β} [is_add_submonoid s] (a : s) (n : ℕ) : ((add_monoid.smul n a : s) : β) = add_monoid.smul n a := by induction n; [refl, simp [*, succ_smul]] -attribute [to_additive is_add_submonoid.smul_coe] is_submonoid.coe_pow +attribute [to_additive smul_coe] is_submonoid.coe_pow -@[to_additive subtype_val.is_add_monoid_hom] +@[to_additive is_add_monoid_hom] instance subtype_val.is_monoid_hom [is_submonoid s] : is_monoid_hom (subtype.val : s → α) := { map_one := rfl, map_mul := λ _ _, rfl } -@[to_additive coe.is_add_monoid_hom] +@[to_additive is_add_monoid_hom] instance coe.is_monoid_hom [is_submonoid s] : is_monoid_hom (coe : s → α) := subtype_val.is_monoid_hom -@[to_additive subtype_mk.is_add_monoid_hom] +@[to_additive is_add_monoid_hom] instance subtype_mk.is_monoid_hom {γ : Type*} [monoid γ] [is_submonoid s] (f : γ → α) [is_monoid_hom f] (h : ∀ x, f x ∈ s) : is_monoid_hom (λ x, (⟨f x, h x⟩ : s)) := { map_one := subtype.eq (is_monoid_hom.map_one f), map_mul := λ x y, subtype.eq (is_monoid_hom.map_mul f x y) } -@[to_additive set_inclusion.is_add_monoid_hom] +@[to_additive is_add_monoid_hom] instance set_inclusion.is_monoid_hom (t : set α) [is_submonoid s] [is_submonoid t] (h : s ⊆ t) : is_monoid_hom (set.inclusion h) := subtype_mk.is_monoid_hom _ _ +namespace add_monoid + +inductive in_closure (s : set β) : β → Prop +| basic {a : β} : a ∈ s → in_closure a +| zero : in_closure 0 +| add {a b : β} : in_closure a → in_closure b → in_closure (a + b) + +end add_monoid + namespace monoid inductive in_closure (s : set α) : α → Prop @@ -213,24 +210,35 @@ inductive in_closure (s : set α) : α → Prop | one : in_closure 1 | mul {a b : α} : in_closure a → in_closure b → in_closure (a * b) +attribute [to_additive] monoid.in_closure +attribute [to_additive] monoid.in_closure.one +attribute [to_additive] monoid.in_closure.mul + +@[to_additive] def closure (s : set α) : set α := {a | in_closure s a } +@[to_additive is_add_submonoid] instance closure.is_submonoid (s : set α) : is_submonoid (closure s) := { one_mem := in_closure.one s, mul_mem := assume a b, in_closure.mul } +@[to_additive] theorem subset_closure {s : set α} : s ⊆ closure s := assume a, in_closure.basic +@[to_additive] theorem closure_subset {s t : set α} [is_submonoid t] (h : s ⊆ t) : closure s ⊆ t := assume a ha, by induction ha; simp [h _, *, is_submonoid.one_mem, is_submonoid.mul_mem] +@[to_additive] theorem closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t := closure_subset $ set.subset.trans h subset_closure +@[to_additive] theorem closure_singleton {x : α} : closure ({x} : set α) = powers x := set.eq_of_subset_of_subset (closure_subset $ set.singleton_subset_iff.2 $ powers.self_mem) $ is_submonoid.power_subset $ set.singleton_subset_iff.1 $ subset_closure +@[to_additive] lemma image_closure {β : Type*} [monoid β] (f : α → β) [is_monoid_hom f] (s : set α) : f '' closure s = closure (f '' s) := le_antisymm @@ -243,6 +251,7 @@ le_antisymm end (closure_subset $ set.image_subset _ subset_closure) +@[to_additive] theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a ∈ closure s) : (∃l:list α, (∀x∈l, x ∈ s) ∧ l.prod = a) := begin @@ -258,6 +267,7 @@ begin } end +@[to_additive] theorem mem_closure_union_iff {α : Type*} [comm_monoid α] {s t : set α} {x : α} : x ∈ closure (s ∪ t) ↔ ∃ y ∈ closure s, ∃ z ∈ closure t, y * z = x := ⟨λ hx, let ⟨L, HL1, HL2⟩ := exists_list_of_mem_closure hx in HL2 ▸ @@ -271,59 +281,3 @@ theorem mem_closure_union_iff {α : Type*} [comm_monoid α] {s t : set α} {x : end monoid -namespace add_monoid - -def closure (s : set β) : set β := @monoid.closure (multiplicative β) _ s -attribute [to_additive add_monoid.closure] monoid.closure - -instance closure.is_add_submonoid (s : set β) : is_add_submonoid (closure s) := -multiplicative.is_submonoid_iff.1 $ monoid.closure.is_submonoid s -attribute [to_additive add_monoid.closure.is_add_submonoid] monoid.closure.is_submonoid - -theorem subset_closure {s : set β} : s ⊆ closure s := -monoid.subset_closure -attribute [to_additive add_monoid.subset_closure] monoid.subset_closure - -theorem closure_subset {s t : set β} [is_add_submonoid t] : s ⊆ t → closure s ⊆ t := -monoid.closure_subset -attribute [to_additive add_monoid.closure_subset] monoid.closure_subset - -theorem closure_mono {s t : set β} (h : s ⊆ t) : closure s ⊆ closure t := -closure_subset $ set.subset.trans h subset_closure -attribute [to_additive add_monoid.closure_mono] monoid.closure_mono - -theorem closure_singleton {x : β} : closure ({x} : set β) = multiples x := -monoid.closure_singleton -attribute [to_additive add_monoid.closure_singleton] monoid.closure_singleton - -theorem exists_list_of_mem_closure {s : set β} {a : β} : - a ∈ closure s → ∃l:list β, (∀x∈l, x ∈ s) ∧ l.sum = a := -monoid.exists_list_of_mem_closure -attribute [to_additive add_monoid.exists_list_of_mem_closure] monoid.exists_list_of_mem_closure - -@[elab_as_eliminator] -theorem in_closure.rec_on {s : set β} {C : β → Prop} - {a : β} (H : a ∈ closure s) - (H1 : ∀ {a : β}, a ∈ s → C a) (H2 : C 0) - (H3 : ∀ {a b : β}, a ∈ closure s → b ∈ closure s → C a → C b → C (a + b)) : - C a := -monoid.in_closure.rec_on H (λ _, H1) H2 (λ _ _, H3) - -lemma image_closure {γ : Type*} [add_monoid γ] (f : β → γ) [is_add_monoid_hom f] (s : set β) : - f '' closure s = closure (f '' s) := -le_antisymm - begin - rintros _ ⟨x, hx, rfl⟩, - apply in_closure.rec_on hx; intros, - { solve_by_elim [subset_closure, set.mem_image_of_mem] }, - { rw [is_add_monoid_hom.map_zero f], apply is_add_submonoid.zero_mem }, - { rw [is_add_monoid_hom.map_add f], solve_by_elim [is_add_submonoid.add_mem] } - end - (closure_subset $ set.image_subset _ subset_closure) -attribute [to_additive add_monoid.image_closure] monoid.image_closure - -theorem mem_closure_union_iff {β : Type*} [add_comm_monoid β] {s t : set β} {x : β} : - x ∈ closure (s ∪ t) ↔ ∃ y ∈ closure s, ∃ z ∈ closure t, y + z = x := -monoid.mem_closure_union_iff - -end add_monoid diff --git a/src/linear_algebra/tensor_product.lean b/src/linear_algebra/tensor_product.lean index ff2ab898d86e2..6738e710ad0f4 100644 --- a/src/linear_algebra/tensor_product.lean +++ b/src/linear_algebra/tensor_product.lean @@ -162,15 +162,15 @@ notation x ` ⊗ₜ[`:100 R `] ` y := tmul R x y lemma add_tmul (m₁ m₂ : M) (n : N) : (m₁ + m₂) ⊗ₜ n = m₁ ⊗ₜ n + m₂ ⊗ₜ[R] n := eq.symm $ sub_eq_zero.1 $ eq.symm $ quotient.sound $ - group.in_closure.basic $ or.inl $ ⟨m₁, m₂, n, rfl⟩ + add_group.in_closure.basic $ or.inl $ ⟨m₁, m₂, n, rfl⟩ lemma tmul_add (m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ + n₂) = m ⊗ₜ n₁ + m ⊗ₜ[R] n₂ := eq.symm $ sub_eq_zero.1 $ eq.symm $ quotient.sound $ - group.in_closure.basic $ or.inr $ or.inl $ ⟨m, n₁, n₂, rfl⟩ + add_group.in_closure.basic $ or.inr $ or.inl $ ⟨m, n₁, n₂, rfl⟩ lemma smul_tmul (r : R) (m : M) (n : N) : (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n) := sub_eq_zero.1 $ eq.symm $ quotient.sound $ - group.in_closure.basic $ or.inr $ or.inr $ ⟨r, m, n, rfl⟩ + add_group.in_closure.basic $ or.inr $ or.inr $ ⟨r, m, n, rfl⟩ local attribute [instance] quotient_add_group.is_add_group_hom_quotient_lift diff --git a/src/meta/expr.lean b/src/meta/expr.lean index 297ce488f7d9b..10f84b2802649 100644 --- a/src/meta/expr.lean +++ b/src/meta/expr.lean @@ -16,6 +16,14 @@ Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lew -/ namespace name + +/-- Find the largest prefix `n` of a `name` such that `f n ≠ none`, then replace this prefix +with the value of `f n`. -/ +def map_prefix (f : name → option name) : name → name +| anonymous := anonymous +| (mk_string s n') := (f (mk_string s n')).get_or_else (mk_string s $ map_prefix n') +| (mk_numeral d n') := (f (mk_numeral d n')).get_or_else (mk_numeral d $ map_prefix n') + /-- If `nm` is a simple name (having only one string component) starting with `_`, then `deinternalize_field nm` removes the underscore. Otherwise, it does nothing. -/ meta def deinternalize_field : name → name | (mk_string s name.anonymous) := @@ -107,6 +115,14 @@ end level namespace expr open tactic +/-- Apply a function to each constant (inductive type, defined function etc) in an expression. -/ +protected meta def apply_replacement_fun (f : name → name) (e : expr) : expr := +e.replace $ λ e d, + match e with + | expr.const n ls := some $ expr.const (f n) ls + | _ := none + end + /-- Turns an expression into a positive natural number, assuming it is only built up from `has_one.one`, `bit0` and `bit1`. -/ protected meta def to_pos_nat : expr → option ℕ @@ -261,8 +277,14 @@ e.fold (return x) (λ d t, t >>= fn d) end environment namespace declaration - open tactic + +protected meta def update_with_fun (f : name → name) (tgt : name) (decl : declaration) : + declaration := +let decl := decl.update_name $ tgt in +let decl := decl.update_type $ decl.type.apply_replacement_fun f in +decl.update_value $ decl.value.apply_replacement_fun f + /-- Checks whether the declaration is declared in the current file. This is a simple wrapper around `environment.in_current_file'` -/ meta def in_current_file (d : declaration) : tactic bool := diff --git a/src/order/filter/pointwise.lean b/src/order/filter/pointwise.lean index 93176f5304554..abbbb84a9abd2 100644 --- a/src/order/filter/pointwise.lean +++ b/src/order/filter/pointwise.lean @@ -22,18 +22,19 @@ local attribute [instance] classical.prop_decidable pointwise_one pointwise_mul namespace filter open set -@[to_additive filter.pointwise_zero] +@[to_additive] def pointwise_one [has_one α] : has_one (filter α) := ⟨principal {1}⟩ local attribute [instance] pointwise_one -@[simp, to_additive filter.mem_pointwise_zero] +@[simp, to_additive] lemma mem_pointwise_one [has_one α] (s : set α) : s ∈ (1 : filter α) ↔ (1:α) ∈ s := calc s ∈ (1:filter α) ↔ {(1:α)} ⊆ s : iff.rfl ... ↔ (1:α) ∈ s : by simp +@[to_additive] def pointwise_mul [monoid α] : has_mul (filter α) := ⟨λf g, { sets := { s | ∃t₁∈f, ∃t₂∈g, t₁ * t₂ ⊆ s }, univ_sets := @@ -56,49 +57,21 @@ def pointwise_mul [monoid α] : has_mul (filter α) := ⟨λf g, subset.trans (pointwise_mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _)) t₁t₂⟩, end }⟩ -def pointwise_add [add_monoid α] : has_add (filter α) := ⟨λf g, -{ sets := { s | ∃t₁∈f, ∃t₂∈g, t₁ + t₂ ⊆ s }, - univ_sets := - begin - have h₁ : (∃x, x ∈ f.sets) := ⟨univ, univ_sets f⟩, - have h₂ : (∃x, x ∈ g.sets) := ⟨univ, univ_sets g⟩, - simpa using and.intro h₁ h₂ - end, - sets_of_superset := λx y hx hxy, - begin - rcases hx with ⟨t₁, ht₁, t₂, ht₂, t₁t₂⟩, - exact ⟨t₁, ht₁, t₂, ht₂, subset.trans t₁t₂ hxy⟩ - end, - inter_sets := λx y, - begin - simp only [exists_prop, mem_set_of_eq, subset_inter_iff], - rintros ⟨s₁, hs₁, s₂, hs₂, s₁s₂⟩ ⟨t₁, ht₁, t₂, ht₂, t₁t₂⟩, - exact ⟨s₁ ∩ t₁, inter_sets f hs₁ ht₁, s₂ ∩ t₂, inter_sets g hs₂ ht₂, - subset.trans (pointwise_add_subset_add (inter_subset_left _ _) (inter_subset_left _ _)) s₁s₂, - subset.trans (pointwise_add_subset_add (inter_subset_right _ _) (inter_subset_right _ _)) t₁t₂⟩, - end }⟩ - -attribute [to_additive filter.pointwise_add] pointwise_mul -attribute [to_additive filter.pointwise_add._proof_1] pointwise_mul._proof_1 -attribute [to_additive filter.pointwise_add._proof_2] pointwise_mul._proof_2 -attribute [to_additive filter.pointwise_add._proof_3] pointwise_mul._proof_3 -attribute [to_additive filter.pointwise_add.equations.eqn_1] filter.pointwise_mul.equations._eqn_1 - local attribute [instance] pointwise_mul pointwise_add -@[to_additive filter.mem_pointwise_add] +@[to_additive] lemma mem_pointwise_mul [monoid α] {f g : filter α} {s : set α} : s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s := iff.rfl -@[to_additive filter.add_mem_pointwise_add] +@[to_additive] lemma mul_mem_pointwise_mul [monoid α] {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) : s * t ∈ f * g := ⟨_, hs, _, ht, subset.refl _⟩ -@[to_additive filter.pointwise_add_le_add] +@[to_additive] lemma pointwise_mul_le_mul [monoid α] {f₁ f₂ g₁ g₂ : filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁ * g₁ ≤ f₂ * g₂ := assume _ ⟨s, hs, t, ht, hst⟩, ⟨s, hf hs, t, hg ht, hst⟩ -@[to_additive filter.pointwise_add_ne_bot] +@[to_additive] lemma pointwise_mul_ne_bot [monoid α] {f g : filter α} : f ≠ ⊥ → g ≠ ⊥ → f * g ≠ ⊥ := begin simp only [forall_sets_neq_empty_iff_neq_bot.symm], @@ -107,7 +80,7 @@ begin exact ne_empty_iff_exists_mem.2 ⟨x, ab hx⟩ end -@[to_additive filter.pointwise_add_assoc] +@[to_additive] lemma pointwise_mul_assoc [monoid α] (f g h : filter α) : f * g * h = f * (g * h) := begin ext s, split, @@ -127,7 +100,7 @@ end local attribute [instance] pointwise_mul_monoid -@[to_additive filter.pointwise_zero_add] +@[to_additive] lemma pointwise_one_mul [monoid α] (f : filter α) : 1 * f = f := begin ext s, split, @@ -139,7 +112,7 @@ begin refine ⟨(1:set α), mem_principal_self _, s, hs, by simp only [one_mul]⟩ } end -@[to_additive filter.pointwise_add_zero] +@[to_additive] lemma pointwise_mul_one [monoid α] (f : filter α) : f * 1 = f := begin ext s, split, @@ -151,7 +124,7 @@ begin refine ⟨s, hs, (1:set α), mem_principal_self _, by simp only [mul_one]⟩ } end -@[to_additive filter.pointwise_add_add_monoid] +@[to_additive pointwise_add_add_monoid] def pointwise_mul_monoid [monoid α] : monoid (filter α) := { mul_assoc := pointwise_mul_assoc, one_mul := pointwise_one_mul, @@ -166,7 +139,7 @@ open is_mul_hom variables [monoid α] [monoid β] {f : filter α} (m : α → β) -@[to_additive filter.map_pointwise_add] +@[to_additive] lemma map_pointwise_mul [is_mul_hom m] {f₁ f₂ : filter α} : map m (f₁ * f₂) = map m f₁ * map m f₂ := filter_eq $ set.ext $ assume s, begin @@ -182,7 +155,7 @@ begin (pointwise_mul_subset_mul (image_preimage_subset _ _) (image_preimage_subset _ _)) t₁t₂ }, end -@[to_additive filter.map_pointwise_zero] +@[to_additive] lemma map_pointwise_one [is_monoid_hom m] : map m (1:filter α) = 1 := le_antisymm (le_principal_iff.2 $ mem_map_sets_iff.2 ⟨(1:set α), by simp, @@ -203,10 +176,10 @@ def pointwise_add_map_is_add_monoid_hom {α : Type*} {β : Type*} [add_monoid α { map_zero := map_pointwise_zero m, map_add := λ _ _, map_pointwise_add m } -attribute [to_additive filter.pointwise_add_map_is_add_monoid_hom] pointwise_mul_map_is_monoid_hom +attribute [to_additive pointwise_add_map_is_add_monoid_hom] pointwise_mul_map_is_monoid_hom -- The other direction does not hold in general. -@[to_additive filter.comap_add_comap_le] +@[to_additive] lemma comap_mul_comap_le [is_mul_hom m] {f₁ f₂ : filter β} : comap m f₁ * comap m f₂ ≤ comap m (f₁ * f₂) := begin @@ -218,7 +191,7 @@ end variables {m} -@[to_additive filter.tendsto_add_add] +@[to_additive] lemma tendsto_mul_mul [is_mul_hom m] {f₁ g₁ : filter α} {f₂ g₂ : filter β} : tendsto m f₁ f₂ → tendsto m g₁ g₂ → tendsto m (f₁ * g₁) (f₂ * g₂) := assume hf hg, by { rw [tendsto, map_pointwise_mul m], exact pointwise_mul_le_mul hf hg } diff --git a/src/tactic/algebra.lean b/src/tactic/algebra.lean index 099afdee506ba..6c9c057ae8f41 100644 --- a/src/tactic/algebra.lean +++ b/src/tactic/algebra.lean @@ -28,13 +28,22 @@ do cs ← get_ancestors cl, end tactic attribute [ancestor has_mul] semigroup +attribute [ancestor semigroup] comm_semigroup attribute [ancestor semigroup has_one] monoid +attribute [ancestor monoid comm_semigroup] comm_monoid attribute [ancestor monoid has_inv] group -attribute [ancestor group has_comm] comm_group +attribute [ancestor group comm_monoid] comm_group attribute [ancestor has_add] add_semigroup +attribute [ancestor add_semigroup] add_comm_semigroup attribute [ancestor add_semigroup has_zero] add_monoid +attribute [ancestor add_monoid add_comm_semigroup] add_comm_monoid attribute [ancestor add_monoid has_neg] add_group -attribute [ancestor add_group has_add_comm] add_comm_group +attribute [ancestor add_group add_comm_monoid] add_comm_group + +attribute [ancestor semigroup] left_cancel_semigroup +attribute [ancestor semigroup] right_cancel_semigroup +attribute [ancestor add_semigroup] add_left_cancel_semigroup +attribute [ancestor add_semigroup] add_right_cancel_semigroup attribute [ancestor ring has_inv zero_ne_one_class] division_ring attribute [ancestor division_ring comm_ring] field diff --git a/src/tactic/transport.lean b/src/tactic/transport.lean new file mode 100644 index 0000000000000..cf6500cb51aab --- /dev/null +++ b/src/tactic/transport.lean @@ -0,0 +1,29 @@ +import meta.expr meta.rb_map + +namespace tactic + +private meta def transport_with_prefix_fun_aux (f : name → option name) (pre tgt_pre : name) + (attrs : list name) : + name → command := +λ src, +do + let tgt := src.map_prefix (λ n, if n = pre then some tgt_pre else none), + (get_decl tgt >> skip) <|> + do + decl ← get_decl src, + (decl.type.list_names_with_prefix pre).mfold () (λ n _, transport_with_prefix_fun_aux n), + (decl.value.list_names_with_prefix pre).mfold () (λ n _, transport_with_prefix_fun_aux n), + add_decl (decl.update_with_fun (name.map_prefix f) tgt), + attrs.mmap' (λ n, copy_attribute n src tt tgt) + +meta def transport_with_prefix_fun (f : name → option name) (src tgt : name) (attrs : list name) : + command := +do transport_with_prefix_fun_aux f src tgt attrs src, + ls ← get_eqn_lemmas_for tt src, + ls.mmap' $ transport_with_prefix_fun_aux f src tgt attrs + +meta def transport_with_prefix_dict (dict : name_map name) (src tgt : name) (attrs : list name) : + command := +transport_with_prefix_fun dict.find src tgt attrs + +end tactic diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean index 663f6873be462..fa7b21c6cd041 100644 --- a/src/topology/algebra/group.lean +++ b/src/topology/algebra/group.lean @@ -19,97 +19,83 @@ variables {α : Type u} {β : Type v} {γ : Type w} section topological_group -/-- A topological group is a group in which the multiplication and inversion operations are -continuous. -/ -class topological_group (α : Type*) [topological_space α] [group α] - extends topological_monoid α : Prop := -(continuous_inv : continuous (λa:α, a⁻¹)) - /-- A topological (additive) group is a group in which the addition and negation operations are continuous. -/ class topological_add_group (α : Type u) [topological_space α] [add_group α] extends topological_add_monoid α : Prop := (continuous_neg : continuous (λa:α, -a)) -attribute [to_additive topological_add_group] topological_group -attribute [to_additive topological_add_group.mk] topological_group.mk -attribute [to_additive topological_add_group.continuous_neg] topological_group.continuous_inv -attribute [to_additive topological_add_group.to_topological_add_monoid] topological_group.to_topological_monoid +/-- A topological group is a group in which the multiplication and inversion operations are +continuous. -/ +@[to_additive topological_add_group] +class topological_group (α : Type*) [topological_space α] [group α] + extends topological_monoid α : Prop := +(continuous_inv : continuous (λa:α, a⁻¹)) variables [topological_space α] [group α] -@[to_additive continuous_neg'] +@[to_additive] lemma continuous_inv' [topological_group α] : continuous (λx:α, x⁻¹) := topological_group.continuous_inv α -@[to_additive continuous_neg] +@[to_additive] lemma continuous_inv [topological_group α] [topological_space β] {f : β → α} (hf : continuous f) : continuous (λx, (f x)⁻¹) := continuous_inv'.comp hf -@[to_additive continuous_on.neg] +@[to_additive] lemma continuous_on.inv [topological_group α] [topological_space β] {f : β → α} {s : set β} (hf : continuous_on f s) : continuous_on (λx, (f x)⁻¹) s := continuous_inv'.comp_continuous_on hf -@[to_additive tendsto_neg] +@[to_additive] lemma tendsto_inv [topological_group α] {f : β → α} {x : filter β} {a : α} (hf : tendsto f x (nhds a)) : tendsto (λx, (f x)⁻¹) x (nhds a⁻¹) := tendsto.comp (continuous_iff_continuous_at.mp (topological_group.continuous_inv α) a) hf -@[to_additive prod.topological_add_group] +@[to_additive topological_add_group] instance [topological_group α] [topological_space β] [group β] [topological_group β] : topological_group (α × β) := { continuous_inv := continuous.prod_mk (continuous_inv continuous_fst) (continuous_inv continuous_snd) } attribute [instance] prod.topological_add_group +@[to_additive] protected def homeomorph.mul_left [topological_group α] (a : α) : α ≃ₜ α := { continuous_to_fun := continuous_mul continuous_const continuous_id, continuous_inv_fun := continuous_mul continuous_const continuous_id, .. equiv.mul_left a } -attribute [to_additive homeomorph.add_left._proof_1] homeomorph.mul_left._proof_1 -attribute [to_additive homeomorph.add_left._proof_2] homeomorph.mul_left._proof_2 -attribute [to_additive homeomorph.add_left._proof_3] homeomorph.mul_left._proof_3 -attribute [to_additive homeomorph.add_left._proof_4] homeomorph.mul_left._proof_4 -attribute [to_additive homeomorph.add_left] homeomorph.mul_left -@[to_additive is_open_map_add_left] +@[to_additive] lemma is_open_map_mul_left [topological_group α] (a : α) : is_open_map (λ x, a * x) := (homeomorph.mul_left a).is_open_map -@[to_additive is_closed_map_add_left] +@[to_additive] lemma is_closed_map_mul_left [topological_group α] (a : α) : is_closed_map (λ x, a * x) := (homeomorph.mul_left a).is_closed_map +@[to_additive] protected def homeomorph.mul_right {α : Type*} [topological_space α] [group α] [topological_group α] (a : α) : α ≃ₜ α := { continuous_to_fun := continuous_mul continuous_id continuous_const, continuous_inv_fun := continuous_mul continuous_id continuous_const, .. equiv.mul_right a } -attribute [to_additive homeomorph.add_right._proof_1] homeomorph.mul_right._proof_1 -attribute [to_additive homeomorph.add_right._proof_2] homeomorph.mul_right._proof_2 -attribute [to_additive homeomorph.add_right._proof_3] homeomorph.mul_right._proof_3 -attribute [to_additive homeomorph.add_right._proof_4] homeomorph.mul_right._proof_4 -attribute [to_additive homeomorph.add_right] homeomorph.mul_right -@[to_additive is_open_map_add_right] +@[to_additive] lemma is_open_map_mul_right [topological_group α] (a : α) : is_open_map (λ x, x * a) := (homeomorph.mul_right a).is_open_map -@[to_additive is_closed_map_add_right] +@[to_additive] lemma is_closed_map_mul_right [topological_group α] (a : α) : is_closed_map (λ x, x * a) := (homeomorph.mul_right a).is_closed_map +@[to_additive] protected def homeomorph.inv (α : Type*) [topological_space α] [group α] [topological_group α] : α ≃ₜ α := { continuous_to_fun := continuous_inv', continuous_inv_fun := continuous_inv', .. equiv.inv α } -attribute [to_additive homeomorph.neg._proof_1] homeomorph.inv._proof_1 -attribute [to_additive homeomorph.neg._proof_2] homeomorph.inv._proof_2 -attribute [to_additive homeomorph.neg] homeomorph.inv @[to_additive exists_nhds_half] lemma exists_nhds_split [topological_group α] {s : set α} (hs : s ∈ nhds (1 : α)) : @@ -147,7 +133,7 @@ end section variable (α) -@[to_additive nhds_zero_symm] +@[to_additive] lemma nhds_one_symm [topological_group α] : comap (λr:α, r⁻¹) (nhds (1 : α)) = nhds (1 : α) := begin have lim : tendsto (λr:α, r⁻¹) (nhds 1) (nhds 1), @@ -157,7 +143,7 @@ begin end end -@[to_additive nhds_translation_add_neg] +@[to_additive] lemma nhds_translation_mul_inv [topological_group α] (x : α) : comap (λy:α, y * x⁻¹) (nhds 1) = nhds x := begin @@ -169,7 +155,7 @@ begin exact tendsto_mul tendsto_id tendsto_const_nhds } end -@[to_additive topological_add_group.ext] +@[to_additive] lemma topological_group.ext {G : Type*} [group G] {t t' : topological_space G} (tg : @topological_group G t _) (tg' : @topological_group G t' _) (h : @nhds G t 1 = @nhds G t' 1) : t = t' := @@ -180,12 +166,10 @@ end topological_group section quotient_topological_group variables [topological_space α] [group α] [topological_group α] (N : set α) [normal_subgroup N] -@[to_additive quotient_add_group.quotient.topological_space] +@[to_additive] instance : topological_space (quotient_group.quotient N) := by dunfold quotient_group.quotient; apply_instance -attribute [instance] quotient_add_group.quotient.topological_space - open quotient_group @[to_additive quotient_add_group_saturate] lemma quotient_group_saturate (s : set α) : @@ -199,7 +183,7 @@ begin ⟨a, ha, by simp only [eq.symm, (mul_assoc _ _ _).symm, inv_mul_cancel_left, hi]⟩ } end -@[to_additive quotient_add_group.open_coe] +@[to_additive] lemma quotient_group.open_coe : is_open_map (coe : α → quotient N) := begin intros s s_op, @@ -347,7 +331,7 @@ local attribute [instance] section variables [topological_space α] [group α] [topological_group α] -@[to_additive is_open_pointwise_add_left] +@[to_additive] lemma is_open_pointwise_mul_left {s t : set α} : is_open t → is_open (s * t) := λ ht, begin have : ∀a, is_open ((λ (x : α), a * x) '' t), @@ -356,7 +340,7 @@ begin exact is_open_Union (λa, is_open_Union $ λha, this _), end -@[to_additive is_open_pointwise_add_right] +@[to_additive] lemma is_open_pointwise_mul_right {s t : set α} : is_open s → is_open (s * t) := λ hs, begin have : ∀a, is_open ((λ (x : α), x * a) '' s), @@ -402,7 +386,7 @@ end section variables [topological_space α] [comm_group α] [topological_group α] -@[to_additive nhds_pointwise_add] +@[to_additive] lemma nhds_pointwise_mul (x y : α) : nhds (x * y) = nhds x * nhds y := filter_eq $ set.ext $ assume s, begin @@ -425,7 +409,7 @@ begin { simp only [inv_mul_cancel_right] } } end -@[to_additive nhds_is_add_hom] +@[to_additive] def nhds_is_mul_hom : is_mul_hom (λx:α, nhds x) := ⟨λ_ _, nhds_pointwise_mul _ _⟩ end diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean index 7439dce31e13b..7e2eb67283b0d 100644 --- a/src/topology/algebra/monoid.lean +++ b/src/topology/algebra/monoid.lean @@ -30,31 +30,29 @@ class topological_add_monoid (α : Type u) [topological_space α] [add_monoid α (continuous_add : continuous (λp:α×α, p.1 + p.2)) attribute [to_additive topological_add_monoid] topological_monoid -attribute [to_additive topological_add_monoid.mk] topological_monoid.mk -attribute [to_additive topological_add_monoid.continuous_add] topological_monoid.continuous_mul section variables [topological_space α] [monoid α] [topological_monoid α] -@[to_additive continuous_add'] +@[to_additive] lemma continuous_mul' : continuous (λp:α×α, p.1 * p.2) := topological_monoid.continuous_mul α -@[to_additive continuous_add] +@[to_additive] lemma continuous_mul [topological_space β] {f : β → α} {g : β → α} (hf : continuous f) (hg : continuous g) : continuous (λx, f x * g x) := continuous_mul'.comp (hf.prod_mk hg) -@[to_additive continuous_add_left] +@[to_additive] lemma continuous_mul_left (a : α) : continuous (λ b:α, a * b) := continuous_mul continuous_const continuous_id -@[to_additive continuous_add_right] +@[to_additive] lemma continuous_mul_right (a : α) : continuous (λ b:α, b * a) := continuous_mul continuous_id continuous_const -@[to_additive continuous_on.add] +@[to_additive] lemma continuous_on.mul [topological_space β] {f : β → α} {g : β → α} {s : set β} (hf : continuous_on f s) (hg : continuous_on g s) : continuous_on (λx, f x * g x) s := @@ -65,17 +63,17 @@ lemma continuous_pow : ∀ n : ℕ, continuous (λ a : α, a ^ n) | 0 := by simpa using continuous_const | (k+1) := show continuous (λ (a : α), a * a ^ k), from continuous_mul continuous_id (continuous_pow _) -@[to_additive tendsto_add'] +@[to_additive] lemma tendsto_mul' {a b : α} : tendsto (λp:α×α, p.fst * p.snd) (nhds (a, b)) (nhds (a * b)) := continuous_iff_continuous_at.mp (topological_monoid.continuous_mul α) (a, b) -@[to_additive tendsto_add] +@[to_additive] lemma tendsto_mul {f : β → α} {g : β → α} {x : filter β} {a b : α} (hf : tendsto f x (nhds a)) (hg : tendsto g x (nhds b)) : tendsto (λx, f x * g x) x (nhds (a * b)) := tendsto.comp (by rw [←nhds_prod_eq]; exact tendsto_mul') (hf.prod_mk hg) -@[to_additive tendsto_list_sum] +@[to_additive] lemma tendsto_list_prod {f : γ → β → α} {x : filter β} {a : γ → α} : ∀l:list γ, (∀c∈l, tendsto (f c) x (nhds (a c))) → tendsto (λb, (l.map (λc, f c b)).prod) x (nhds ((l.map a).prod)) @@ -88,14 +86,14 @@ lemma tendsto_list_prod {f : γ → β → α} {x : filter β} {a : γ → α} : (tendsto_list_prod l (assume c hc, h c (list.mem_cons_of_mem _ hc))) end -@[to_additive continuous_list_sum] +@[to_additive] lemma continuous_list_prod [topological_space β] {f : γ → β → α} (l : list γ) (h : ∀c∈l, continuous (f c)) : continuous (λa, (l.map (λc, f c a)).prod) := continuous_iff_continuous_at.2 $ assume x, tendsto_list_prod l $ assume c hc, continuous_iff_continuous_at.1 (h c hc) x -@[to_additive prod.topological_add_monoid] +@[to_additive topological_add_monoid] instance [topological_space β] [monoid β] [topological_monoid β] : topological_monoid (α × β) := ⟨continuous.prod_mk (continuous_mul (continuous_fst.comp continuous_fst) (continuous_fst.comp continuous_snd)) @@ -108,28 +106,28 @@ end section variables [topological_space α] [comm_monoid α] [topological_monoid α] -@[to_additive tendsto_multiset_sum] +@[to_additive] lemma tendsto_multiset_prod {f : γ → β → α} {x : filter β} {a : γ → α} (s : multiset γ) : (∀c∈s, tendsto (f c) x (nhds (a c))) → tendsto (λb, (s.map (λc, f c b)).prod) x (nhds ((s.map a).prod)) := by { rcases s with ⟨l⟩, simp, exact tendsto_list_prod l } -@[to_additive tendsto_finset_sum] +@[to_additive] lemma tendsto_finset_prod {f : γ → β → α} {x : filter β} {a : γ → α} (s : finset γ) : (∀c∈s, tendsto (f c) x (nhds (a c))) → tendsto (λb, s.prod (λc, f c b)) x (nhds (s.prod a)) := tendsto_multiset_prod _ -@[to_additive continuous_multiset_sum] +@[to_additive] lemma continuous_multiset_prod [topological_space β] {f : γ → β → α} (s : multiset γ) : (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).prod) := by { rcases s with ⟨l⟩, simp, exact continuous_list_prod l } -@[to_additive continuous_finset_sum] +@[to_additive] lemma continuous_finset_prod [topological_space β] {f : γ → β → α} (s : finset γ) : (∀c∈s, continuous (f c)) → continuous (λa, s.prod (λc, f c a)) := continuous_multiset_prod _ -@[to_additive is_add_submonoid.mem_nhds_zero] +@[to_additive] lemma is_submonoid.mem_nhds_one (β : set α) [is_submonoid β] (oβ : is_open β) : β ∈ nhds (1 : α) := mem_nhds_sets_iff.2 ⟨β, (by refl), oβ, is_submonoid.one_mem _⟩ diff --git a/src/topology/algebra/open_subgroup.lean b/src/topology/algebra/open_subgroup.lean index 5e471e051dc4e..302801104cadd 100644 --- a/src/topology/algebra/open_subgroup.lean +++ b/src/topology/algebra/open_subgroup.lean @@ -10,67 +10,63 @@ variables (G : Type*) [group G] [topological_space G] [topological_group G] @[to_additive open_add_subgroup] def open_subgroup := { U : set G // is_open U ∧ is_subgroup U } +@[to_additive] instance open_subgroup.has_coe : has_coe (open_subgroup G) (opens G) := ⟨λ U, ⟨U.1, U.2.1⟩⟩ end -section -open topological_space -variables (G : Type*) [add_group G] [topological_space G] [topological_add_group G] - -instance open_add_subgroup.has_coe : - has_coe (open_add_subgroup G) (opens G) := ⟨λ U, ⟨U.1, U.2.1⟩⟩ - -attribute [to_additive open_add_subgroup.has_coe] open_subgroup.has_coe -attribute [to_additive open_add_subgroup.has_coe.equations._eqn_1] open_subgroup.has_coe.equations._eqn_1 - -end +-- Tell Lean that `open_add_subgroup` is a namespace +namespace open_add_subgroup +end open_add_subgroup namespace open_subgroup open function lattice topological_space variables {G : Type*} [group G] [topological_space G] [topological_group G] variables {U V : open_subgroup G} -@[to_additive open_add_subgroup.has_mem] +@[to_additive] instance : has_mem G (open_subgroup G) := ⟨λ g U, g ∈ (U : set G)⟩ -attribute [to_additive open_add_subgroup.has_mem.equations._eqn_1] open_subgroup.has_mem.equations._eqn_1 - -@[to_additive open_add_subgroup.ext] +@[to_additive] lemma ext : (U = V) ↔ ((U : set G) = V) := by cases U; cases V; split; intro h; try {congr}; assumption -@[extensionality, to_additive open_add_subgroup.ext'] +@[extensionality, to_additive] lemma ext' (h : (U : set G) = V) : (U = V) := ext.mpr h -@[to_additive open_add_subgroup.coe_injective] +@[to_additive] lemma coe_injective : injective (λ U : open_subgroup G, (U : set G)) := λ U V h, ext' h -@[to_additive open_add_subgroup.is_add_subgroup] +@[to_additive is_add_subgroup] instance : is_subgroup (U : set G) := U.2.2 variable (U) -@[to_additive open_add_subgroup.is_open] +@[to_additive] protected lemma is_open : is_open (U : set G) := U.2.1 +@[to_additive] protected lemma one_mem : (1 : G) ∈ U := is_submonoid.one_mem (U : set G) +@[to_additive] protected lemma inv_mem {g : G} (h : g ∈ U) : g⁻¹ ∈ U := @is_subgroup.inv_mem G _ U _ g h +@[to_additive] protected lemma mul_mem {g₁ g₂ : G} (h₁ : g₁ ∈ U) (h₂ : g₂ ∈ U) : g₁ * g₂ ∈ U := @is_submonoid.mul_mem G _ U _ g₁ g₂ h₁ h₂ +@[to_additive] lemma mem_nhds_one : (U : set G) ∈ nhds (1 : G) := mem_nhds_sets U.is_open U.one_mem variable {U} +@[to_additive] instance : inhabited (open_subgroup G) := { default := ⟨set.univ, ⟨is_open_univ, by apply_instance⟩⟩ } -@[to_additive open_add_subgroup.is_open_of_nonempty_open_subset] +@[to_additive] lemma is_open_of_nonempty_open_subset {s : set G} [is_subgroup s] (h : ∃ U : opens G, nonempty U ∧ (U : set G) ⊆ s) : is_open s := @@ -96,12 +92,12 @@ begin rw [← mul_assoc, mul_right_inv, one_mul] } end +@[to_additive is_open_of_open_add_subgroup] lemma is_open_of_open_subgroup {s : set G} [is_subgroup s] (h : ∃ U : open_subgroup G, (U : set G) ⊆ s) : is_open s := is_open_of_nonempty_open_subset $ let ⟨U, hU⟩ := h in ⟨U, ⟨⟨1, U.one_mem⟩⟩, hU⟩ - -@[to_additive open_add_subgroup.is_closed] +@[to_additive] lemma is_closed (U : open_subgroup G) : is_closed (U : set G) := begin show is_open (-(U : set G)), @@ -123,13 +119,16 @@ end section variables {H : Type*} [group H] [topological_space H] [topological_group H] +@[to_additive] def prod (U : open_subgroup G) (V : open_subgroup H) : open_subgroup (G × H) := ⟨(U : set G).prod (V : set H), is_open_prod U.is_open V.is_open, by apply_instance⟩ end +@[to_additive] instance : partial_order (open_subgroup G) := partial_order.lift _ coe_injective (by apply_instance) +@[to_additive] instance : semilattice_inf_top (open_subgroup G) := { inf := λ U V, ⟨(U : set G) ∩ V, is_open_inter U.is_open V.is_open, by apply_instance⟩, inf_le_left := λ U V, set.inter_subset_left _ _, @@ -139,6 +138,7 @@ instance : semilattice_inf_top (open_subgroup G) := le_top := λ U, set.subset_univ _, ..open_subgroup.partial_order } +@[to_additive] instance : semilattice_sup_top (open_subgroup G) := { sup := λ U V, { val := group.closure ((U : set G) ∪ V), @@ -154,97 +154,12 @@ instance : semilattice_sup_top (open_subgroup G) := sup_le := λ U V W hU hV, group.closure_subset $ set.union_subset hU hV, ..open_subgroup.lattice.semilattice_inf_top } -@[simp] lemma coe_inf : (↑(U ⊓ V) : set G) = (U : set G) ∩ V := rfl +@[simp, to_additive] lemma coe_inf : (↑(U ⊓ V) : set G) = (U : set G) ∩ V := rfl -lemma le_iff : U ≤ V ↔ (U : set G) ⊆ V := iff.rfl +@[to_additive] lemma le_iff : U ≤ V ↔ (U : set G) ⊆ V := iff.rfl end open_subgroup -namespace open_add_subgroup -open lattice -variables {G : Type*} [add_group G] [topological_space G] [topological_add_group G] -variables {U V : open_add_subgroup G} - -variable (U) - -protected lemma zero_mem : (0 : G) ∈ U := is_add_submonoid.zero_mem (U : set G) -attribute [to_additive open_add_subgroup.zero_mem] open_subgroup.one_mem - -protected lemma neg_mem {g : G} (h : g ∈ U) : -g ∈ U := - @is_add_subgroup.neg_mem G _ U _ g h -attribute [to_additive open_add_subgroup.neg_mem] open_subgroup.inv_mem - -protected lemma add_mem {g₁ g₂ : G} (h₁ : g₁ ∈ U) (h₂ : g₂ ∈ U) : g₁ + g₂ ∈ U := - @is_add_submonoid.add_mem G _ U _ g₁ g₂ h₁ h₂ -attribute [to_additive open_add_subgroup.add_mem] open_subgroup.mul_mem - -lemma mem_nhds_zero : (U : set G) ∈ nhds (0 : G) := -mem_nhds_sets U.is_open U.zero_mem -attribute [to_additive open_add_subgroup.mem_nhds_zero] open_subgroup.mem_nhds_one - -variable {U} - -lemma is_open_of_open_add_subgroup {s : set G} [_root_.is_add_subgroup s] - (h : ∃ U : open_add_subgroup G, (U : set G) ⊆ s) : _root_.is_open s := -is_open_of_nonempty_open_subset $ let ⟨U, hU⟩ := h in ⟨U, ⟨⟨0, U.zero_mem⟩⟩, hU⟩ - -attribute [to_additive open_add_subgroup.is_open_of_open_add_subgroup] -open_subgroup.is_open_of_open_subgroup - -section -variables {H : Type*} [add_group H] [topological_space H] [topological_add_group H] - -def prod (U : open_add_subgroup G) (V : open_add_subgroup H) : open_add_subgroup (G × H) := -⟨(U : set G).prod (V : set H), is_open_prod U.is_open V.is_open, by apply_instance⟩ -attribute [to_additive open_add_subgroup.prod] open_subgroup.prod -attribute [to_additive open_add_subgroup.prod.equations._eqn_1] open_subgroup.prod.equations._eqn_1 - -end - -instance : inhabited (open_add_subgroup G) := -{ default := ⟨set.univ, ⟨is_open_univ, by apply_instance⟩⟩ } -attribute [to_additive open_add_subgroup.inhabited] open_subgroup.inhabited - -instance : partial_order (open_add_subgroup G) := partial_order.lift _ coe_injective (by apply_instance) -attribute [to_additive open_add_subgroup.partial_order] open_subgroup.partial_order -attribute [to_additive open_add_subgroup.partial_order.equations._eqn_1] open_subgroup.partial_order.equations._eqn_1 - -instance : semilattice_inf_top (open_add_subgroup G) := -{ inf := λ U V, ⟨(U : set G) ∩ V, is_open_inter U.is_open V.is_open, by apply_instance⟩, - inf_le_left := λ U V, set.inter_subset_left _ _, - inf_le_right := λ U V, set.inter_subset_right _ _, - le_inf := λ U V W hV hW, set.subset_inter hV hW, - top := default _, - le_top := λ U, set.subset_univ _, - ..open_add_subgroup.partial_order } -attribute [to_additive open_add_subgroup.lattice.semilattice_inf_top] open_subgroup.lattice.semilattice_inf_top -attribute [to_additive open_add_subgroup.lattice.semilattice_inf_top.equations._eqn_1] open_subgroup.lattice.semilattice_inf_top.equations._eqn_1 - -instance : semilattice_sup_top (open_add_subgroup G) := -{ sup := λ U V, - { val := add_group.closure ((U : set G) ∪ V), - property := - begin - have subgrp := _, refine ⟨_, subgrp⟩, - { refine is_open_of_open_add_subgroup _, - exact ⟨U, set.subset.trans (set.subset_union_left _ _) add_group.subset_closure⟩ }, - { apply_instance } - end }, - le_sup_left := λ U V, set.subset.trans (set.subset_union_left _ _) group.subset_closure, - le_sup_right := λ U V, set.subset.trans (set.subset_union_right _ _) group.subset_closure, - sup_le := λ U V W hU hV, group.closure_subset $ set.union_subset hU hV, - ..open_add_subgroup.lattice.semilattice_inf_top } -attribute [to_additive open_add_subgroup.lattice.semilattice_sup_top] open_subgroup.lattice.semilattice_sup_top -attribute [to_additive open_add_subgroup.lattice.semilattice_sup_top.equations._eqn_1] open_subgroup.lattice.semilattice_sup_top.equations._eqn_1 - -@[simp] lemma coe_inf : (↑(U ⊓ V) : set G) = (U : set G) ∩ V := rfl -attribute [to_additive open_add_subgroup.coe_inf] open_subgroup.coe_inf - -lemma le_iff : U ≤ V ↔ (U : set G) ⊆ V := iff.rfl -attribute [to_additive open_add_subgroup.le_iff] open_subgroup.le_iff - -end open_add_subgroup - namespace submodule open open_add_subgroup variables {R : Type*} {M : Type*} [comm_ring R]