modules over a ring

Stream: Is there code for X?

[Scott Morrison]

Any suggestions on how to get

import linear_algebra.basic

example (R : Type) [ring R] (M N : Type) [add_comm_monoid M] [add_comm_monoid N]
  [module R M] [module R N] : add_comm_group (M →ₗ[R] N) :=
by apply_instance -- fails!

If I add local attribute [instance] module.add_comm_monoid_to_add_comm_group then instead of failing the typeclass search hits max depth.

[Scott Morrison]

(The idea here being that you pick up negation on the linear maps by multiplying by -1 : R, which is central.)

[Johan Commelin]

@Eric Wieser @Kevin Buzzard I think you've been struggling(?) with similar things lately in the graded project, right?

[Johan Commelin]

My guess is that a global instance could cause diamonds for the sub and neg fields.

[Johan Commelin]

But it's really strange that you get timeouts with that local instance.

[Scott Morrison]

import linear_algebra.basic

example (R : Type) [ring R] (M N : Type) [add_comm_monoid M] [add_comm_monoid N]
  [module R M] [module R N] : add_comm_group (M →ₗ[R] N) :=
{ neg := λ f,
  { to_fun := λ x, (-1 : R) • f x,
    map_add' := λ x y, by simp,
    map_smul' := λ r x, by simp [←mul_smul],  },
  add_left_neg := λ f, begin
    ext,
    change (-1 : R) • f x + f x = 0,
    conv_lhs { congr, skip , rw ←one_smul R (f x), },
    rw ←add_smul,
    simp,
  end,
  ..(by apply_instance : add_comm_monoid (M →ₗ[R] N))}

works, but hopefully someone who has been fighting with modules/semimodules recently knows better than me if this belongs somewhere.

[Scott Morrison]

(Or is easier to achieve.)

[Kevin Buzzard]

Does this actually happen in the wild? I thought Eric wrote an instance in mathlib making M into an add_comm_group it's an add_comm_monoid which is a module over a ring but I've never had to use it. In the grading work in LTE we just avoid this issue by only working with subgroups when grading rings.

[Kevin Buzzard]

My gut feeling is that you should make M and N add_comm_groups first and that there's an instance somewhere which does this, or maybe it's just a def? [edit: oh, I just realised you knew this already!]

[Kevin Buzzard]

docs#module.add_comm_monoid_to_add_comm_group . It's a def, not an instance.

[Eric Wieser]

As Johan points out, the instance you're asking for is one that mathlib can't provide without introducing diamonds

[Eric Wieser]

What if instead of local attribute you summon the M and N instances with have?

[Eric Wieser]

docs#module.add_comm_monoid_to_add_comm_group can't be an instance even if we ignored the diamonds it would create, because typeclass search explodes looking for an R, and it creates a loop with docs#add_comm_group.to_add_comm_monoid

[Johan Commelin]

I think that in the end, you need to explain to Lean why N is a group, and then the rest can be done automatically by TC.

[Kevin Buzzard]

Scott, are you really in a situation where you need this? I can't really imagine that one finds oneself with an add_monoid that magically only becomes a group because it has an action of a ring. An action of a ring is much stronger than an action of the integers.

[Kevin Buzzard]

In the grading file in LTE I proved that an add_comm_group graded by add_submonoids has the property that all the add_submonoids are add_subgroups, but I can't imagine ever using it.

[Scott Morrison]

The thing I'm trying (and abjectly failing at) is proving that the general notion of projective in any category specializes in Module R to something that agrees with Kevin's is_projective predicate.

[Scott Morrison]

Module R is set up so that is expects R to be a ring, not just a semi-ring, and the objects to have add_comm_group instances, not just add_comm_monoid instances.

[Scott Morrison]

That in itself is fine.

[Scott Morrison]

The difficulty comes when I try to use is_projective.of_lifting_property, which quantifies over add_comm_monoids, even when we know we're looking at a ring, not a semiring.

[Scott Morrison]

And there is just typeclass hell. :-(

[Scott Morrison]

One possibility that I haven't tried out yet is pushing this all into the explicit/non-categorical side, and proving a variant of of_lifting_property that knows we're working over a ring, and then only quantifies over add_comm_groups.

[Scott Morrison]

(but probably this is just pushing the work around? at least no categorical machinery would be involved)

[Scott Morrison]

Okay, so I think this is the challenge: add to algebra/module/projective.lean the following:

theorem of_lifting_property' {R : Type u} [ring R]
  {P : Type v} [add_comm_group P] [module R P]
  -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
  (huniv : ∀ {M : Type (max v u)} {N : Type v} [add_comm_group M] [add_comm_group N],
    by exactI
    ∀ [module R M] [module R N],
    by exactI
    ∀ (f : M →ₗ[R] N) (g : P →ₗ[R] N),
  function.surjective f → ∃ (h : P →ₗ[R] M), f.comp h = g) :
  -- then `P` is projective.
  is_projective R P := sorry

[Scott Morrison]

It "should" just follow immediately from of_lifting_property, using that all modules over R are have an add_comm_group structure anyway. But it doesn't seem to be so easy. :-(

[Kevin Buzzard]

I would definitely write the sensible version quantifying over add_comm_groups! If I set things up for semirings then it was only to placate the "max generality" people. Who cares in practice about projective modules over a semiring which isn't a ring??

[Scott Morrison]

Huh... interestingly, if you don't bother trying to prove it using the existing of_lifting_property, but instead just copy and paste the proof with no changes, it works just fine. :-)

[Kevin Buzzard]

I'd just be tempted to reprove it. I had the same sort of issue with grading.lean in LTE. I couldn't reuse code because I had a map to subgroups and lean wanted a map to submonoids and I ran into problems so just gave up and duplicated code, and then later on when I was unhappy with the duplicated code I fixed it by deleting the submonoid stuff because we never used it

[Sebastien Gouezel]

I agree this should just be done over rings. Semimodules and semirings are, in my opinion, mainly useful when you want to use matrices with natural coefficients to do combinatorics. More abstract stuff is certainly fine with rings.

[Kevin Buzzard]

Yes, I also copy pasted code and it worked no problem

[Eric Wieser]

Johan Commelin said:

I think that in the end, you need to explain to Lean why N is a group, and then the rest can be done automatically by TC.

Even this turns out to be a nightmare, as the module you can produce is not the right type any more:

import linear_algebra.basic

attribute [ext] add_comm_monoid

example (R : Type) [ring R] (M N : Type) [add_comm_monoid M] [add_comm_monoid N]
  [module R M] [module R N] : add_comm_group (M →ₗ[R] N) :=
begin
  letI : add_comm_group N := module.add_comm_monoid_to_add_comm_group R,
  letI ret := @linear_map.add_comm_group R M N _ _ _ _ (id _),
  swap,
  { convert _inst_5,
    { ext; refl } },
  convert ret,
  sorry
end

[Scott Morrison]

Okay, now that I've realised I can prove of_lifting_property' by copy and paste, my proposed course of action is:

1. a first PR that shows that the existing defn of is_projective agrees with the categorical projective.
2. an optional second PR to restrict the existing defn of is_projective to modules over rings.

[Eric Wieser]

Ah, got it:

example (R : Type) [ring R] (M N : Type) [add_comm_monoid M] [add_comm_monoid N]
  [module R M] [module R N] : add_comm_group (M →ₗ[R] N) :=
begin
  letI g : add_comm_group N := module.add_comm_monoid_to_add_comm_group R,
  have key : @add_comm_group.to_add_comm_monoid _ g = ‹add_comm_monoid N› := by { ext; refl },
  letI ret := @linear_map.add_comm_group R M N _ _ _ _ (id _),
  swap,
  { rw key,
    exact _inst_5, },
  { convert ret,
    { rw key},
    simp,
    refine (cast_heq _ _).symm }
end

[Eric Wieser]

possibly golfable

[Eric Wieser]

The fact that key is not (and cannot be?) true by rfl is what dooms that proof