Algebras generated by a submodule

Stream: maths

[Eric Wieser]

Do we have a canonical way to express (⨆ i : ℕ, ιS ^ i) = ⊤ when ιS is a submodule of generators of an algebra? I was able to prove this for clifford_algebra, exterior_algebra, and tensor_algebra, but I can't work out how to avoid copy-pasting the proof three times:

import linear_algebra.clifford_algebra.basic
import linear_algebra.dfinsupp
import algebra.algebra.subalgebra
import algebra.direct_sum_graded

open_locale direct_sum

namespace submodule
variables {R A : Type*} [comm_ring R] [semiring A] [algebra R A]

lemma to_add_submonoid_supr_nat_powers (S : submodule R A) :
  (⨆ i : ℕ, S ^ i).to_add_submonoid =
  (direct_sum.to_semiring
    (λ i : ℕ, (S ^ i).subtype.to_add_monoid_hom) rfl (λ i j hi hj, rfl)).srange.to_add_submonoid :=
begin
  rw submodule.supr_eq_range_dfinsupp_lsum,
  exact set_like.coe_injective rfl
end

lemma supr_nat_powers_eq_top_iff (S : submodule R A) :
  (⨆ i : ℕ, S ^ i) = ⊤ ↔
  (direct_sum.to_semiring
    (λ i : ℕ, (S ^ i).subtype.to_add_monoid_hom) rfl (λ i j hi hj, rfl)).srange = ⊤ :=
begin
  rw submodule.supr_eq_range_dfinsupp_lsum,
  rw ←subsemiring.to_add_submonoid_injective.eq_iff,
  rw ←submodule.to_add_submonoid_injective.eq_iff,
  exact iff.rfl,
end

end submodule

namespace clifford_algebra
variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
variables {Q : quadratic_form R M}

lemma supr_ι_range_eq_top : (⨆ i : ℕ, (ι Q).range ^ i) = ⊤ :=
begin
  rw [submodule.supr_nat_powers_eq_top_iff, subsemiring.eq_top_iff'],
  intro x,
  rw ring_hom.mem_srange,
  induction x using clifford_algebra.induction,
  case h_grade0 : r {
    refine ⟨direct_sum.of _ 0 _, _⟩,
    refine ⟨algebra_map _ _ r, _⟩,
    { simp only [pow_zero, submodule.mem_one, exists_apply_eq_apply], },
    rw [direct_sum.to_semiring_of],
    refl },
  case h_grade1 : m {
    refine ⟨direct_sum.of _ 1 _, _⟩,
    refine ⟨ι Q m, _⟩,
    { simp only [pow_one, linear_map.mem_range, exists_apply_eq_apply], },
    rw [direct_sum.to_semiring_of],
    refl },
  case h_add : x y hx hy {
    obtain ⟨fx, rfl⟩ := hx,
    obtain ⟨fy, rfl⟩ := hy,
    rw ←ring_hom.map_add,
    exact ⟨_, rfl⟩, },
  case h_mul : x y hx hy {
    obtain ⟨fx, rfl⟩ := hx,
    obtain ⟨fy, rfl⟩ := hy,
    rw ←ring_hom.map_mul,
    exact ⟨_, rfl⟩, },
end

end clifford_algebra

namespace exterior_algebra
variables {R M : Type*} [comm_ring R] [add_comm_monoid M] [module R M]

lemma supr_ι_range_eq_top : (⨆ i : ℕ, (ι R : M →ₗ[_] _).range ^ i) = ⊤ :=
begin
  rw [submodule.supr_nat_powers_eq_top_iff, subsemiring.eq_top_iff'],
  intro x,
  rw ring_hom.mem_srange,
  induction x using exterior_algebra.induction,
  case h_grade0 : r {
    refine ⟨direct_sum.of _ 0 _, _⟩,
    refine ⟨algebra_map _ _ r, _⟩,
    { simp only [pow_zero, submodule.mem_one, exists_apply_eq_apply], },
    rw [direct_sum.to_semiring_of],
    refl },
  case h_grade1 : m {
    refine ⟨direct_sum.of _ 1 _, _⟩,
    refine ⟨ι R m, _⟩,
    { simp only [pow_one, linear_map.mem_range, exists_apply_eq_apply], },
    rw [direct_sum.to_semiring_of],
    refl },
  case h_add : x y hx hy {
    obtain ⟨fx, rfl⟩ := hx,
    obtain ⟨fy, rfl⟩ := hy,
    rw ←ring_hom.map_add,
    exact ⟨_, rfl⟩, },
  case h_mul : x y hx hy {
    obtain ⟨fx, rfl⟩ := hx,
    obtain ⟨fy, rfl⟩ := hy,
    rw ←ring_hom.map_mul,
    exact ⟨_, rfl⟩, },
end

end exterior_algebra

namespace tensor_algebra
variables {R M : Type*} [comm_ring R] [add_comm_monoid M] [module R M]

lemma supr_ι_range_eq_top : (⨆ i : ℕ, (ι R : M →ₗ[_] _).range ^ i) = ⊤ :=
begin
  rw [submodule.supr_nat_powers_eq_top_iff, subsemiring.eq_top_iff'],
  intro x,
  rw ring_hom.mem_srange,
  induction x using tensor_algebra.induction,
  case h_grade0 : r {
    refine ⟨direct_sum.of _ 0 _, _⟩,
    refine ⟨algebra_map _ _ r, _⟩,
    { simp only [pow_zero, submodule.mem_one, exists_apply_eq_apply], },
    rw [direct_sum.to_semiring_of],
    refl },
  case h_grade1 : m {
    refine ⟨direct_sum.of _ 1 _, _⟩,
    refine ⟨ι R m, _⟩,
    { simp only [pow_one, linear_map.mem_range, exists_apply_eq_apply], },
    rw [direct_sum.to_semiring_of],
    refl },
  case h_add : x y hx hy {
    obtain ⟨fx, rfl⟩ := hx,
    obtain ⟨fy, rfl⟩ := hy,
    rw ←ring_hom.map_add,
    exact ⟨_, rfl⟩, },
  case h_mul : x y hx hy {
    obtain ⟨fx, rfl⟩ := hx,
    obtain ⟨fy, rfl⟩ := hy,
    rw ←ring_hom.map_mul,
    exact ⟨_, rfl⟩, },
end

end tensor_algebra

[Eric Wieser]

PR'd as #8781 for ease of reading, but I'm hoping for a trick to deduplicate it before considering merging