Agreement on intersection

Stream: new members

[uzu]

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]

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

[uzu]

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]

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 :=
begin
  sorry,
end

[uzu]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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 :=
begin
  sorry,
end

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]

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

[Mario Carneiro]

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 :=
begin
  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 },
end

[uzu]

oh wow okay

[uzu]

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

[Eric Wieser]

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]

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