internal/external direct sum

Stream: maths

[Antoine Chambert-Loir]

Given an R-algebra A, with submodules (\iota \to M) my goal this weekend was to endow this algebra of a structure of graded algebra. I wrote the code below, but I wonder whether this could already be somewhere…

Moreover, it is likely that I don't understand something, I feel docs#algebra.direct_sum.internal talks about external direct sums, and don't understand why docs#direct_sum.coe_ring_hom should be an isomorphism (as written in the docstring).

import algebra.direct_sum.basic
import ring_theory.graded_algebra.basic

noncomputable theory

section direct_sum
/- Given an R-algebra A and a family (ι → submodule R A) of submodules
parameterized by an additive monoid
and statisfying `set_like.graded_monoid M` (essentially, is multiplicative)
such that `direct_sum.is_internal M` (A is the direct sum of the M i),
we endow A with the structure of a graded algebra.
The submodules are the *homogeneous* parts -/


variables (R : Type*) [comm_semiring R] (A : Type*) [comm_semiring A] [algebra R A]
variables (ι : Type*) [decidable_eq ι]

variables (M : ι → submodule R A) [add_monoid ι] [set_like.graded_monoid M]

variables {R A ι M}

def decompose_fun_of (hM : direct_sum.is_internal M) :
  A → direct_sum ι (λ (i : ι), ↥(M i)) := (function.bijective_iff_has_inverse.mp hM).some

lemma decompose_fun_of_apply_iff (hM : direct_sum.is_internal M) (a : A) (b : direct_sum ι (λ (i : ι), ↥(M i))) : decompose_fun_of hM a = b ↔
  a = direct_sum.coe_add_monoid_hom M b :=
begin
  have hMl : function.left_inverse (decompose_fun_of hM) ⇑(direct_sum.coe_add_monoid_hom M) := (function.bijective_iff_has_inverse.mp hM).some_spec.1,
  have hMr : function.right_inverse (decompose_fun_of hM) ⇑(direct_sum.coe_add_monoid_hom M) := (function.bijective_iff_has_inverse.mp hM).some_spec.2,
  split,
  { intro hab, rw [← hab, hMr a], },
  { intro hab, rw [hab, hMl b], }
end

def decompose_of (hM : direct_sum.is_internal M) :
  A →ₐ[R] direct_sum ι (λ (i : ι), ↥(M i)) := {
to_fun    := decompose_fun_of hM,
map_one'  :=
begin
  rw decompose_fun_of_apply_iff,
  have : (direct_sum.of (λ (i : ι), ↥(M i)) 0) 1 = 1 := rfl,
  simp only [← this,  direct_sum.coe_add_monoid_hom_of],
  refl,
end,
map_mul'  := λ a b,
begin
  classical,
  rw direct_sum.mul_eq_sum_support_ghas_mul,
  rw decompose_fun_of_apply_iff,
  conv_lhs { rw (decompose_fun_of_apply_iff hM a _).mp rfl,
    rw (decompose_fun_of_apply_iff hM b _).mp rfl,
  rw ← direct_sum.sum_support_of (λ i, ↥(M i)) (decompose_fun_of hM a),
  rw ← direct_sum.sum_support_of (λ i, ↥(M i)) (decompose_fun_of hM b), },
  rw map_sum, rw map_sum,
  rw finset.sum_mul_sum,
  rw map_sum,
  apply congr_arg2,
  refl,
  ext ⟨i,j⟩,
  simp only [direct_sum.coe_add_monoid_hom_of, set_like.coe_ghas_mul],
end,
map_zero' := by rw [decompose_fun_of_apply_iff, map_zero],
map_add'  := λ a b,
begin
  rw [decompose_fun_of_apply_iff, map_add],
  apply congr_arg2 (+),
  rw ← decompose_fun_of_apply_iff, rw ← decompose_fun_of_apply_iff,
end,
commutes' := λ r,
begin
  rw [decompose_fun_of_apply_iff, direct_sum.algebra_map_apply],
  simp only [direct_sum.coe_add_monoid_hom_of, submodule.set_like.coe_galgebra_to_fun],
end }

