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


#### 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}
(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 (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
(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


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: May 10 2021 at 18:22 UTC