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 , where is a subspace of a vector space .
The argument I was thinking of is that you can take the short exact sequence , dualize it to get , and then identify with the kernel of , which happens to be 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 ⟨φ, hφ⟩, exact (submodule.mem_dual_annihilator φ).1 hφ 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 over a field , and, essentially, obtained a duality between quotients of 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 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 example where it's multiplication by 2? All of these are projective -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 , the -module is injective if and only if 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
anddual
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