Zulip Chat Archive

Stream: Is there code for X?

Topic: Obtain isomorphism from short exact sequence


Kyle Miller (Nov 13 2022 at 17:19):

I've been working on filling out some of the API around dual annihilators of submodules, and an isomorphism that would be nice to have is that (V/W)ann(W)(V/W)^* \approx \operatorname{ann}(W), where WW is a subspace of a vector space VV.

The argument I was thinking of is that you can take the short exact sequence 0WVV/W00 \to W \to V \to V/W \to 0, dualize it to get 0(V/W)WV00 \to (V/W)^* \to W^* \to V^* \to 0, and then identify (V/W)(V/W)^* with the kernel of WVW^* \to V^*, which happens to be ann(W)\operatorname{ann}(W) by definition.

This is where I'm working: https://github.com/leanprover-community/mathlib/pull/17521/files#diff-44f047eef7a6b2bf415612b8834b73544a7697e940b4b7f81e5359560e28ab7cR936

Here's the sorried definition:

import linear_algebra.dual

variables {K : Type*} [field K] {V₁ : Type*}
variables [add_comm_group V₁] [module K V₁]

def dual_quot_equiv_dual_annihilator (W : submodule K V₁) :
  module.dual K (V₁  W) ≃ₗ[K] W.dual_annihilator :=
sorry

Kyle Miller (Nov 13 2022 at 17:27):

While the high-powered fact is that taking duals of vector spaces is an exact functor so colimits become limits, maybe there's an easier construction that comes from pre-existing linear algebra in mathlib?

Adam Topaz (Nov 13 2022 at 17:57):

@Kyle Miller I think I proved this result in https://github.com/adamtopaz/lean-acl-pairs

Adam Topaz (Nov 13 2022 at 17:58):

I was planning to put the general duality stuff proved there in mathlib, but haven't gotten to it yet

Junyan Xu (Nov 13 2022 at 19:11):

No need of field here, comm_ring suffices (and no need of (dualizing) exact sequences, it's pretty much by definition):

import linear_algebra.dual

variables {K : Type*} [comm_ring K] {V₁ : Type*}
variables [add_comm_group V₁] [module K V₁]

def dual_quot_equiv_dual_annihilator (W : submodule K V₁) :
  module.dual K (V₁  W) ≃ₗ[K] W.dual_annihilator :=
linear_equiv.of_linear
  (linear_map.cod_restrict _ (module.dual.transpose W.mkq) $
    λ φ, (submodule.mem_dual_annihilator _).2 $
    λ w hw, (congr_arg φ $ W^.quotient.mk_eq_zero.2 hw).trans φ.map_zero)
  (linear_map.flip $ W.liftq (linear_map.dom_restrict (module.dual_pairing K V₁) _).flip $
    λ w hw, by { ext φ, ⟩, exact (submodule.mem_dual_annihilator φ).1  w hw })
  (by { ext, refl }) (by { ext, refl })

Adam Topaz (Nov 13 2022 at 19:27):

You need field (or some projectivity assumption) for the cokernel on the dual side.

Junyan Xu (Nov 13 2022 at 19:31):

In general, V₁ ⧸ W →ₗ[K] V can be identified with a K-submodule of V₁ →ₗ[K] V. More generally, if U →ₗ[K] V is surjective then the induced map (V →ₗ[K] W) →ₗ[K] (U →ₗ[K] W) is injective for any W, so we can identify V →ₗ[K] W with a K-submodule of U →ₗ[K] W.

By the way, W* → V* should be V* → W* in the first post.

Junyan Xu (Nov 13 2022 at 19:32):

You need field (or some projectivity assumption) for the cokernel on the dual side.

Where is cokernel on the dual side used? In your repo or in Kyle's work?

Adam Topaz (Nov 13 2022 at 19:34):

Oh I don't think it appears in the original post. Or in the repo. I just mentioned this because it's part of having a "good" duality theory. You want quotients in the dual to correspond to submodules in the original module, and vice versa.

Adam Topaz (Nov 13 2022 at 19:57):

I think it's actually an interesting question regarding how to best set up such "duality" theories. In the case that I needed for my repo linked above, I had a vector space VV over a field KK, and, essentially, obtained a duality between quotients of VV and closed (w.r.t. the weak topology) subspaces of the dual. I'm sure the functional analysts have developed a general approach to such things... does anyone know of a good reference for this?

Anatole Dedecker (Nov 13 2022 at 21:10):

Section IV.1.4 in Bourbaki TVS seems to be related, but there are probably ways to make it way easier for the special case of the weak dual topology.

Kyle Miller (Nov 14 2022 at 17:21):

Thanks @Junyan Xu!

I extracted this characterization you mentioned of the dual annihilator as a quick corollary of the equivalence:

lemma range_dual_map_mkq_eq_dual_annihilator (W : submodule R M) :
  (submodule.mkq W).dual_map.range = W.dual_annihilator

In #17521 I also have the following lemma for vector spaces

lemma range_dual_map_eq_dual_annihilator_ker (f : V₁ →ₗ[K] V₂) :
  f.dual_map.range = f.ker.dual_annihilator

Do you think this could be generalized to commutative rings as well? I've already added a version for when f is a surjection as a corollary to range_dual_map_mkq_eq_dual_annihilator.

Junyan Xu (Nov 14 2022 at 17:58):

Looks nice! I think you can get f.dual_map.range ≤ f.ker.dual_annihilator but for the other direction you can only get a R-linear functional on V₁ ⧸ f.ker but can't necessarily extend it to a functional on V₂.

Kyle Miller (Nov 14 2022 at 17:58):

Yeah, I just realized it doesn't generalize. For example, the map f:ZZf : \mathbb{Z}\to\mathbb{Z} from multiplication by two.

Adam Topaz (Nov 14 2022 at 17:58):

you need projectivity :)

