[Merged by Bors] - feat(algebra/direct_sum): specialize submodule_is_internal.independent to add_subgroup

src/algebra/direct_sum/module.lean

@@ -258,4 +258,16 @@ lemma submodule_is_internal_iff_independent_and_supr_eq_top {R M : Type*}
 ⟨λ i, ⟨i.independent, i.supr_eq_top⟩,
  and.rec submodule_is_internal_of_independent_of_supr_eq_top⟩
 
+/-! Now copy the lemmas for subgroup and submonoids. -/
+
+lemma add_submonoid_is_internal.independent {M : Type*} [add_comm_monoid M]
+  {A : ι → add_submonoid M} (h : add_submonoid_is_internal A) :
+  complete_lattice.independent A :=
+complete_lattice.independent_of_dfinsupp_sum_add_hom_injective _ h.injective
+
+lemma add_subgroup_is_internal.independent {M : Type*} [add_comm_group M]
+  {A : ι → add_subgroup M} (h : add_subgroup_is_internal A) :
+  complete_lattice.independent A :=
+complete_lattice.independent_of_dfinsupp_sum_add_hom_injective' _ h.injective
+
 end direct_sum

src/linear_algebra/dfinsupp.lean

@@ -324,6 +324,18 @@ begin
   simpa [eq_comm] using this,
 end
 
+/- If `dfinsupp.sum_add_hom` applied with `add_submonoid.subtype` is injective then the additive
+submonoids are independent. -/
+lemma independent_of_dfinsupp_sum_add_hom_injective (p : ι → add_submonoid N)
+  (h : function.injective (sum_add_hom (λ i, (p i).subtype))) :
+  independent p :=
+begin
+  obtain p_eq : add_submonoid.to_nat_submodule.symm ∘ add_submonoid.to_nat_submodule ∘ p = p :=
+    funext (λ i, order_iso.symm_apply_apply _ _),
+  rw ←p_eq at ⊢ h,
+  exact (independent_of_dfinsupp_lsum_injective _ h).map_order_iso _,
+end
+
 /-- Combining `dfinsupp.lsum` with `linear_map.to_span_singleton` is the same as `finsupp.total` -/
 lemma lsum_comp_map_range_to_span_singleton
   [Π (m : R), decidable (m ≠ 0)]
@@ -340,6 +352,19 @@ end semiring
 section ring
 variables [ring R] [add_comm_group N] [module R N]
 
+
+/- If `dfinsupp.sum_add_hom` applied with `add_submonoid.subtype` is injective then the additive
+subgroups are independent. -/
+lemma independent_of_dfinsupp_sum_add_hom_injective' (p : ι → add_subgroup N)
+  (h : function.injective (sum_add_hom (λ i, (p i).subtype))) :
+  independent p :=
+begin
+  obtain p_eq : add_subgroup.to_int_submodule.symm ∘ add_subgroup.to_int_submodule ∘ p = p :=
+    funext (λ i, order_iso.symm_apply_apply _ _),
+  rw ←p_eq at ⊢ h,
+  exact (independent_of_dfinsupp_lsum_injective _ h).map_order_iso _,
+end
+
 /-- The canonical map out of a direct sum of a family of submodules is injective when the submodules
 are `complete_lattice.independent`.
 
@@ -366,6 +391,17 @@ begin
     add_eq_zero_iff_eq_neg, ←submodule.coe_neg] at hm,
 end
 
+/-- The canonical map out of a direct sum of a family of additive subgroups is injective when the
+additive subgroups are `complete_lattice.independent`. -/
+lemma independent.dfinsupp_sum_add_hom_injective {p : ι → add_subgroup N}
+  (h : independent p) : function.injective (sum_add_hom (λ i, (p i).subtype)) :=
+begin
+  obtain p_eq : add_subgroup.to_int_submodule.symm ∘ add_subgroup.to_int_submodule ∘ p = p :=
+    funext (λ i, order_iso.symm_apply_apply _ _),
+  rw ←p_eq,
+  exact (h.map_order_iso _).dfinsupp_lsum_injective,
+end
+
 /-- A family of submodules over an additive group are independent if and only iff `dfinsupp.lsum`
 applied with `submodule.subtype` is injective.
 