def graded_algebra_of (hM : direct_sum.is_internal M): graded_algebra M :=
graded_algebra.of_alg_hom M (decompose_of hM) (
  begin
    ext a,
    simp only [alg_hom.coe_comp, function.comp_app, alg_hom.coe_id, id.def],
    apply symm,
    suffices : a = (direct_sum.coe_add_monoid_hom M) ((decompose_fun_of hM) a),
    exact this,
    rw ← (decompose_fun_of_apply_iff hM _ _),
  end) (
  begin
    intros i x,
    suffices : (decompose_fun_of hM) ↑x = _,
    exact this,
    rw decompose_fun_of_apply_iff hM,
    rw direct_sum.coe_add_monoid_hom_of ,
  end)

end direct_sum

[Adam Topaz]

I think the word "isomorphism" in this docstring (and the definition that follows it) is a typo

[Adam Topaz]

The other link you mentioned doesn't work for me. Did you mean docs#direct_sum.is_internal ?

[Adam Topaz]

If you only care about the algebra isomorphism, then the following simplifies things a little bit:

import algebra.direct_sum.basic
import ring_theory.graded_algebra.basic

noncomputable theory

section direct_sum
/- Given an R-algebra A and a family (ι → submodule R A) of submodules
parameterized by an additive monoid
and statisfying `set_like.graded_monoid M` (essentially, is multiplicative)
such that `direct_sum.is_internal M` (A is the direct sum of the M i),
we endow A with the structure of a graded algebra.
The submodules are the *homogeneous* parts -/


variables (R : Type*) [comm_semiring R] (A : Type*) [comm_semiring A] [algebra R A]
variables (ι : Type*) [decidable_eq ι]

variables (M : ι → submodule R A) [add_monoid ι] [set_like.graded_monoid M]

variables {R A ι M}

def coe_alg_iso_of_is_internal (hM : direct_sum.is_internal M) :
  direct_sum ι (λ i, ↥(M i)) ≃ₐ[R] A :=
{ commutes' := λ r, by simp,
  ..(ring_equiv.of_bijective (direct_sum.coe_alg_hom M) hM) }

end direct_sum

[Adam Topaz]

your map would then become coe_alg_iso_of_is_internal M hM).symm

[Adam Topaz]

We also have docs#direct_sum.decompose_alg_equiv but that would require a docs#graded_algebra instance

[Adam Topaz]

Here's a more complete bit of code, with the final graded algebra instance:

import algebra.direct_sum.basic
import ring_theory.graded_algebra.basic

noncomputable theory

section direct_sum
/- Given an R-algebra A and a family (ι → submodule R A) of submodules
parameterized by an additive monoid
and statisfying `set_like.graded_monoid M` (essentially, is multiplicative)
such that `direct_sum.is_internal M` (A is the direct sum of the M i),
we endow A with the structure of a graded algebra.
The submodules are the *homogeneous* parts -/


variables (R : Type*) [comm_semiring R] (A : Type*) [comm_semiring A] [algebra R A]
variables (ι : Type*) [decidable_eq ι]

variables (M : ι → submodule R A) [add_monoid ι] [set_like.graded_monoid M]

variables {R A ι M}

def coe_alg_iso_of_is_internal (hM : direct_sum.is_internal M) :
  direct_sum ι (λ i, ↥(M i)) ≃ₐ[R] A :=
{ commutes' := λ r, by simp,
  ..(ring_equiv.of_bijective (direct_sum.coe_alg_hom M) hM) }

def graded_algebra_of_is_internal (hM : direct_sum.is_internal M) :
  graded_algebra M :=
{ decompose' := (coe_alg_iso_of_is_internal hM).symm,
  left_inv := (coe_alg_iso_of_is_internal hM).symm.left_inv,
  right_inv := (coe_alg_iso_of_is_internal hM).left_inv,
  ..(infer_instance : set_like.graded_monoid M) }

end direct_sum

[Antoine Chambert-Loir]

Adam Topaz said:

The other link you mentioned doesn't work for me. Did you mean docs#direct_sum.is_internal ?

Actually, I meant the whole file that contains docs#direct_sum.is_internal…

[Antoine Chambert-Loir]

There are similar instances that one could write (graded modules, etc.). Do you think I should add them to mathlib? (With @María Inés de Frutos Fernández , we will probably need quotients of graded modules, algebra, etc. That will also be useful for those working on schemes.)

[Eric Wieser]

The expectation is that you use docs#graded_algebra here, as that's the constructive version of is_internal

[Eric Wieser]

I would guess you can golf the above even further with docs#alg_equiv.of_bijective

[Adam Topaz]

I looked for this alg equiv of bijective but didn’t find it! Yes using that would be even better.