Span.lean

/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Frédéric Dupuis,
  Heather Macbeth
-/
import Mathlib.Algebra.Module.Prod
import Mathlib.Algebra.Module.Submodule.EqLocus
import Mathlib.Algebra.Module.Submodule.Equiv
import Mathlib.Algebra.Module.Submodule.RestrictScalars
import Mathlib.Algebra.Ring.Idempotents
import Mathlib.Data.Set.Pointwise.SMul
import Mathlib.Order.CompactlyGenerated.Basic
import Mathlib.Order.OmegaCompletePartialOrder

#align_import linear_algebra.span from "leanprover-community/mathlib"@"10878f6bf1dab863445907ab23fbfcefcb5845d0"

/-!
# The span of a set of vectors, as a submodule

* `Submodule.span s` is defined to be the smallest submodule containing the set `s`.

## Notations

* We introduce the notation `R ∙ v` for the span of a singleton, `Submodule.span R {v}`.  This is
  `\span`, not the same as the scalar multiplication `•`/`\bub`.

-/

variable {R R₂ K M M₂ V S : Type*}

namespace Submodule

open Function Set

open Pointwise

section AddCommMonoid

variable [Semiring R] [AddCommMonoid M] [Module R M]
variable {x : M} (p p' : Submodule R M)
variable [Semiring R₂] {σ₁₂ : R →+* R₂}
variable [AddCommMonoid M₂] [Module R₂ M₂]
variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂]

section

variable (R)

/-- The span of a set `s ⊆ M` is the smallest submodule of M that contains `s`. -/
def span (s : Set M) : Submodule R M :=
  sInf { p | s ⊆ p }
#align submodule.span Submodule.span

variable {R}

-- Porting note: renamed field to `principal'` and added `principal` to fix explicit argument
/-- An `R`-submodule of `M` is principal if it is generated by one element. -/
@[mk_iff]
class IsPrincipal (S : Submodule R M) : Prop where
  principal' : ∃ a, S = span R {a}
#align submodule.is_principal Submodule.IsPrincipal

theorem IsPrincipal.principal (S : Submodule R M) [S.IsPrincipal] :
    ∃ a, S = span R {a} :=
  Submodule.IsPrincipal.principal'
#align submodule.is_principal.principal Submodule.IsPrincipal.principal

end

variable {s t : Set M}

theorem mem_span : x ∈ span R s ↔ ∀ p : Submodule R M, s ⊆ p → x ∈ p :=
  mem_iInter₂
#align submodule.mem_span Submodule.mem_span

@[aesop safe 20 apply (rule_sets := [SetLike])]
theorem subset_span : s ⊆ span R s := fun _ h => mem_span.2 fun _ hp => hp h
#align submodule.subset_span Submodule.subset_span

theorem span_le {p} : span R s ≤ p ↔ s ⊆ p :=
  ⟨Subset.trans subset_span, fun ss _ h => mem_span.1 h _ ss⟩
#align submodule.span_le Submodule.span_le

theorem span_mono (h : s ⊆ t) : span R s ≤ span R t :=
  span_le.2 <| Subset.trans h subset_span
#align submodule.span_mono Submodule.span_mono

theorem span_monotone : Monotone (span R : Set M → Submodule R M) := fun _ _ => span_mono
#align submodule.span_monotone Submodule.span_monotone

theorem span_eq_of_le (h₁ : s ⊆ p) (h₂ : p ≤ span R s) : span R s = p :=
  le_antisymm (span_le.2 h₁) h₂
#align submodule.span_eq_of_le Submodule.span_eq_of_le

theorem span_eq : span R (p : Set M) = p :=
  span_eq_of_le _ (Subset.refl _) subset_span
#align submodule.span_eq Submodule.span_eq

theorem span_eq_span (hs : s ⊆ span R t) (ht : t ⊆ span R s) : span R s = span R t :=
  le_antisymm (span_le.2 hs) (span_le.2 ht)
#align submodule.span_eq_span Submodule.span_eq_span