@@ -375,6 +411,12 @@ lemma independent_iff_dfinsupp_lsum_injective (p : ι → submodule R N) :
   independent p ↔ function.injective (lsum ℕ (λ i, (p i).subtype)) :=
 ⟨independent.dfinsupp_lsum_injective, independent_of_dfinsupp_lsum_injective p⟩
 
+/-- A family of additive subgroups over an additive group are independent if and only iff
+`dfinsupp.sum_add_hom` applied with `add_subgroup.subtype` is injective. -/
+lemma independent_iff_dfinsupp_sum_add_hom_injective (p : ι → add_subgroup N) :
+  independent p ↔ function.injective (sum_add_hom (λ i, (p i).subtype)) :=
+⟨independent.dfinsupp_sum_add_hom_injective, independent_of_dfinsupp_sum_add_hom_injective' p⟩
+
 omit dec_ι
 /-- If a family of submodules is `independent`, then a choice of nonzero vector from each submodule
 forms a linearly independent family. -/

src/order/complete_lattice.lean

@@ -1334,7 +1334,7 @@ lemma independent.mono {ι : Type*} {α : Type*} [complete_lattice α]
   independent t :=
 λ i, (hs i).mono (hst i) (supr_le_supr $ λ j, supr_le_supr $ λ _, hst j)
 
-/-- Composing an indepedent indexed family with an injective function on the index results in
+/-- Composing an independent indexed family with an injective function on the index results in
 another indepedendent indexed family. -/
 lemma independent.comp {ι ι' : Sort*} {α : Type*} [complete_lattice α]
   {s : ι → α} (hs : independent s) (f : ι' → ι) (hf : function.injective f) :
@@ -1344,6 +1344,22 @@ lemma independent.comp {ι ι' : Sort*} {α : Type*} [complete_lattice α]
   exact supr_le_supr_const hf.ne,
 end
 
+/-- Composing an indepedent indexed family with an order isomorphism on the elements results in
+another indepedendent indexed family. -/
+/-- Composing an indepedent indexed family with an order isomorphism on the elements results in
+another indepedendent indexed family. -/
+lemma independent.map_order_iso {ι : Sort*} {α β : Type*}
+  [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} (ha : independent a) :
+  independent (f ∘ a) :=
+λ i, ((ha i).map_order_iso f).mono_right (f.monotone.le_map_supr2 _)
+
+@[simp] lemma independent_map_order_iso_iff {ι : Sort*} {α β : Type*}
+  [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} :
+  independent (f ∘ a) ↔ independent a :=
+⟨ λ h, have hf : f.symm ∘ f ∘ a = a := congr_arg (∘ a) f.left_inv.comp_eq_id,
+      hf ▸ h.map_order_iso f.symm,
+  λ h, h.map_order_iso f⟩
+
 /-- If the elements of a set are independent, then any element is disjoint from the `supr` of some
 subset of the rest. -/
 lemma independent.disjoint_bsupr {ι : Type*} {α : Type*} [complete_lattice α]

src/order/rel_iso.lean

@@ -795,6 +795,18 @@ begin
   simpa [← f.symm.le_iff_le] using f.symm.to_order_embedding.map_inf_le (f x) (f y)
 end
 
+/-- Note that this goal could also be stated `(disjoint on f) a b` -/
+lemma disjoint.map_order_iso [semilattice_inf_bot α] [semilattice_inf_bot β] {a b : α}
+  (f : α ≃o β) (ha : disjoint a b) : disjoint (f a) (f b) :=
+begin
+  rw [disjoint, ←f.map_inf, ←f.map_bot],
+  exact f.monotone ha,
+end
+
+@[simp] lemma disjoint_map_order_iso_iff [semilattice_inf_bot α] [semilattice_inf_bot β] {a b : α}
+  (f : α ≃o β) : disjoint (f a) (f b) ↔ disjoint a b :=
+⟨λ h, f.symm_apply_apply a ▸ f.symm_apply_apply b ▸ h.map_order_iso f.symm, λ h, h.map_order_iso f⟩
+
 lemma order_embedding.le_map_sup [semilattice_sup α] [semilattice_sup β]
   (f : α ↪o β) (x y : α) :
   f x ⊔ f y ≤ f (x ⊔ y) :=