Vertical line test for group homs

This file proves the vertical line test for monoid homomorphisms/isomorphisms.

Let f : G → H × I be a homomorphism to a product of monoids. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(h, i) | i : I} at most once. Then the image of f is the graph of some monoid homomorphism f' : H → I.

Furthermore, if f is also surjective on the second factor and its image intersects every "horizontal line" {(h, i) | h : H} at most once, then f' is actually an isomorphism f' : H ≃ I.

We also prove specialised versions when f is the inclusion of a subgroup of the direct product. (The version for general homomorphisms can easily be reduced to this special case, but the homomorphism version is more flexible in applications.)

def MonoidHom.mgraph {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : Submonoid (G × H)

The graph of a monoid homomorphism as a submonoid.

See also MonoidHom.graph for the graph as a subgroup.

def AddMonoidHom.mgraph {G : Type u_1} {H : Type u_2} [AddMonoid G] [AddMonoid H] (f : G →+ H) : AddSubmonoid (G × H)

The graph of a monoid homomorphism as a submonoid.

See also AddMonoidHom.graph for the graph as a subgroup.

@[simp]

theorem MonoidHom.coe_mgraph {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : ↑f.mgraph = {x : G × H | f x.1 = x.2}

@[simp]

theorem AddMonoidHom.coe_mgraph {G : Type u_1} {H : Type u_2} [AddMonoid G] [AddMonoid H] (f : G →+ H) : ↑f.mgraph = {x : G × H | f x.1 = x.2}

@[simp]

theorem MonoidHom.mem_mgraph {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] {f : G →* H} {x : G × H} : x ∈ f.mgraph ↔ f x.1 = x.2

@[simp]

theorem AddMonoidHom.mem_mgraph {G : Type u_1} {H : Type u_2} [AddMonoid G] [AddMonoid H] {f : G →+ H} {x : G × H} : x ∈ f.mgraph ↔ f x.1 = x.2

theorem MonoidHom.mgraph_eq_mrange_prod {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) : f.mgraph = mrange ((id G).prod f)

theorem AddMonoidHom.mgraph_eq_mrange_prod {G : Type u_1} {H : Type u_2} [AddMonoid G] [AddMonoid H] (f : G →+ H) : f.mgraph = mrange ((id G).prod f)

@[deprecated AddMonoidHom.mgraph_eq_mrange_prod (since := "2025-03-11")]

theorem AddMonoidHom.mgraph_eq_mrange_sum {G : Type u_1} {H : Type u_2} [AddMonoid G] [AddMonoid H] (f : G →+ H) : f.mgraph = mrange ((id G).prod f)

Alias of AddMonoidHom.mgraph_eq_mrange_prod.

theorem MonoidHom.exists_mrange_eq_mgraph {G : Type u_1} {H : Type u_2} {I : Type u_3} [Monoid G] [Monoid H] [Monoid I] {f : G →* H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ (f' : H →* I), mrange f = f'.mgraph

Vertical line test for monoid homomorphisms.

Let f : G → H × I be a homomorphism to a product of monoids. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(h, i) | i : I} at most once. Then the image of f is the graph of some monoid homomorphism f' : H → I.

theorem AddMonoidHom.exists_mrange_eq_mgraph {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddMonoid G] [AddMonoid H] [AddMonoid I] {f : G →+ H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ (f' : H →+ I), mrange f = f'.mgraph

Vertical line test for monoid homomorphisms.

Let f : G → H × I be a homomorphism to a product of monoids. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(h, i) | i : I} at most once. Then the image of f is the graph of some monoid homomorphism f' : H → I.

theorem MonoidHom.exists_mulEquiv_mrange_eq_mgraph {G : Type u_1} {H : Type u_2} {I : Type u_3} [Monoid G] [Monoid H] [Monoid I] {f : G →* H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf₂ : Function.Surjective (Prod.snd ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ (e : H ≃* I), mrange f = e.toMonoidHom.mgraph

Line test for monoid isomorphisms.

Let f : G → H × I be a homomorphism to a product of monoids. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(h, i) | i : I} and every "horizontal line" {(h, i) | h : H} at most once. Then the image of f is the graph of some monoid isomorphism f' : H ≃ I.

theorem AddMonoidHom.exists_addEquiv_mrange_eq_mgraph {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddMonoid G] [AddMonoid H] [AddMonoid I] {f : G →+ H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf₂ : Function.Surjective (Prod.snd ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ (e : H ≃+ I), mrange f = e.toAddMonoidHom.mgraph

Line test for monoid isomorphisms.

Let f : G → H × I be a homomorphism to a product of monoids. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(h, i) | i : I} and every "horizontal line" {(h, i) | h : H} at most once. Then the image of f is the graph of some monoid isomorphism f' : H ≃ I.

theorem Submonoid.exists_eq_mgraph {H : Type u_2} {I : Type u_3} [Monoid H] [Monoid I] {G : Submonoid (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) : ∃ (f : H →* I), G = f.mgraph

Vertical line test for monoid homomorphisms.

Let G ≤ H × I be a submonoid of a product of monoids. Assume that G maps bijectively to the first factor. Then G is the graph of some monoid homomorphism f : H → I.

theorem AddSubmonoid.exists_eq_mgraph {H : Type u_2} {I : Type u_3} [AddMonoid H] [AddMonoid I] {G : AddSubmonoid (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) : ∃ (f : H →+ I), G = f.mgraph

Vertical line test for additive monoid homomorphisms.

Let G ≤ H × I be a submonoid of a product of monoids. Assume that G surjects onto the first factor and G intersects every "vertical line" {(h, i) | i : I} at most once. Then G is the graph of some monoid homomorphism f : H → I.

theorem Submonoid.exists_mulEquiv_eq_mgraph {H : Type u_2} {I : Type u_3} [Monoid H] [Monoid I] {G : Submonoid (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) (hG₂ : Function.Bijective (Prod.snd ∘ ⇑G.subtype)) : ∃ (e : H ≃* I), G = e.toMonoidHom.mgraph

Goursat's lemma for monoid isomorphisms.

Let G ≤ H × I be a submonoid of a product of monoids. Assume that the natural maps from G to both factors are bijective. Then G is the graph of some isomorphism f : H ≃* I.

theorem AddSubmonoid.exists_addEquiv_eq_mgraph {H : Type u_2} {I : Type u_3} [AddMonoid H] [AddMonoid I] {G : AddSubmonoid (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) (hG₂ : Function.Bijective (Prod.snd ∘ ⇑G.subtype)) : ∃ (e : H ≃+ I), G = e.toAddMonoidHom.mgraph

Goursat's lemma for additive monoid isomorphisms.

Let G ≤ H × I be a submonoid of a product of additive monoids. Assume that the natural maps from G to both factors are bijective. Then G is the graph of some isomorphism f : H ≃+ I.

def MonoidHom.graph {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) : Subgroup (G × H)

The graph of a group homomorphism as a subgroup.

See also MonoidHom.mgraph for the graph as a submonoid.

def AddMonoidHom.graph {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : AddSubgroup (G × H)

The graph of a group homomorphism as a subgroup.

See also AddMonoidHom.mgraph for the graph as a submonoid.

@[simp]

theorem MonoidHom.coe_graph {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) : ↑f.graph = {x : G × H | f x.1 = x.2}

@[simp]

theorem MonoidHom.graph_toSubmonoid {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) : f.graph.toSubmonoid = f.mgraph

@[simp]

theorem AddMonoidHom.graph_toAddSubmonoid {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : f.graph.toAddSubmonoid = f.mgraph

@[simp]

theorem AddMonoidHom.coe_graph {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : ↑f.graph = {x : G × H | f x.1 = x.2}

theorem MonoidHom.mem_graph {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} {x : G × H} : x ∈ f.graph ↔ f x.1 = x.2

theorem AddMonoidHom.mem_graph {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} {x : G × H} : x ∈ f.graph ↔ f x.1 = x.2

theorem MonoidHom.graph_eq_range_prod {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) : f.graph = ((id G).prod f).range

theorem AddMonoidHom.graph_eq_range_prod {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : f.graph = ((id G).prod f).range

@[deprecated MonoidHom.graph_eq_range_prod (since := "2025-03-11")]

theorem MonoidHom.AddMonoidHom.graph_eq_range_sum {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) : f.graph = ((id G).prod f).range

Alias of MonoidHom.graph_eq_range_prod.

theorem MonoidHom.exists_range_eq_graph {G : Type u_1} {H : Type u_2} {I : Type u_3} [Group G] [Group H] [Group I] {f : G →* H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ (f' : H →* I), f.range = f'.graph

Vertical line test for group homomorphisms.

Let f : G → H × I be a homomorphism to a product of groups. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(h, i) | i : I} at most once. Then the image of f is the graph of some group homomorphism f' : H → I.

theorem AddMonoidHom.exists_range_eq_graph {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddGroup G] [AddGroup H] [AddGroup I] {f : G →+ H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ (f' : H →+ I), f.range = f'.graph

Vertical line test for group homomorphisms.

Let f : G → H × I be a homomorphism to a product of groups. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(h, i) | i : I} at most once. Then the image of f is the graph of some group homomorphism f' : H → I.

theorem MonoidHom.exists_mulEquiv_range_eq_graph {G : Type u_1} {H : Type u_2} {I : Type u_3} [Group G] [Group H] [Group I] {f : G →* H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf₂ : Function.Surjective (Prod.snd ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ (e : H ≃* I), f.range = e.toMonoidHom.graph

Line test for group isomorphisms.

Let f : G → H × I be a homomorphism to a product of groups. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(h, i) | i : I} and every "horizontal line" {(h, i) | h : H} at most once. Then the image of f is the graph of some group isomorphism f' : H ≃ I.

theorem AddMonoidHom.exists_addEquiv_range_eq_graph {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddGroup G] [AddGroup H] [AddGroup I] {f : G →+ H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf₂ : Function.Surjective (Prod.snd ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ (e : H ≃+ I), f.range = e.toAddMonoidHom.graph

Line test for monoid isomorphisms.

Let f : G → H × I be a homomorphism to a product of groups. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(h, i) | i : I} and every "horizontal line" {(h, i) | h : H} at most once. Then the image of f is the graph of some group isomorphism f' : H ≃ I.

theorem Subgroup.exists_eq_graph {H : Type u_2} {I : Type u_3} [Group H] [Group I] {G : Subgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) : ∃ (f : H →* I), G = f.graph

Vertical line test for group homomorphisms.

Let G ≤ H × I be a subgroup of a product of monoids. Assume that G maps bijectively to the first factor. Then G is the graph of some monoid homomorphism f : H → I.

theorem AddSubgroup.exists_eq_graph {H : Type u_2} {I : Type u_3} [AddGroup H] [AddGroup I] {G : AddSubgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) : ∃ (f : H →+ I), G = f.graph

Vertical line test for additive monoid homomorphisms.

Let G ≤ H × I be a submonoid of a product of monoids. Assume that G surjects onto the first factor and G intersects every "vertical line" {(h, i) | i : I} at most once. Then G is the graph of some monoid homomorphism f : H → I.

theorem Subgroup.exists_mulEquiv_eq_graph {H : Type u_2} {I : Type u_3} [Group H] [Group I] {G : Subgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) (hG₂ : Function.Bijective (Prod.snd ∘ ⇑G.subtype)) : ∃ (e : H ≃* I), G = e.toMonoidHom.graph

Goursat's lemma for monoid isomorphisms.

Let G ≤ H × I be a submonoid of a product of monoids. Assume that the natural maps from G to both factors are bijective. Then G is the graph of some isomorphism f : H ≃* I.

theorem AddSubgroup.exists_addEquiv_eq_graph {H : Type u_2} {I : Type u_3} [AddGroup H] [AddGroup I] {G : AddSubgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) (hG₂ : Function.Bijective (Prod.snd ∘ ⇑G.subtype)) : ∃ (e : H ≃+ I), G = e.toAddMonoidHom.graph

Goursat's lemma for additive monoid isomorphisms.

Let G ≤ H × I be a submonoid of a product of additive monoids. Assume that the natural maps from G to both factors are bijective. Then G is the graph of some isomorphism f : H ≃+ I.