/-- A version of `Submodule.span_eq` for subobjects closed under addition and scalar multiplication
and containing zero. In general, this should not be used directly, but can be used to quickly
generate proofs for specific types of subobjects. -/
lemma coe_span_eq_self [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :
    (span R (s : Set M) : Set M) = s := by
  refine le_antisymm ?_ subset_span
  let s' : Submodule R M :=
    { carrier := s
      add_mem' := add_mem
      zero_mem' := zero_mem _
      smul_mem' := SMulMemClass.smul_mem }
  exact span_le (p := s') |>.mpr le_rfl

/-- A version of `Submodule.span_eq` for when the span is by a smaller ring. -/
@[simp]
theorem span_coe_eq_restrictScalars [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
    span S (p : Set M) = p.restrictScalars S :=
  span_eq (p.restrictScalars S)
#align submodule.span_coe_eq_restrict_scalars Submodule.span_coe_eq_restrictScalars

/-- A version of `Submodule.map_span_le` that does not require the `RingHomSurjective`
assumption. -/
theorem image_span_subset (f : F) (s : Set M) (N : Submodule R₂ M₂) :
    f '' span R s ⊆ N ↔ ∀ m ∈ s, f m ∈ N := image_subset_iff.trans <| span_le (p := N.comap f)

theorem image_span_subset_span (f : F) (s : Set M) : f '' span R s ⊆ span R₂ (f '' s) :=
  (image_span_subset f s _).2 fun x hx ↦ subset_span ⟨x, hx, rfl⟩

theorem map_span [RingHomSurjective σ₁₂] (f : F) (s : Set M) :
    (span R s).map f = span R₂ (f '' s) :=
  Eq.symm <| span_eq_of_le _ (Set.image_subset f subset_span) (image_span_subset_span f s)
#align submodule.map_span Submodule.map_span

alias _root_.LinearMap.map_span := Submodule.map_span
#align linear_map.map_span LinearMap.map_span

theorem map_span_le [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) :
    map f (span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N := image_span_subset f s N
#align submodule.map_span_le Submodule.map_span_le

alias _root_.LinearMap.map_span_le := Submodule.map_span_le
#align linear_map.map_span_le LinearMap.map_span_le

@[simp]
theorem span_insert_zero : span R (insert (0 : M) s) = span R s := by
  refine le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))
  rw [span_le, Set.insert_subset_iff]
  exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩
#align submodule.span_insert_zero Submodule.span_insert_zero

-- See also `span_preimage_eq` below.
theorem span_preimage_le (f : F) (s : Set M₂) :
    span R (f ⁻¹' s) ≤ (span R₂ s).comap f := by
  rw [span_le, comap_coe]
  exact preimage_mono subset_span
#align submodule.span_preimage_le Submodule.span_preimage_le

alias _root_.LinearMap.span_preimage_le := Submodule.span_preimage_le
#align linear_map.span_preimage_le LinearMap.span_preimage_le

theorem closure_subset_span {s : Set M} : (AddSubmonoid.closure s : Set M) ⊆ span R s :=
  (@AddSubmonoid.closure_le _ _ _ (span R s).toAddSubmonoid).mpr subset_span
#align submodule.closure_subset_span Submodule.closure_subset_span

theorem closure_le_toAddSubmonoid_span {s : Set M} :
    AddSubmonoid.closure s ≤ (span R s).toAddSubmonoid :=
  closure_subset_span
#align submodule.closure_le_to_add_submonoid_span Submodule.closure_le_toAddSubmonoid_span

@[simp]
theorem span_closure {s : Set M} : span R (AddSubmonoid.closure s : Set M) = span R s :=
  le_antisymm (span_le.mpr closure_subset_span) (span_mono AddSubmonoid.subset_closure)
#align submodule.span_closure Submodule.span_closure

/-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
preserved under addition and scalar multiplication, then `p` holds for all elements of the span of
`s`. -/
@[elab_as_elim]
theorem span_induction {p : M → Prop} (h : x ∈ span R s) (mem : ∀ x ∈ s, p x) (zero : p 0)
    (add : ∀ x y, p x → p y → p (x + y)) (smul : ∀ (a : R) (x), p x → p (a • x)) : p x :=
  ((@span_le (p := ⟨⟨⟨p, by intros x y; exact add x y⟩, zero⟩, smul⟩)) s).2 mem h
#align submodule.span_induction Submodule.span_induction

/-- An induction principle for span membership. This is a version of `Submodule.span_induction`
for binary predicates. -/
theorem span_induction₂ {p : M → M → Prop} {a b : M} (ha : a ∈ Submodule.span R s)
    (hb : b ∈ Submodule.span R s) (mem_mem : ∀ x ∈ s, ∀ y ∈ s, p x y)
    (zero_left : ∀ y, p 0 y) (zero_right : ∀ x, p x 0)
    (add_left : ∀ x₁ x₂ y, p x₁ y → p x₂ y → p (x₁ + x₂) y)
    (add_right : ∀ x y₁ y₂, p x y₁ → p x y₂ → p x (y₁ + y₂))
    (smul_left : ∀ (r : R) x y, p x y → p (r • x) y)
    (smul_right : ∀ (r : R) x y, p x y → p x (r • y)) : p a b :=
  Submodule.span_induction ha
    (fun x hx => Submodule.span_induction hb (mem_mem x hx) (zero_right x) (add_right x) fun r =>
      smul_right r x)
    (zero_left b) (fun x₁ x₂ => add_left x₁ x₂ b) fun r x => smul_left r x b

/-- A dependent version of `Submodule.span_induction`. -/
@[elab_as_elim]
theorem span_induction' {p : ∀ x, x ∈ span R s → Prop}
    (mem : ∀ (x) (h : x ∈ s), p x (subset_span h))
    (zero : p 0 (Submodule.zero_mem _))
    (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›))
    (smul : ∀ (a : R) (x hx), p x hx → p (a • x) (Submodule.smul_mem _ _ ‹_›)) {x}
    (hx : x ∈ span R s) : p x hx := by
  refine Exists.elim ?_ fun (hx : x ∈ span R s) (hc : p x hx) => hc
  refine
    span_induction hx (fun m hm => ⟨subset_span hm, mem m hm⟩) ⟨zero_mem _, zero⟩
      (fun x y hx hy =>
        Exists.elim hx fun hx' hx =>
          Exists.elim hy fun hy' hy => ⟨add_mem hx' hy', add _ _ _ _ hx hy⟩)
      fun r x hx => Exists.elim hx fun hx' hx => ⟨smul_mem _ _ hx', smul r _ _ hx⟩
#align submodule.span_induction' Submodule.span_induction'

open AddSubmonoid in
theorem span_eq_closure {s : Set M} : (span R s).toAddSubmonoid = closure (@univ R • s) := by
  refine le_antisymm
    (fun x hx ↦ span_induction hx (fun x hx ↦ subset_closure ⟨1, trivial, x, hx, one_smul R x⟩)
      (zero_mem _) (fun _ _ ↦ add_mem) fun r m hm ↦ closure_induction hm ?_ ?_ fun _ _ h h' ↦ ?_)
    (closure_le.2 ?_)
  · rintro _ ⟨r, -, m, hm, rfl⟩; exact smul_mem _ _ (subset_span hm)
  · rintro _ ⟨r', -, m, hm, rfl⟩; exact subset_closure ⟨r * r', trivial, m, hm, mul_smul r r' m⟩
  · rw [smul_zero]; apply zero_mem
  · rw [smul_add]; exact add_mem h h'

/-- A variant of `span_induction` that combines `∀ x ∈ s, p x` and `∀ r x, p x → p (r • x)`
into a single condition `∀ r, ∀ x ∈ s, p (r • x)`, which can be easier to verify. -/
@[elab_as_elim]
theorem closure_induction {p : M → Prop} (h : x ∈ span R s) (zero : p 0)
    (add : ∀ x y, p x → p y → p (x + y)) (smul_mem : ∀ r : R, ∀ x ∈ s, p (r • x)) : p x := by
  rw [← mem_toAddSubmonoid, span_eq_closure] at h
  refine AddSubmonoid.closure_induction h ?_ zero add
  rintro _ ⟨r, -, m, hm, rfl⟩
  exact smul_mem r m hm

/-- A dependent version of `Submodule.closure_induction`. -/
@[elab_as_elim]
theorem closure_induction' {p : ∀ x, x ∈ span R s → Prop}
    (zero : p 0 (Submodule.zero_mem _))
    (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›))
    (smul_mem : ∀ (r x) (h : x ∈ s), p (r • x) (Submodule.smul_mem _ _ <| subset_span h)) {x}
    (hx : x ∈ span R s) : p x hx := by
  refine Exists.elim ?_ fun (hx : x ∈ span R s) (hc : p x hx) ↦ hc
  refine closure_induction hx ⟨zero_mem _, zero⟩
    (fun x y hx hy ↦ Exists.elim hx fun hx' hx ↦
      Exists.elim hy fun hy' hy ↦ ⟨add_mem hx' hy', add _ _ _ _ hx hy⟩)
    fun r x hx ↦ ⟨Submodule.smul_mem _ _ (subset_span hx), smul_mem r x hx⟩

@[simp]
theorem span_span_coe_preimage : span R (((↑) : span R s → M) ⁻¹' s) = ⊤ :=
  eq_top_iff.2 fun x ↦ Subtype.recOn x fun x hx _ ↦ by
    refine span_induction' (p := fun x hx ↦ (⟨x, hx⟩ : span R s) ∈ span R (Subtype.val ⁻¹' s))
      (fun x' hx' ↦ subset_span hx') ?_ (fun x _ y _ ↦ ?_) (fun r x _ ↦ ?_) hx
    · exact zero_mem _
    · exact add_mem
    · exact smul_mem _ _
#align submodule.span_span_coe_preimage Submodule.span_span_coe_preimage

@[simp]
lemma span_setOf_mem_eq_top :
    span R {x : span R s | (x : M) ∈ s} = ⊤ :=
  span_span_coe_preimage

theorem span_nat_eq_addSubmonoid_closure (s : Set M) :
    (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s := by
  refine Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)
  apply (OrderIso.to_galoisConnection (AddSubmonoid.toNatSubmodule (M := M)).symm).l_le
     (a := span ℕ s) (b := AddSubmonoid.closure s)
  rw [span_le]
  exact AddSubmonoid.subset_closure
#align submodule.span_nat_eq_add_submonoid_closure Submodule.span_nat_eq_addSubmonoid_closure

@[simp]
theorem span_nat_eq (s : AddSubmonoid M) : (span ℕ (s : Set M)).toAddSubmonoid = s := by
  rw [span_nat_eq_addSubmonoid_closure, s.closure_eq]
#align submodule.span_nat_eq Submodule.span_nat_eq

theorem span_int_eq_addSubgroup_closure {M : Type*} [AddCommGroup M] (s : Set M) :
    (span ℤ s).toAddSubgroup = AddSubgroup.closure s :=
  Eq.symm <|
    AddSubgroup.closure_eq_of_le _ subset_span fun x hx =>
      span_induction hx (fun x hx => AddSubgroup.subset_closure hx) (AddSubgroup.zero_mem _)
        (fun _ _ => AddSubgroup.add_mem _) fun _ _ _ => AddSubgroup.zsmul_mem _ ‹_› _
#align submodule.span_int_eq_add_subgroup_closure Submodule.span_int_eq_addSubgroup_closure

@[simp]
theorem span_int_eq {M : Type*} [AddCommGroup M] (s : AddSubgroup M) :
    (span ℤ (s : Set M)).toAddSubgroup = s := by rw [span_int_eq_addSubgroup_closure, s.closure_eq]
#align submodule.span_int_eq Submodule.span_int_eq

section

variable (R M)

/-- `span` forms a Galois insertion with the coercion from submodule to set. -/
protected def gi : GaloisInsertion (@span R M _ _ _) (↑) where
  choice s _ := span R s
  gc _ _ := span_le
  le_l_u _ := subset_span
  choice_eq _ _ := rfl
#align submodule.gi Submodule.gi

end

@[simp]
theorem span_empty : span R (∅ : Set M) = ⊥ :=
  (Submodule.gi R M).gc.l_bot
#align submodule.span_empty Submodule.span_empty

@[simp]
theorem span_univ : span R (univ : Set M) = ⊤ :=
  eq_top_iff.2 <| SetLike.le_def.2 <| subset_span
#align submodule.span_univ Submodule.span_univ

theorem span_union (s t : Set M) : span R (s ∪ t) = span R s ⊔ span R t :=
  (Submodule.gi R M).gc.l_sup
#align submodule.span_union Submodule.span_union

theorem span_iUnion {ι} (s : ι → Set M) : span R (⋃ i, s i) = ⨆ i, span R (s i) :=
  (Submodule.gi R M).gc.l_iSup
#align submodule.span_Union Submodule.span_iUnion

/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
theorem span_iUnion₂ {ι} {κ : ι → Sort*} (s : ∀ i, κ i → Set M) :
    span R (⋃ (i) (j), s i j) = ⨆ (i) (j), span R (s i j) :=
  (Submodule.gi R M).gc.l_iSup₂
#align submodule.span_Union₂ Submodule.span_iUnion₂

theorem span_attach_biUnion [DecidableEq M] {α : Type*} (s : Finset α) (f : s → Finset M) :
    span R (s.attach.biUnion f : Set M) = ⨆ x, span R (f x) := by simp [span_iUnion]
#align submodule.span_attach_bUnion Submodule.span_attach_biUnion

theorem sup_span : p ⊔ span R s = span R (p ∪ s) := by rw [Submodule.span_union, p.span_eq]
#align submodule.sup_span Submodule.sup_span

theorem span_sup : span R s ⊔ p = span R (s ∪ p) := by rw [Submodule.span_union, p.span_eq]
#align submodule.span_sup Submodule.span_sup

notation:1000
  /- Note that the character `∙` U+2219 used below is different from the scalar multiplication
character `•` U+2022. -/
R " ∙ " x => span R (singleton x)

theorem span_eq_iSup_of_singleton_spans (s : Set M) : span R s = ⨆ x ∈ s, R ∙ x := by
  simp only [← span_iUnion, Set.biUnion_of_singleton s]
#align submodule.span_eq_supr_of_singleton_spans Submodule.span_eq_iSup_of_singleton_spans

theorem span_range_eq_iSup {ι : Sort*} {v : ι → M} : span R (range v) = ⨆ i, R ∙ v i := by
  rw [span_eq_iSup_of_singleton_spans, iSup_range]
#align submodule.span_range_eq_supr Submodule.span_range_eq_iSup

theorem span_smul_le (s : Set M) (r : R) : span R (r • s) ≤ span R s := by
  rw [span_le]
  rintro _ ⟨x, hx, rfl⟩
  exact smul_mem (span R s) r (subset_span hx)
#align submodule.span_smul_le Submodule.span_smul_le

theorem subset_span_trans {U V W : Set M} (hUV : U ⊆ Submodule.span R V)
    (hVW : V ⊆ Submodule.span R W) : U ⊆ Submodule.span R W :=
  (Submodule.gi R M).gc.le_u_l_trans hUV hVW
#align submodule.subset_span_trans Submodule.subset_span_trans

/-- See `Submodule.span_smul_eq` (in `RingTheory.Ideal.Operations`) for
`span R (r • s) = r • span R s` that holds for arbitrary `r` in a `CommSemiring`. -/
theorem span_smul_eq_of_isUnit (s : Set M) (r : R) (hr : IsUnit r) : span R (r • s) = span R s := by
  apply le_antisymm
  · apply span_smul_le
  · convert span_smul_le (r • s) ((hr.unit⁻¹ : _) : R)
    rw [smul_smul]
    erw [hr.unit.inv_val]
    rw [one_smul]
#align submodule.span_smul_eq_of_is_unit Submodule.span_smul_eq_of_isUnit

@[simp]
theorem coe_iSup_of_directed {ι} [Nonempty ι] (S : ι → Submodule R M)
    (H : Directed (· ≤ ·) S) : ((iSup S: Submodule R M) : Set M) = ⋃ i, S i :=
  let s : Submodule R M :=
    { __ := AddSubmonoid.copy _ _ (AddSubmonoid.coe_iSup_of_directed H).symm
      smul_mem' := fun r _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
        Set.mem_iUnion.mpr ⟨i, (S i).smul_mem' r hi⟩ }
  have : iSup S = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set M)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
  this.symm ▸ rfl
#align submodule.coe_supr_of_directed Submodule.coe_iSup_of_directed

@[simp]
theorem mem_iSup_of_directed {ι} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (· ≤ ·) S) {x} :
    x ∈ iSup S ↔ ∃ i, x ∈ S i := by
  rw [← SetLike.mem_coe, coe_iSup_of_directed S H, mem_iUnion]
  rfl
#align submodule.mem_supr_of_directed Submodule.mem_iSup_of_directed

theorem mem_sSup_of_directed {s : Set (Submodule R M)} {z} (hs : s.Nonempty)
    (hdir : DirectedOn (· ≤ ·) s) : z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y := by
  have : Nonempty s := hs.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists, Subtype.coe_mk,
    exists_prop]
#align submodule.mem_Sup_of_directed Submodule.mem_sSup_of_directed

@[norm_cast, simp]
theorem coe_iSup_of_chain (a : ℕ →o Submodule R M) : (↑(⨆ k, a k) : Set M) = ⋃ k, (a k : Set M) :=
  coe_iSup_of_directed a a.monotone.directed_le
#align submodule.coe_supr_of_chain Submodule.coe_iSup_of_chain

/-- We can regard `coe_iSup_of_chain` as the statement that `(↑) : (Submodule R M) → Set M` is
Scott continuous for the ω-complete partial order induced by the complete lattice structures. -/
theorem coe_scott_continuous :
    OmegaCompletePartialOrder.Continuous' ((↑) : Submodule R M → Set M) :=
  ⟨SetLike.coe_mono, coe_iSup_of_chain⟩
#align submodule.coe_scott_continuous Submodule.coe_scott_continuous

@[simp]
theorem mem_iSup_of_chain (a : ℕ →o Submodule R M) (m : M) : (m ∈ ⨆ k, a k) ↔ ∃ k, m ∈ a k :=
  mem_iSup_of_directed a a.monotone.directed_le
#align submodule.mem_supr_of_chain Submodule.mem_iSup_of_chain

section

variable {p p'}

theorem mem_sup : x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x :=
  ⟨fun h => by
    rw [← span_eq p, ← span_eq p', ← span_union] at h
    refine span_induction h ?_ ?_ ?_ ?_
    · rintro y (h | h)
      · exact ⟨y, h, 0, by simp, by simp⟩
      · exact ⟨0, by simp, y, h, by simp⟩
    · exact ⟨0, by simp, 0, by simp⟩
    · rintro _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, add_mem hy₁ hy₂, _, add_mem hz₁ hz₂, by
        rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]⟩
    · rintro a _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, smul_mem _ a hy, _, smul_mem _ a hz, by simp [smul_add]⟩, by
    rintro ⟨y, hy, z, hz, rfl⟩
    exact add_mem ((le_sup_left : p ≤ p ⊔ p') hy) ((le_sup_right : p' ≤ p ⊔ p') hz)⟩
#align submodule.mem_sup Submodule.mem_sup

theorem mem_sup' : x ∈ p ⊔ p' ↔ ∃ (y : p) (z : p'), (y : M) + z = x :=
  mem_sup.trans <| by simp only [Subtype.exists, exists_prop]
#align submodule.mem_sup' Submodule.mem_sup'

lemma exists_add_eq_of_codisjoint (h : Codisjoint p p') (x : M) :
    ∃ y ∈ p, ∃ z ∈ p', y + z = x := by
  suffices x ∈ p ⊔ p' by exact Submodule.mem_sup.mp this
  simpa only [h.eq_top] using Submodule.mem_top

variable (p p')

theorem coe_sup : ↑(p ⊔ p') = (p + p' : Set M) := by
  ext
  rw [SetLike.mem_coe, mem_sup, Set.mem_add]
  simp
#align submodule.coe_sup Submodule.coe_sup

theorem sup_toAddSubmonoid : (p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid := by
  ext x
  rw [mem_toAddSubmonoid, mem_sup, AddSubmonoid.mem_sup]
  rfl
#align submodule.sup_to_add_submonoid Submodule.sup_toAddSubmonoid

theorem sup_toAddSubgroup {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    (p p' : Submodule R M) : (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup := by
  ext x
  rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]
  rfl
#align submodule.sup_to_add_subgroup Submodule.sup_toAddSubgroup

end

theorem mem_span_singleton_self (x : M) : x ∈ R ∙ x :=
  subset_span rfl
#align submodule.mem_span_singleton_self Submodule.mem_span_singleton_self

theorem nontrivial_span_singleton {x : M} (h : x ≠ 0) : Nontrivial (R ∙ x) :=
  ⟨by
    use 0, ⟨x, Submodule.mem_span_singleton_self x⟩
    intro H
    rw [eq_comm, Submodule.mk_eq_zero] at H
    exact h H⟩
#align submodule.nontrivial_span_singleton Submodule.nontrivial_span_singleton

theorem mem_span_singleton {y : M} : (x ∈ R ∙ y) ↔ ∃ a : R, a • y = x :=
  ⟨fun h => by
    refine span_induction h ?_ ?_ ?_ ?_
    · rintro y (rfl | ⟨⟨_⟩⟩)
      exact ⟨1, by simp⟩
    · exact ⟨0, by simp⟩
    · rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩
      exact ⟨a + b, by simp [add_smul]⟩
    · rintro a _ ⟨b, rfl⟩
      exact ⟨a * b, by simp [smul_smul]⟩, by
    rintro ⟨a, y, rfl⟩; exact smul_mem _ _ (subset_span <| by simp)⟩
#align submodule.mem_span_singleton Submodule.mem_span_singleton

theorem le_span_singleton_iff {s : Submodule R M} {v₀ : M} :
    (s ≤ R ∙ v₀) ↔ ∀ v ∈ s, ∃ r : R, r • v₀ = v := by simp_rw [SetLike.le_def, mem_span_singleton]
#align submodule.le_span_singleton_iff Submodule.le_span_singleton_iff

variable (R)

theorem span_singleton_eq_top_iff (x : M) : (R ∙ x) = ⊤ ↔ ∀ v, ∃ r : R, r • x = v := by
  rw [eq_top_iff, le_span_singleton_iff]
  tauto
#align submodule.span_singleton_eq_top_iff Submodule.span_singleton_eq_top_iff

@[simp]
theorem span_zero_singleton : (R ∙ (0 : M)) = ⊥ := by
  ext
  simp [mem_span_singleton, eq_comm]
#align submodule.span_zero_singleton Submodule.span_zero_singleton

theorem span_singleton_eq_range (y : M) : ↑(R ∙ y) = range ((· • y) : R → M) :=
  Set.ext fun _ => mem_span_singleton
#align submodule.span_singleton_eq_range Submodule.span_singleton_eq_range

theorem span_singleton_smul_le {S} [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M]
    (r : S) (x : M) : (R ∙ r • x) ≤ R ∙ x := by
  rw [span_le, Set.singleton_subset_iff, SetLike.mem_coe]
  exact smul_of_tower_mem _ _ (mem_span_singleton_self _)
#align submodule.span_singleton_smul_le Submodule.span_singleton_smul_le

theorem span_singleton_group_smul_eq {G} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M]
    (g : G) (x : M) : (R ∙ g • x) = R ∙ x := by
  refine le_antisymm (span_singleton_smul_le R g x) ?_
  convert span_singleton_smul_le R g⁻¹ (g • x)
  exact (inv_smul_smul g x).symm
#align submodule.span_singleton_group_smul_eq Submodule.span_singleton_group_smul_eq

variable {R}

theorem span_singleton_smul_eq {r : R} (hr : IsUnit r) (x : M) : (R ∙ r • x) = R ∙ x := by
  lift r to Rˣ using hr
  rw [← Units.smul_def]
  exact span_singleton_group_smul_eq R r x
#align submodule.span_singleton_smul_eq Submodule.span_singleton_smul_eq

theorem disjoint_span_singleton {K E : Type*} [DivisionRing K] [AddCommGroup E] [Module K E]
    {s : Submodule K E} {x : E} : Disjoint s (K ∙ x) ↔ x ∈ s → x = 0 := by
  refine disjoint_def.trans ⟨fun H hx => H x hx <| subset_span <| mem_singleton x, ?_⟩
  intro H y hy hyx
  obtain ⟨c, rfl⟩ := mem_span_singleton.1 hyx
  by_cases hc : c = 0
  · rw [hc, zero_smul]
  · rw [s.smul_mem_iff hc] at hy
    rw [H hy, smul_zero]
#align submodule.disjoint_span_singleton Submodule.disjoint_span_singleton

theorem disjoint_span_singleton' {K E : Type*} [DivisionRing K] [AddCommGroup E] [Module K E]
    {p : Submodule K E} {x : E} (x0 : x ≠ 0) : Disjoint p (K ∙ x) ↔ x ∉ p :=
  disjoint_span_singleton.trans ⟨fun h₁ h₂ => x0 (h₁ h₂), fun h₁ h₂ => (h₁ h₂).elim⟩
#align submodule.disjoint_span_singleton' Submodule.disjoint_span_singleton'

theorem mem_span_singleton_trans {x y z : M} (hxy : x ∈ R ∙ y) (hyz : y ∈ R ∙ z) : x ∈ R ∙ z := by
  rw [← SetLike.mem_coe, ← singleton_subset_iff] at *
  exact Submodule.subset_span_trans hxy hyz
#align submodule.mem_span_singleton_trans Submodule.mem_span_singleton_trans

theorem span_insert (x) (s : Set M) : span R (insert x s) = (R ∙ x) ⊔ span R s := by
  rw [insert_eq, span_union]
#align submodule.span_insert Submodule.span_insert

theorem span_insert_eq_span (h : x ∈ span R s) : span R (insert x s) = span R s :=
  span_eq_of_le _ (Set.insert_subset_iff.mpr ⟨h, subset_span⟩) (span_mono <| subset_insert _ _)
#align submodule.span_insert_eq_span Submodule.span_insert_eq_span

theorem span_span : span R (span R s : Set M) = span R s :=
  span_eq _
#align submodule.span_span Submodule.span_span

theorem mem_span_insert {y} :
    x ∈ span R (insert y s) ↔ ∃ a : R, ∃ z ∈ span R s, x = a • y + z := by
  simp [span_insert, mem_sup, mem_span_singleton, eq_comm (a := x)]
#align submodule.mem_span_insert Submodule.mem_span_insert

theorem mem_span_pair {x y z : M} :
    z ∈ span R ({x, y} : Set M) ↔ ∃ a b : R, a • x + b • y = z := by
  simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]
#align submodule.mem_span_pair Submodule.mem_span_pair

variable (R S s)

/-- If `R` is "smaller" ring than `S` then the span by `R` is smaller than the span by `S`. -/
theorem span_le_restrictScalars [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] :
    span R s ≤ (span S s).restrictScalars R :=
  Submodule.span_le.2 Submodule.subset_span
#align submodule.span_le_restrict_scalars Submodule.span_le_restrictScalars

/-- A version of `Submodule.span_le_restrictScalars` with coercions. -/
@[simp]
theorem span_subset_span [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] :
    ↑(span R s) ⊆ (span S s : Set M) :=
  span_le_restrictScalars R S s
#align submodule.span_subset_span Submodule.span_subset_span

/-- Taking the span by a large ring of the span by the small ring is the same as taking the span
by just the large ring. -/
theorem span_span_of_tower [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] :
    span S (span R s : Set M) = span S s :=
  le_antisymm (span_le.2 <| span_subset_span R S s) (span_mono subset_span)
#align submodule.span_span_of_tower Submodule.span_span_of_tower

variable {R S s}

theorem span_eq_bot : span R (s : Set M) = ⊥ ↔ ∀ x ∈ s, (x : M) = 0 :=
  eq_bot_iff.trans
    ⟨fun H _ h => (mem_bot R).1 <| H <| subset_span h, fun H =>
      span_le.2 fun x h => (mem_bot R).2 <| H x h⟩
#align submodule.span_eq_bot Submodule.span_eq_bot

@[simp]
theorem span_singleton_eq_bot : (R ∙ x) = ⊥ ↔ x = 0 :=
  span_eq_bot.trans <| by simp
#align submodule.span_singleton_eq_bot Submodule.span_singleton_eq_bot

@[simp]
theorem span_zero : span R (0 : Set M) = ⊥ := by rw [← singleton_zero, span_singleton_eq_bot]
#align submodule.span_zero Submodule.span_zero

@[simp]
theorem span_singleton_le_iff_mem (m : M) (p : Submodule R M) : (R ∙ m) ≤ p ↔ m ∈ p := by
  rw [span_le, singleton_subset_iff, SetLike.mem_coe]
#align submodule.span_singleton_le_iff_mem Submodule.span_singleton_le_iff_mem

theorem span_singleton_eq_span_singleton {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] {x y : M} : ((R ∙ x) = R ∙ y) ↔ ∃ z : Rˣ, z • x = y := by
  constructor
  · simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]
    rintro ⟨⟨a, rfl⟩, b, hb⟩
    rcases eq_or_ne y 0 with rfl | hy; · simp
    refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
    · apply smul_left_injective R hy
      simpa only [mul_smul, one_smul]
    · rw [← hb] at hy
      apply smul_left_injective R (smul_ne_zero_iff.1 hy).2
      simp only [mul_smul, one_smul, hb]
  · rintro ⟨u, rfl⟩
    exact (span_singleton_group_smul_eq _ _ _).symm
#align submodule.span_singleton_eq_span_singleton Submodule.span_singleton_eq_span_singleton

-- Should be `@[simp]` but doesn't fire due to `lean4#3701`.
theorem span_image [RingHomSurjective σ₁₂] (f : F) :
    span R₂ (f '' s) = map f (span R s) :=
  (map_span f s).symm
#align submodule.span_image Submodule.span_image

@[simp] -- Should be replaced with `Submodule.span_image` when `lean4#3701` is fixed.
theorem span_image' [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
    span R₂ (f '' s) = map f (span R s) :=
  span_image _

theorem apply_mem_span_image_of_mem_span [RingHomSurjective σ₁₂] (f : F) {x : M}
    {s : Set M} (h : x ∈ Submodule.span R s) : f x ∈ Submodule.span R₂ (f '' s) := by
  rw [Submodule.span_image]
  exact Submodule.mem_map_of_mem h
#align submodule.apply_mem_span_image_of_mem_span Submodule.apply_mem_span_image_of_mem_span

theorem apply_mem_span_image_iff_mem_span [RingHomSurjective σ₁₂] {f : F} {x : M}
    {s : Set M} (hf : Function.Injective f) :
    f x ∈ Submodule.span R₂ (f '' s) ↔ x ∈ Submodule.span R s := by
  rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]

@[simp]
theorem map_subtype_span_singleton {p : Submodule R M} (x : p) :
    map p.subtype (R ∙ x) = R ∙ (x : M) := by simp [← span_image]
#align submodule.map_subtype_span_singleton Submodule.map_subtype_span_singleton

/-- `f` is an explicit argument so we can `apply` this theorem and obtain `h` as a new goal. -/
theorem not_mem_span_of_apply_not_mem_span_image [RingHomSurjective σ₁₂] (f : F) {x : M}
    {s : Set M} (h : f x ∉ Submodule.span R₂ (f '' s)) : x ∉ Submodule.span R s :=
  h.imp (apply_mem_span_image_of_mem_span f)
#align submodule.not_mem_span_of_apply_not_mem_span_image Submodule.not_mem_span_of_apply_not_mem_span_image

theorem iSup_span {ι : Sort*} (p : ι → Set M) : ⨆ i, span R (p i) = span R (⋃ i, p i) :=
  le_antisymm (iSup_le fun i => span_mono <| subset_iUnion _ i) <|
    span_le.mpr <| iUnion_subset fun i _ hm => mem_iSup_of_mem i <| subset_span hm
#align submodule.supr_span Submodule.iSup_span

theorem iSup_eq_span {ι : Sort*} (p : ι → Submodule R M) : ⨆ i, p i = span R (⋃ i, ↑(p i)) := by
  simp_rw [← iSup_span, span_eq]
#align submodule.supr_eq_span Submodule.iSup_eq_span

theorem iSup_toAddSubmonoid {ι : Sort*} (p : ι → Submodule R M) :
    (⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid := by
  refine le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)
  simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]
  intro hx
  refine Submodule.span_induction hx (fun x hx => ?_) ?_ (fun x y hx hy => ?_) fun r x hx => ?_
  · exact AddSubmonoid.subset_closure hx
  · exact AddSubmonoid.zero_mem _
  · exact AddSubmonoid.add_mem _ hx hy
  · refine AddSubmonoid.closure_induction hx ?_ ?_ ?_
    · rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩
      apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
      exact smul_mem _ r hix
    · rw [smul_zero]
      exact AddSubmonoid.zero_mem _
    · intro x y hx hy
      rw [smul_add]
      exact AddSubmonoid.add_mem _ hx hy
#align submodule.supr_to_add_submonoid Submodule.iSup_toAddSubmonoid

/-- An induction principle for elements of `⨆ i, p i`.
If `C` holds for `0` and all elements of `p i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `p`. -/
@[elab_as_elim]
theorem iSup_induction {ι : Sort*} (p : ι → Submodule R M) {C : M → Prop} {x : M}
    (hx : x ∈ ⨆ i, p i) (hp : ∀ (i), ∀ x ∈ p i, C x) (h0 : C 0)
    (hadd : ∀ x y, C x → C y → C (x + y)) : C x := by
  rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx
  exact AddSubmonoid.iSup_induction (x := x) _ hx hp h0 hadd
#align submodule.supr_induction Submodule.iSup_induction

/-- A dependent version of `submodule.iSup_induction`. -/
@[elab_as_elim]
theorem iSup_induction' {ι : Sort*} (p : ι → Submodule R M) {C : ∀ x, (x ∈ ⨆ i, p i) → Prop}
    (mem : ∀ (i) (x) (hx : x ∈ p i), C x (mem_iSup_of_mem i hx)) (zero : C 0 (zero_mem _))
    (add : ∀ x y hx hy, C x hx → C y hy → C (x + y) (add_mem ‹_› ‹_›)) {x : M}
    (hx : x ∈ ⨆ i, p i) : C x hx := by
  refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : C x hx) => hc
  refine iSup_induction p (C := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), C x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_
  · exact ⟨_, mem _ _ hx⟩
  · exact ⟨_, zero⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, add _ _ _ _ Cx Cy⟩
#align submodule.supr_induction' Submodule.iSup_induction'

theorem singleton_span_isCompactElement (x : M) :
    CompleteLattice.IsCompactElement (span R {x} : Submodule R M) := by
  rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
  intro d hemp hdir hsup
  have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)
  obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_sSup_of_directed hemp hdir).mp this
  exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff] ⟩⟩
#align submodule.singleton_span_is_compact_element Submodule.singleton_span_isCompactElement

/-- The span of a finite subset is compact in the lattice of submodules. -/
theorem finset_span_isCompactElement (S : Finset M) :
    CompleteLattice.IsCompactElement (span R S : Submodule R M) := by
  rw [span_eq_iSup_of_singleton_spans]
  simp only [Finset.mem_coe]
  rw [← Finset.sup_eq_iSup]
  exact
    CompleteLattice.isCompactElement_finsetSup S fun x _ => singleton_span_isCompactElement x
#align submodule.finset_span_is_compact_element Submodule.finset_span_isCompactElement

/-- The span of a finite subset is compact in the lattice of submodules. -/
theorem finite_span_isCompactElement (S : Set M) (h : S.Finite) :
    CompleteLattice.IsCompactElement (span R S : Submodule R M) :=
  Finite.coe_toFinset h ▸ finset_span_isCompactElement h.toFinset
#align submodule.finite_span_is_compact_element Submodule.finite_span_isCompactElement

instance : IsCompactlyGenerated (Submodule R M) :=
  ⟨fun s =>
    ⟨(fun x => span R {x}) '' s,
      ⟨fun t ht => by
        rcases (Set.mem_image _ _ _).1 ht with ⟨x, _, rfl⟩
        apply singleton_span_isCompactElement, by
        rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, span_eq]⟩⟩⟩

/-- A submodule is equal to the supremum of the spans of the submodule's nonzero elements. -/
theorem submodule_eq_sSup_le_nonzero_spans (p : Submodule R M) :
    p = sSup { T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m} } := by
  let S := { T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m} }
  apply le_antisymm
  · intro m hm
    by_cases h : m = 0
    · rw [h]
      simp
    · exact @le_sSup _ _ S _ ⟨m, ⟨hm, ⟨h, rfl⟩⟩⟩ m (mem_span_singleton_self m)
  · rw [sSup_le_iff]
    rintro S ⟨_, ⟨_, ⟨_, rfl⟩⟩⟩
    rwa [span_singleton_le_iff_mem]
#align submodule.submodule_eq_Sup_le_nonzero_spans Submodule.submodule_eq_sSup_le_nonzero_spans

theorem lt_sup_iff_not_mem {I : Submodule R M} {a : M} : (I < I ⊔ R ∙ a) ↔ a ∉ I := by simp
#align submodule.lt_sup_iff_not_mem Submodule.lt_sup_iff_not_mem

theorem mem_iSup {ι : Sort*} (p : ι → Submodule R M) {m : M} :
    (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N := by
  rw [← span_singleton_le_iff_mem, le_iSup_iff]
  simp only [span_singleton_le_iff_mem]
#align submodule.mem_supr Submodule.mem_iSup

theorem mem_sSup {s : Set (Submodule R M)} {m : M} :
    (m ∈ sSup s) ↔ ∀ N, (∀ p ∈ s, p ≤ N) → m ∈ N := by
  simp_rw [sSup_eq_iSup, Submodule.mem_iSup, iSup_le_iff]

section

/-- For every element in the span of a set, there exists a finite subset of the set
such that the element is contained in the span of the subset. -/
theorem mem_span_finite_of_mem_span {S : Set M} {x : M} (hx : x ∈ span R S) :
    ∃ T : Finset M, ↑T ⊆ S ∧ x ∈ span R (T : Set M) := by
  classical
  refine span_induction hx (fun x hx => ?_) ?_ ?_ ?_
  · refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x
  · use ∅
    simp
  · rintro x y ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
    refine ⟨X ∪ Y, ?_, ?_⟩
    · rw [Finset.coe_union]
      exact Set.union_subset hX hY
    rw [Finset.coe_union, span_union, mem_sup]
    exact ⟨x, hxX, y, hyY, rfl⟩
  · rintro a x ⟨T, hT, h2⟩
    exact ⟨T, hT, smul_mem _ _ h2⟩
#align submodule.mem_span_finite_of_mem_span Submodule.mem_span_finite_of_mem_span

end

variable {M' : Type*} [AddCommMonoid M'] [Module R M'] (q₁ q₁' : Submodule R M')

/-- The product of two submodules is a submodule. -/
def prod : Submodule R (M × M') :=
  { p.toAddSubmonoid.prod q₁.toAddSubmonoid with
    carrier := p ×ˢ q₁
    smul_mem' := by rintro a ⟨x, y⟩ ⟨hx, hy⟩; exact ⟨smul_mem _ a hx, smul_mem _ a hy⟩ }
#align submodule.prod Submodule.prod

@[simp]
theorem prod_coe : (prod p q₁ : Set (M × M')) = (p : Set M) ×ˢ (q₁ : Set M') :=
  rfl
#align submodule.prod_coe Submodule.prod_coe

@[simp]
theorem mem_prod {p : Submodule R M} {q : Submodule R M'} {x : M × M'} :
    x ∈ prod p q ↔ x.1 ∈ p ∧ x.2 ∈ q :=
  Set.mem_prod
#align submodule.mem_prod Submodule.mem_prod

theorem span_prod_le (s : Set M) (t : Set M') : span R (s ×ˢ t) ≤ prod (span R s) (span R t) :=
  span_le.2 <| Set.prod_mono subset_span subset_span
#align submodule.span_prod_le Submodule.span_prod_le

@[simp]
theorem prod_top : (prod ⊤ ⊤ : Submodule R (M × M')) = ⊤ := by ext; simp
#align submodule.prod_top Submodule.prod_top

@[simp]
theorem prod_bot : (prod ⊥ ⊥ : Submodule R (M × M')) = ⊥ := by ext ⟨x, y⟩; simp [Prod.zero_eq_mk]
#align submodule.prod_bot Submodule.prod_bot

theorem prod_mono {p p' : Submodule R M} {q q' : Submodule R M'} :
    p ≤ p' → q ≤ q' → prod p q ≤ prod p' q' :=
  Set.prod_mono
#align submodule.prod_mono Submodule.prod_mono

@[simp]
theorem prod_inf_prod : prod p q₁ ⊓ prod p' q₁' = prod (p ⊓ p') (q₁ ⊓ q₁') :=
  SetLike.coe_injective Set.prod_inter_prod
#align submodule.prod_inf_prod Submodule.prod_inf_prod

@[simp]
theorem prod_sup_prod : prod p q₁ ⊔ prod p' q₁' = prod (p ⊔ p') (q₁ ⊔ q₁') := by
  refine le_antisymm
    (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_
  simp [SetLike.le_def]; intro xx yy hxx hyy
  rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩
  rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩
  exact mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩
#align submodule.prod_sup_prod Submodule.prod_sup_prod

end AddCommMonoid

section AddCommGroup

variable [Ring R] [AddCommGroup M] [Module R M]

@[simp]
theorem span_neg (s : Set M) : span R (-s) = span R s :=
  calc
    span R (-s) = span R ((-LinearMap.id : M →ₗ[R] M) '' s) := by simp
    _ = map (-LinearMap.id) (span R s) := (map_span (-LinearMap.id) _).symm
    _ = span R s := by simp
#align submodule.span_neg Submodule.span_neg

theorem mem_span_insert' {x y} {s : Set M} :
    x ∈ span R (insert y s) ↔ ∃ a : R, x + a • y ∈ span R s := by
  rw [mem_span_insert]; constructor
  · rintro ⟨a, z, hz, rfl⟩
    exact ⟨-a, by simp [hz, add_assoc]⟩
  · rintro ⟨a, h⟩
    exact ⟨-a, _, h, by simp [add_comm, add_left_comm]⟩
#align submodule.mem_span_insert' Submodule.mem_span_insert'

instance : IsModularLattice (Submodule R M) :=
  ⟨fun y z xz a ha => by
    rw [mem_inf, mem_sup] at ha
    rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩
    rw [mem_sup]
    refine ⟨b, hb, c, mem_inf.2 ⟨hc, ?_⟩, rfl⟩
    rw [← add_sub_cancel_right c b, add_comm]
    apply z.sub_mem haz (xz hb)⟩

lemma isCompl_comap_subtype_of_isCompl_of_le {p q r : Submodule R M}
    (h₁ : IsCompl q r) (h₂ : q ≤ p) :
    IsCompl (q.comap p.subtype) (r.comap p.subtype) := by
  simpa [p.mapIic.isCompl_iff, Iic.isCompl_iff] using Iic.isCompl_inf_inf_of_isCompl_of_le h₁ h₂

end AddCommGroup

section AddCommGroup

variable [Semiring R] [Semiring R₂]
variable [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂]
variable {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂]

theorem comap_map_eq (f : F) (p : Submodule R M) : comap f (map f p) = p ⊔ LinearMap.ker f := by
  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (comap_mono bot_le))
  rintro x ⟨y, hy, e⟩
  exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩
#align submodule.comap_map_eq Submodule.comap_map_eq

theorem comap_map_eq_self {f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p) :
    comap f (map f p) = p := by rw [Submodule.comap_map_eq, sup_of_le_left h]
#align submodule.comap_map_eq_self Submodule.comap_map_eq_self

lemma _root_.LinearMap.range_domRestrict_eq_range_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
    LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ (LinearMap.ker f) = ⊤ := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [eq_top_iff]
    intro x _
    have : f x ∈ LinearMap.range f := LinearMap.mem_range_self f x
    rw [← h] at this
    obtain ⟨y, hy⟩ : ∃ y : S, f.domRestrict S y = f x := this
    have : (y : M) + (x - y) ∈ S ⊔ (LinearMap.ker f) := Submodule.add_mem_sup y.2 (by simp [← hy])
    simpa using this
  · refine le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_
    rintro x ⟨y, rfl⟩
    obtain ⟨s, hs, t, ht, rfl⟩ : ∃ s, s ∈ S ∧ ∃ t, t ∈ LinearMap.ker f ∧ s + t = y :=
      Submodule.mem_sup.1 (by simp [h])
    exact ⟨⟨s, hs⟩, by simp [LinearMap.mem_ker.1 ht]⟩

@[simp] lemma _root_.LinearMap.surjective_domRestrict_iff
    {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Surjective f) :
    Surjective (f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤ := by
  rw [← LinearMap.range_eq_top] at hf ⊢
  rw [← hf]
  exact LinearMap.range_domRestrict_eq_range_iff

@[simp]
lemma biSup_comap_subtype_eq_top {ι : Type*} (s : Set ι) (p : ι → Submodule R M) :
    ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤ := by
  refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_
  suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
    exact hy
  suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
    simpa only [map_iSup, biSup_congr this]
  intro i hi
  rw [map_comap_eq, range_subtype, inf_eq_right]
  exact le_biSup p hi

lemma biSup_comap_eq_top_of_surjective {ι : Type*} (s : Set ι) (hs : s.Nonempty)
    (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤)
    (f : M →ₛₗ[τ₁₂] M₂) (hf : Surjective f) :
    ⨆ i ∈ s, (p i).comap f = ⊤ := by
  obtain ⟨k, hk⟩ := hs
  suffices (⨆ i ∈ s, (p i).comap f) ⊔ LinearMap.ker f = ⊤ by
    rw [← this, left_eq_sup]; exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)
  rw [iSup_subtype'] at hp ⊢
  rw [← comap_map_eq, map_iSup_comap_of_sujective hf, hp, comap_top]

lemma biSup_comap_eq_top_of_range_eq_biSup
    {R R₂ : Type*} [Ring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
    [Module R M] [Module R₂ M₂] {ι : Type*} (s : Set ι) (hs : s.Nonempty)
    (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
    ⨆ i ∈ s, (p i).comap f = ⊤ := by
  suffices ⨆ i ∈ s, (p i).comap (LinearMap.range f).subtype = ⊤ by
    rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]; rfl
  exact hf ▸ biSup_comap_subtype_eq_top s p

end AddCommGroup

section DivisionRing

variable [DivisionRing K] [AddCommGroup V] [Module K V]

/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `WCovBy` version. -/
theorem wcovBy_span_singleton_sup (x : V) (p : Submodule K V) : WCovBy p ((K ∙ x) ⊔ p) := by
  refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_le ?_⟩
  rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩
  obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ p, c • x + z = y := by
    simpa [mem_sup, mem_span_singleton] using hqp.le hyq
  rcases eq_or_ne c 0 with rfl | hc
  · simp [hz] at hyp
  · have : x ∈ q := by
      rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq
    simp [hpq.le, this]

/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `CovBy` version. -/
theorem covBy_span_singleton_sup {x : V} {p : Submodule K V} (h : x ∉ p) : CovBy p ((K ∙ x) ⊔ p) :=
  ⟨by simpa, (wcovBy_span_singleton_sup _ _).2⟩

end DivisionRing

end Submodule

namespace LinearMap

open Submodule Function

section AddCommGroup

variable [Semiring R] [Semiring R₂]
variable [AddCommGroup M] [AddCommGroup M₂]
variable [Module R M] [Module R₂ M₂]
variable {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂]

protected theorem map_le_map_iff (f : F) {p p'} : map f p ≤ map f p' ↔ p ≤ p' ⊔ ker f := by
  rw [map_le_iff_le_comap, Submodule.comap_map_eq]
#align linear_map.map_le_map_iff LinearMap.map_le_map_iff

theorem map_le_map_iff' {f : F} (hf : ker f = ⊥) {p p'} : map f p ≤ map f p' ↔ p ≤ p' := by
  rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]
#align linear_map.map_le_map_iff' LinearMap.map_le_map_iff'

theorem map_injective {f : F} (hf : ker f = ⊥) : Injective (map f) := fun _ _ h =>
  le_antisymm ((map_le_map_iff' hf).1 (le_of_eq h)) ((map_le_map_iff' hf).1 (ge_of_eq h))
#align linear_map.map_injective LinearMap.map_injective

theorem map_eq_top_iff {f : F} (hf : range f = ⊤) {p : Submodule R M} :
    p.map f = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤ := by
  simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]
#align linear_map.map_eq_top_iff LinearMap.map_eq_top_iff

end AddCommGroup

section

variable (R) (M) [Semiring R] [AddCommMonoid M] [Module R M]

/-- Given an element `x` of a module `M` over `R`, the natural map from
    `R` to scalar multiples of `x`. See also `LinearMap.ringLmapEquivSelf`. -/
@[simps!]
def toSpanSingleton (x : M) : R →ₗ[R] M :=
  LinearMap.id.smulRight x
#align linear_map.to_span_singleton LinearMap.toSpanSingleton

/-- The range of `toSpanSingleton x` is the span of `x`. -/
theorem span_singleton_eq_range (x : M) : (R ∙ x) = range (toSpanSingleton R M x) :=
  Submodule.ext fun y => by
    refine Iff.trans ?_ LinearMap.mem_range.symm
    exact mem_span_singleton
#align linear_map.span_singleton_eq_range LinearMap.span_singleton_eq_range

-- @[simp] -- Porting note (#10618): simp can prove this
theorem toSpanSingleton_one (x : M) : toSpanSingleton R M x 1 = x :=
  one_smul _ _
#align linear_map.to_span_singleton_one LinearMap.toSpanSingleton_one

@[simp]
theorem toSpanSingleton_zero : toSpanSingleton R M 0 = 0 := by
  ext
  simp
#align linear_map.to_span_singleton_zero LinearMap.toSpanSingleton_zero

variable {R M}

theorem toSpanSingleton_isIdempotentElem_iff {e : R} :
    IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e := by
  simp_rw [IsIdempotentElem, ext_iff, mul_apply, toSpanSingleton_apply, smul_eq_mul, mul_assoc]
  exact ⟨fun h ↦ by conv_rhs => rw [← one_mul e, ← h, one_mul], fun h _ ↦ by rw [h]⟩

theorem isIdempotentElem_apply_one_iff {f : Module.End R R} :
    IsIdempotentElem (f 1) ↔ IsIdempotentElem f := by
  rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem, ext_iff]
  simp_rw [mul_apply]
  exact ⟨fun h r ↦ by rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h], (· 1)⟩

end

section AddCommMonoid

variable [Semiring R] [AddCommMonoid M] [Module R M]
variable [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂]
variable {F : Type*} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂]

/-- Two linear maps are equal on `Submodule.span s` iff they are equal on `s`. -/
theorem eqOn_span_iff {s : Set M} {f g : F} : Set.EqOn f g (span R s) ↔ Set.EqOn f g s := by
  rw [← le_eqLocus, span_le]; rfl

/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

This version uses `Set.EqOn`, and the hidden argument will expand to `h : x ∈ (span R s : Set M)`.
See `LinearMap.eqOn_span` for a version that takes `h : x ∈ span R s` as an argument. -/
theorem eqOn_span' {s : Set M} {f g : F} (H : Set.EqOn f g s) :
    Set.EqOn f g (span R s : Set M) :=
  eqOn_span_iff.2 H
#align linear_map.eq_on_span' LinearMap.eqOn_span'

/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

See also `LinearMap.eqOn_span'` for a version using `Set.EqOn`. -/
theorem eqOn_span {s : Set M} {f g : F} (H : Set.EqOn f g s) ⦃x⦄ (h : x ∈ span R s) :
    f x = g x :=
  eqOn_span' H h
#align linear_map.eq_on_span LinearMap.eqOn_span

/-- If `s` generates the whole module and linear maps `f`, `g` are equal on `s`, then they are
equal. -/
theorem ext_on {s : Set M} {f g : F} (hv : span R s = ⊤) (h : Set.EqOn f g s) : f = g :=
  DFunLike.ext _ _ fun _ => eqOn_span h (eq_top_iff'.1 hv _)
#align linear_map.ext_on LinearMap.ext_on

/-- If the range of `v : ι → M` generates the whole module and linear maps `f`, `g` are equal at
each `v i`, then they are equal. -/
theorem ext_on_range {ι : Sort*} {v : ι → M} {f g : F} (hv : span R (Set.range v) = ⊤)
    (h : ∀ i, f (v i) = g (v i)) : f = g :=
  ext_on hv (Set.forall_mem_range.2 h)
#align linear_map.ext_on_range LinearMap.ext_on_range

end AddCommMonoid

section NoZeroDivisors

variable (R M)
variable [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]

theorem ker_toSpanSingleton {x : M} (h : x ≠ 0) : LinearMap.ker (toSpanSingleton R M x) = ⊥ :=
  SetLike.ext fun _ => smul_eq_zero.trans <| or_iff_left_of_imp fun h' => (h h').elim
#align linear_map.ker_to_span_singleton LinearMap.ker_toSpanSingleton

end NoZeroDivisors

section Field

variable [Field K] [AddCommGroup V] [Module K V]

theorem span_singleton_sup_ker_eq_top (f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) :
    (K ∙ x) ⊔ ker f = ⊤ :=
  top_unique fun y _ =>
    Submodule.mem_sup.2
      ⟨(f y * (f x)⁻¹) • x, Submodule.mem_span_singleton.2 ⟨f y * (f x)⁻¹, rfl⟩,
        ⟨y - (f y * (f x)⁻¹) • x, by simp [hx]⟩⟩
#align linear_map.span_singleton_sup_ker_eq_top LinearMap.span_singleton_sup_ker_eq_top

end Field

end LinearMap

open LinearMap

namespace LinearEquiv

variable (R M)
variable [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x ≠ 0)

/-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural
isomorphism from `R` to the span of `x` given by $r \mapsto r \cdot x$. -/
noncomputable
def toSpanNonzeroSingleton : R ≃ₗ[R] R ∙ x :=
  LinearEquiv.trans
    (LinearEquiv.ofInjective (LinearMap.toSpanSingleton R M x)
      (ker_eq_bot.1 <| ker_toSpanSingleton R M h))
    (LinearEquiv.ofEq (range <| toSpanSingleton R M x) (R ∙ x) (span_singleton_eq_range R M x).symm)
#align linear_equiv.to_span_nonzero_singleton LinearEquiv.toSpanNonzeroSingleton

@[simp] theorem toSpanNonzeroSingleton_apply (t : R) :
    LinearEquiv.toSpanNonzeroSingleton R M x h t =
      (⟨t • x, Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self x)⟩ : R ∙ x) := by
  rfl

theorem toSpanNonzeroSingleton_one :
    LinearEquiv.toSpanNonzeroSingleton R M x h 1 =
      (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) := by simp
#align linear_equiv.to_span_nonzero_singleton_one LinearEquiv.toSpanNonzeroSingleton_one

/-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural
isomorphism from the span of `x` to `R` given by $r \cdot x \mapsto r$. -/
noncomputable
abbrev coord : (R ∙ x) ≃ₗ[R] R :=
  (toSpanNonzeroSingleton R M x h).symm
#align linear_equiv.coord LinearEquiv.coord

theorem coord_self : (coord R M x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) = 1 := by
  rw [← toSpanNonzeroSingleton_one R M x h, LinearEquiv.symm_apply_apply]
#align linear_equiv.coord_self LinearEquiv.coord_self

theorem coord_apply_smul (y : Submodule.span R ({x} : Set M)) : coord R M x h y • x = y :=
  Subtype.ext_iff.1 <| (toSpanNonzeroSingleton R M x h).apply_symm_apply _
#align linear_equiv.coord_apply_smul LinearEquiv.coord_apply_smul

end LinearEquiv