Kyle Miller (Nov 14 2022 at 18:06):

Yeah, you can prove it with a very weak form of projectivity:

lemma range_dual_map_eq_dual_annihilator_ker
  (f : M →ₗ[R] M') (hf : function.surjective ((linear_map.range f).subtype.dual_map)) :
  f.dual_map.range = f.ker.dual_annihilator :=

proof

Adam Topaz (Nov 14 2022 at 18:08):

That's probably useful as is (using a surjectivity assumption) but I think it's worthwhile to formulate a lemma using docs#module.projective as well, since that's a typeclass, and any module over a field is projective

Kyle Miller (Nov 14 2022 at 18:09):

@Junyan Xu That inequality is very easy in comparison and works for commutative semirings too. It looks like @JasonKYi added it two years ago (thanks!)

Kyle Miller (Nov 14 2022 at 18:10):

@Adam Topaz I wasn't sure I was going to include it in the PR since the condition is rather technical and I don't need any of this (I'm just trying to add everything that might be considered to be basic theory for dual annihilators to check off the "orthogonality" item off the undergrad list!), but a projective version seems reasonable, though perhaps not to undergrads

Kyle Miller (Nov 14 2022 at 18:12):

Hmm, module.projective isn't available in linear_algebra/dual. Would it be bad to import it?

Johan Commelin (Nov 14 2022 at 18:14):

Given what we've been seeing in the lower parts of the import graph lately, I would suggest this import is "bad".

Johan Commelin (Nov 14 2022 at 18:14):

A priori, projective and dual seem orthogonal concepts. So neither should import the other.

Johan Commelin (Nov 14 2022 at 18:15):

I don't know what their lub should be though.

Adam Topaz (Nov 14 2022 at 18:15):

Maybe there should be a separate file for some sort of "duality theory" (and perhaps the current dual should be renamed)?

Adam Topaz (Nov 14 2022 at 18:16):

OTOH, I would guess that dual is pretty close to being a leaf in the import tree

Kyle Miller (Nov 14 2022 at 18:22):

Actually, I'm getting confused. Is projectivity the right concept, or is it injectivity? It seems like function.surjective f.range.subtype.dual_map is true if R is an injective R-module.

Adam Topaz (Nov 14 2022 at 18:23):

You just need an Ext term to vanish, so you can either assume the ring is injective, or some module is projective

Kyle Miller (Nov 14 2022 at 18:24):

What about the f:ZZf:\mathbb{Z}\to\mathbb{Z} example where it's multiplication by 2? All of these are projective Z\mathbb{Z}-modules.

Adam Topaz (Nov 14 2022 at 18:25):

But the cokernel isnt

Adam Topaz (Nov 14 2022 at 18:26):

The issue is that Z/2 is not projective

Adam Topaz (Nov 14 2022 at 18:36):

Note that at least for domains AA, the AA-module AA is injective if and only if AA is a field, so I think using a projectivity assumption on the quotient would be more useful in more cases.

Kyle Miller (Nov 14 2022 at 18:39):

For now, I'll leave the PR with this technical version, and maybe I'll look into where to put a projective version (maybe one answer is to add a lemma that gives this surjectivity assumption given projectivity of the cokernel?)

Kyle Miller (Nov 14 2022 at 18:40):

Here's another question. I've got

lemma dual_annihilator_infi_eq {ι : Type*} [_root_.finite ι] (W : ι  submodule K V₁) :
  ( (i : ι), W i).dual_annihilator = ( (i : ι), (W i).dual_annihilator)

with this finiteness condition. It's surely true in more cases (like probably if W is a cofiltered family). Is there an obviously good condition to state?

Adam Topaz (Nov 14 2022 at 18:41):

docs#submodule.dual_annihilator

Adam Topaz (Nov 14 2022 at 18:42):

right, in general there is some (topological) closure that needs to happen as well.

Kyle Miller (Nov 14 2022 at 18:42):

I'm very tempted to leave this with a finite indexing type, or at best see if when the vector space is finite-dimensional then there is good API for restricting infinite indexing sets to equivalent finite ones.

Adam Topaz (Nov 14 2022 at 18:49):

It should be easy to obtain an inclusion in one direction in the general case. Maybe that's enough for now?

Kyle Miller (Nov 14 2022 at 18:52):

Yeah, docs#submodule.supr_dual_annihilator_le_infi was straightforward.

Junyan Xu (Nov 14 2022 at 21:18):

Johan Commelin said:

A priori, projective and dual seem orthogonal concepts. So neither should import the other.

Yes probably we should add another file, but I've previously noticed that a lot of stuff around dual and contraction could be generalized from finite free modules to finite projective modules, so they would need to be moved to the new file when generalized. Also note that projective modules of rank 1 are invertible sheaves / line bundles, and the dual is the inverse. For Dedekind domains all nonzero ideals are projective (invertible). So there's definitely a lot of overlapping theory to be developed.

About the generalization from comm_ring to comm_semiring: It's docs#submodule.has_quotient that requires [ring R], and we should probably generalize it as well. (If there's an initial ring that a semiring maps to (not sure if one of commutativity and addition cancellativity is needed) then we may use that, but that's more complicated and the construction isn't in mathlib AFAIK.)

Riccardo Brasca (Nov 14 2022 at 21:40):

I think that rather than generalizing by hand a lot of stuff from free to projective modules, what we should do is to prove that these properties are local for the Zariski topology (and characterize projective modules, something is not in mathlib I am afraid).


Last updated: Dec 20 2023 at 11:08 UTC