Obtain isomorphism from short exact sequence

Stream: Is there code for X?

[Kyle Miller]

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)^* \approx \operatorname{ann}(W)$, where $W$ is a subspace of a vector space $V$.

The argument I was thinking of is that you can take the short exact sequence $0 \to W \to V \to V/W \to 0$, dualize it to get $0 \to (V/W)^* \to W^* \to V^* \to 0$, and then identify $(V/W)^*$ with the kernel of $W^* \to V^*$, which happens to be $\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]

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]

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

[Adam Topaz]

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

[Junyan Xu]

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]

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

[Junyan Xu]

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]

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]

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]

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 $V$ over a field $K$, and, essentially, obtained a duality between quotients of $V$ 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]

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]

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]

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]

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

[Adam Topaz]

you need projectivity :)

[Kyle Miller]

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

begin
  have rr_surj : function.surjective f.range_restrict,
  { rw [← linear_map.range_eq_top, linear_map.range_range_restrict] },
  have := range_dual_map_eq_dual_annihilator_ker_of_surjective f.range_restrict rr_surj,
  convert this using 1,
  { transitivity ((submodule.subtype f.range).comp f.range_restrict).dual_map.range,
    { refl, },
    rw [← linear_map.dual_map_comp_dual_map, linear_map.range_comp_of_range_eq_top],
    rwa linear_map.range_eq_top, },
  { congr' 1,
    exact (linear_map.ker_range_restrict f).symm, },
end

[Adam Topaz]

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]

@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]

@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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Adam Topaz]

But the cokernel isnt

[Adam Topaz]

The issue is that Z/2 is not projective

[Adam Topaz]

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

[Kyle Miller]

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]

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]

docs#submodule.dual_annihilator

[Adam Topaz]

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

[Kyle Miller]

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]

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

[Kyle Miller]

Yeah, docs#submodule.supr_dual_annihilator_le_infi was straightforward.

[Junyan Xu]

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]

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).