Zulip Chat Archive

Stream: new members

Topic: Agreement on intersection

uzu (Mar 11 2021 at 15:14):

Hi, I'm new on this chat :)
I'm currently trying to state and prove the following lemma:
If H1, H2 are subgroups of an abelian group K with maps f1 : H1 ->+ G and f2 : H2 ->+ G, then whenever f1 and f2 agree on the intersection, there is a map from the join H1 v H2 to G such that it restricts to f1 and f2 on H1 and H2.

I'm having problem with specifying that the two maps agree on the intersection. This is because H1 ⊓ H2 is a subgroup of K.
I considered using comap so that I can consider the preimage of H1 ⊓ H2 by H1.subtype and H2.subtype, but then I get two new subgroups of H1 and H2 and I still don't get to specify that f1 and f2 agree on the intersection.

What should I do to specify that two such morphisms agree on the intersection?

Thomas Browning (Mar 11 2021 at 15:37):

Would it work to state that the compositions (H1 cap H2) -> H1 -> G and (H1 cap H2) -> H2 -> G agree?

uzu (Mar 11 2021 at 17:13):

I don't think so, although I see a way to make it work:
If you pull back H1 cap H2 as a subgroup of H1, it has the type subgroup H1.
We then need isomorphisms between (the pullback of H1 cap H2 by H1 -> K) and (H1 cap H2) itself.
Then we can state agreement on intersection. But this seems terribly inelegant.

uzu (Mar 11 2021 at 17:14):

Here's a suggestion from @Eric Wieser, which at least sorts out the statement part of the initial question.

lemma extd_mor_from_add_subgps
{G : Type} [add_group G] (H1 H2 : add_subgroup G) (f1 : H1 →+ G) (f2 : H2 →+ G)
(h :  (x1 : H1) (x2 : H2), (x1 : G) = (x2 : G)  f1 x1 = f2 x2) :
   f : (H1  H2) →+ G,
    f.comp (add_subgroup.inclusion le_sup_left) = f1 
    f.comp (add_subgroup.inclusion le_sup_right) = f2 :=

uzu (Mar 11 2021 at 17:14):

However, Eric noted that it seems hard to actually prove this lemma.

Mario Carneiro (Mar 11 2021 at 17:18):

I would be tempted to generalize it to the case where ↥H1, ↥H2 and ↥(H1 ⊔ H2) are replaced by arbitrary types and you have an explicit pullback square. That should help get those proofs out of the statement

Mario Carneiro (Mar 11 2021 at 17:19):

This splits the task into two parts, one is to prove this theorem and the other is to prove that ↥(H1 ⊔ H2) is a pullback of the appropriate type

Mario Carneiro (Mar 11 2021 at 17:20):

I believe the latter is an easier task than this theorem though, because you can deal only with subsets instead of ->+ morphisms for that

uzu (Mar 11 2021 at 17:24):

That sounds tantalizing. However, at the moment I'm quite a beginner in Lean and I wouldn't know how to work with category here.

Mario Carneiro (Mar 11 2021 at 17:56):

I don't actually mean to use category theory notation, although that is an option; I just meant that you have four types, four ->+ functions and some equalities in the hypotheses that basically assert that the four types are in a pullback square

uzu (Mar 11 2021 at 18:01):

That's true. I'm going to sorry this part for now but if anyone has an idea of how to prove the above sorry, please let me know.

Mario Carneiro (Mar 11 2021 at 18:03):

here's a generalized statement:

lemma extd_mor_from_add_subgps' {G H1 H2 P : Type}
  [add_group G] [add_group H1] [add_group H2] [add_group P]
  (f1 i1 : H1 →+ G) (f2 i2 : H2 →+ G) (k1 : H1 →+ P) (k2 : H2 →+ P)
  (hP : sorry)
  (h :  (x1 : H1) (x2 : H2), i1 x1 = i2 x2  f1 x1 = f2 x2) :
   f : P →+ G, f.comp k1 = f1  f.comp k2 = f2 :=

The hP : sorry should say something about how P is a pullback, which is probably the same statement as the theorem but with i1 and i2 instead of f1 and f2

Mario Carneiro (Mar 11 2021 at 18:06):

Oh, interesting, this isn't a pullback diagram because the k1,k2 arrows go the wrong way

Mario Carneiro (Mar 11 2021 at 20:03):

I think this is actually a nontrivial proof. I think it can be done by zorn's lemma, although I've exceeded my time budget on this problem so I'll let someone else have a crack at it.

lemma extd_mor_from_add_subgps
  {A B : Type*} [add_group A] [add_group B] {ι} (H : ι  add_subgroup A)
  (f :  i, H i →+ B)
  (h :  i j (x1 : H i) (x2 : H j), (x1 : A) = (x2 : A)  f i x1 = f j x2) :
     g : (supr H) →+ B,
       i, g.comp (add_subgroup.inclusion (le_supr _ i)) = f i :=
  let S := {R : set (A × B) |
    ( x : B, ((0:A), x)  R  x = 0) 
     r : add_subgroup (A × B), r.carrier = R},
  let T := add_subgroup.closure {x |  i (a:H i), ((a:A), f i a) = x},
  obtain M, M0, Ma⟩, hM1, hM2 := zorn.zorn_subset₀ S _ T _, T, rfl⟩,
  { sorry },
  { intros c cs hc c0, sorry },
  { intros x h, sorry },

uzu (Mar 11 2021 at 20:16):

oh wow okay

uzu (Mar 11 2021 at 20:17):

maybe ill do a workaround for now, since I just need the case when one of the two subgroups is cyclic

Eric Wieser (Mar 12 2021 at 00:56):

The problem is a lot easier if you assume add_comm_group instead of add_group I think (and stick with the original two-subgroup formulation rather than an indexed family)

Mario Carneiro (Mar 12 2021 at 02:24):

I don't think the two-subgroup formulation is any easier, you need zorn's lemma either way, and there are a couple things you have to do twice instead of once with a variable. If you have commutative groups though this is a lot easier because you can use the fundamental theorem of abelian groups to decompose the sup into a direct sum, and then it's easy to describe the function by its action on the factors

Last updated: Dec 20 2023 at 11:08 UTC