Mathlib.Algebra.Group.Graph

Module docstring

{"# 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.) "}

MonoidHom.mgraph definition

(f : G →* H) : Submonoid (G × H)

Full source

/-- The graph of a monoid homomorphism as a submonoid.

See also `MonoidHom.graph` for the graph as a subgroup. -/
@[to_additive
"The graph of a monoid homomorphism as a submonoid.

See also `AddMonoidHom.graph` for the graph as a subgroup."]
def mgraph (f : G →* H) : Submonoid (G × H) where
  carrier := {x | f x.1 = x.2}
  one_mem' := map_one f
  mul_mem' {x y} := by simp +contextual

Graph of a monoid homomorphism as a submonoid

Informal description

For a monoid homomorphism $f \colon G \to H$, the submonoid $\text{mgraph}(f)$ of $G \times H$ consists of all pairs $(g, h)$ such that $f(g) = h$. This submonoid contains the identity element $(1, 1)$ since $f(1) = 1$, and is closed under multiplication: if $(g_1, h_1), (g_2, h_2) \in \text{mgraph}(f)$, then $(g_1g_2, h_1h_2) \in \text{mgraph}(f)$ because $f(g_1g_2) = f(g_1)f(g_2) = h_1h_2$.

MonoidHom.mem_mgraph theorem

{f : G →* H} {x : G × H} : x ∈ f.mgraph ↔ f x.1 = x.2

Full source

@[to_additive (attr := simp)]
lemma mem_mgraph {f : G →* H} {x : G × H} : x ∈ f.mgraphx ∈ f.mgraph ↔ f x.1 = x.2 := .rfl

Membership in Graph of a Monoid Homomorphism

Informal description

For a monoid homomorphism $f \colon G \to H$ and an element $x = (g, h) \in G \times H$, we have $x \in \text{mgraph}(f)$ if and only if $f(g) = h$.

MonoidHom.mgraph_eq_mrange_prod theorem

(f : G →* H) : f.mgraph = mrange ((id _).prod f)

Full source

@[to_additive mgraph_eq_mrange_prod]
lemma mgraph_eq_mrange_prod (f : G →* H) : f.mgraph = mrange ((id _).prod f) := by aesop

Graph of a Monoid Homomorphism as Range of Product Homomorphism

Informal description

For any monoid homomorphism $f \colon G \to H$, the graph submonoid $\text{mgraph}(f)$ is equal to the range of the product homomorphism $(\text{id}_G, f) \colon G \to G \times H$.

MonoidHom.exists_mrange_eq_mgraph theorem

 {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
  ∃ f' : H →* I, mrange f = f'.mgraph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma exists_mrange_eq_mgraph {f : G →* H × I} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : H →* I, mrange f = f'.mgraph := by
  obtain ⟨f', hf'⟩ := exists_range_eq_graphOn_univ hf₁ hf
  simp only [Set.ext_iff, Set.mem_range, mem_graphOn, mem_univ, true_and, Prod.forall] at hf'
  use
  { toFun := f'
    map_one' := (hf' _ _).1 ⟨1, map_one _⟩
    map_mul' := by
      simp_rw [hf₁.forall]
      rintro g₁ g₂
      exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩ }
  simpa [SetLike.ext_iff] using hf'

Vertical Line Test for Monoid Homomorphisms: Existence of Graph Homomorphism

Informal description

Let $f \colon G \to H \times I$ be a monoid homomorphism to a product of monoids. Suppose that: 1. The composition $\pi_1 \circ f \colon G \to H$ (where $\pi_1$ is the first projection) is surjective. 2. For any $g_1, g_2 \in G$, if the first components satisfy $(f(g_1))_1 = (f(g_2))_1$, then the second components satisfy $(f(g_1))_2 = (f(g_2))_2$. Then there exists a monoid homomorphism $f' \colon H \to I$ such that the range of $f$ equals the graph of $f'$, i.e., $\text{mrange}(f) = \{(h, f'(h)) \mid h \in H\}$.

MonoidHom.exists_mulEquiv_mrange_eq_mgraph theorem

 {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f)) (hf₂ : Surjective (Prod.snd ∘ f))
  (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ e : H ≃* I, mrange f = e.toMonoidHom.mgraph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma exists_mulEquiv_mrange_eq_mgraph {f : G →* H × I} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf₂ : Surjective (Prod.sndProd.snd ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) :
    ∃ e : H ≃* I, mrange f = e.toMonoidHom.mgraph := by
  obtain ⟨e₁, he₁⟩ := f.exists_mrange_eq_mgraph hf₁ fun _ _ ↦ (hf _ _).1
  obtain ⟨e₂, he₂⟩ := (MulEquiv.prodComm.toMonoidHom.comp f).exists_mrange_eq_mgraph (by simpa) <|
    by simp [hf]
  have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [SetLike.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])
  exact ⟨
  { toFun := e₁
    map_mul' := e₁.map_mul'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

Vertical and Horizontal Line Test for Monoid Isomorphisms

Informal description

Let $f \colon G \to H \times I$ be a monoid homomorphism to a product of monoids. Suppose that: 1. The composition $\pi_1 \circ f \colon G \to H$ (where $\pi_1$ is the first projection) is surjective. 2. The composition $\pi_2 \circ f \colon G \to I$ (where $\pi_2$ is the second projection) is surjective. 3. For any $g_1, g_2 \in G$, the equality $(f(g_1))_1 = (f(g_2))_1$ holds if and only if $(f(g_1))_2 = (f(g_2))_2$. Then there exists a monoid isomorphism $e \colon H \simeq I$ such that the range of $f$ equals the graph of $e$, i.e., $\text{mrange}(f) = \{(h, e(h)) \mid h \in H\}$.

Submonoid.exists_eq_mgraph theorem

{G : Submonoid (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) : ∃ f : H →* I, G = f.mgraph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma Submonoid.exists_eq_mgraph {G : Submonoid (H × I)} (hG₁ : Bijective (Prod.fstProd.fst ∘ G.subtype)) :
    ∃ f : H →* I, G = f.mgraph := by
  simpa using MonoidHom.exists_mrange_eq_mgraph hG₁.surjective
    fun a b h ↦ congr_arg (Prod.sndProd.snd ∘ G.subtype) (hG₁.injective h)

Graph Characterization of Submonoids via Bijective Projection

Informal description

Let $G$ be a submonoid of the direct product $H \times I$ of two monoids. Suppose the projection map $\pi_1 \colon G \to H$ (restricted to $G$) is bijective. Then there exists a monoid homomorphism $f \colon H \to I$ such that $G$ is equal to the graph of $f$, i.e., $G = \{(h, f(h)) \mid h \in H\}$.

Submonoid.exists_mulEquiv_eq_mgraph theorem

 {G : Submonoid (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.snd ∘ G.subtype)) :
  ∃ e : H ≃* I, G = e.toMonoidHom.mgraph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma Submonoid.exists_mulEquiv_eq_mgraph {G : Submonoid (H × I)}
    (hG₁ : Bijective (Prod.fstProd.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.sndProd.snd ∘ G.subtype)) :
    ∃ e : H ≃* I, G = e.toMonoidHom.mgraph := by
  simpa using MonoidHom.exists_mulEquiv_mrange_eq_mgraph hG₁.surjective hG₂.surjective
    fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Goursat's Lemma for Monoid Isomorphisms via Bijective Projections

Informal description

Let $G$ be a submonoid of the direct product $H \times I$ of two monoids. Suppose the projection maps $\pi_1 \colon G \to H$ and $\pi_2 \colon G \to I$ (restricted to $G$) are both bijective. Then there exists a monoid isomorphism $e \colon H \simeq I$ such that $G$ is equal to the graph of $e$, i.e., $G = \{(h, e(h)) \mid h \in H\}$.

MonoidHom.graph definition

(f : G →* H) : Subgroup (G × H)

Full source

/-- The graph of a group homomorphism as a subgroup.

See also `MonoidHom.mgraph` for the graph as a submonoid. -/
@[to_additive
"The graph of a group homomorphism as a subgroup.

See also `AddMonoidHom.mgraph` for the graph as a submonoid."]
def graph (f : G →* H) : Subgroup (G × H) where
  toSubmonoid := f.mgraph
  inv_mem' {x} := by simp +contextual

Graph of a monoid homomorphism as a subgroup

Informal description

For a monoid homomorphism $f \colon G \to H$, the subgroup $\text{graph}(f)$ of $G \times H$ consists of all pairs $(g, h)$ such that $f(g) = h$. This subgroup contains the identity element $(1, 1)$ since $f(1) = 1$, is closed under multiplication, and is closed under inverses: if $(g, h) \in \text{graph}(f)$, then $(g^{-1}, h^{-1}) \in \text{graph}(f)$ because $f(g^{-1}) = f(g)^{-1} = h^{-1}$.

MonoidHom.mem_graph theorem

{f : G →* H} {x : G × H} : x ∈ f.graph ↔ f x.1 = x.2

Full source

@[to_additive]
lemma mem_graph {f : G →* H} {x : G × H} : x ∈ f.graphx ∈ f.graph ↔ f x.1 = x.2 := .rfl

Characterization of Graph Membership for Monoid Homomorphisms

Informal description

For a monoid homomorphism $f \colon G \to H$ and an element $x = (g, h) \in G \times H$, the pair $x$ belongs to the graph of $f$ if and only if $f(g) = h$.

MonoidHom.graph_eq_range_prod theorem

(f : G →* H) : f.graph = range ((id _).prod f)

Full source

@[to_additive graph_eq_range_prod]
lemma graph_eq_range_prod (f : G →* H) : f.graph = range ((id _).prod f) := by aesop

Graph of a Monoid Homomorphism as Range of Product Map

Informal description

For any monoid homomorphism $f \colon G \to H$, the graph of $f$ (as a subgroup of $G \times H$) is equal to the range of the product homomorphism $(\text{id}_G, f) \colon G \to G \times H$.

MonoidHom.exists_range_eq_graph theorem

 {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
  ∃ f' : H →* I, range f = f'.graph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma exists_range_eq_graph {f : G →* H × I} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : H →* I, range f = f'.graph := by
  simpa [SetLike.ext_iff] using exists_mrange_eq_mgraph hf₁ hf

Vertical Line Test for Monoid Homomorphisms: Existence of Graph Homomorphism

Informal description

Let $f \colon G \to H \times I$ be a monoid homomorphism to a product of monoids. Suppose that: 1. The composition $\pi_1 \circ f \colon G \to H$ (where $\pi_1$ is the first projection) is surjective. 2. For any $g_1, g_2 \in G$, if $(f(g_1))_1 = (f(g_2))_1$, then $(f(g_1))_2 = (f(g_2))_2$. Then there exists a monoid homomorphism $f' \colon H \to I$ such that the range of $f$ equals the graph of $f'$, i.e., $\text{range}(f) = \{(h, f'(h)) \mid h \in H\}$.

MonoidHom.exists_mulEquiv_range_eq_graph theorem

 {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f)) (hf₂ : Surjective (Prod.snd ∘ f))
  (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ e : H ≃* I, range f = e.toMonoidHom.graph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma exists_mulEquiv_range_eq_graph {f : G →* H × I} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf₂ : Surjective (Prod.sndProd.snd ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) :
    ∃ e : H ≃* I, range f = e.toMonoidHom.graph := by
  simpa [SetLike.ext_iff] using exists_mulEquiv_mrange_eq_mgraph hf₁ hf₂ hf

Vertical and Horizontal Line Test for Group Isomorphisms

Informal description

Let $f \colon G \to H \times I$ be a monoid homomorphism between groups. Suppose that: 1. The composition $\pi_1 \circ f \colon G \to H$ is surjective, 2. The composition $\pi_2 \circ f \colon G \to I$ is surjective, 3. For any $g_1, g_2 \in G$, $(f(g_1))_1 = (f(g_2))_1$ if and only if $(f(g_1))_2 = (f(g_2))_2$. Then there exists a group isomorphism $e \colon H \simeq I$ such that the range of $f$ equals the graph of $e$, i.e., $\text{range}(f) = \{(h, e(h)) \mid h \in H\}$.

Subgroup.exists_eq_graph theorem

{G : Subgroup (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) : ∃ f : H →* I, G = f.graph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma Subgroup.exists_eq_graph {G : Subgroup (H × I)} (hG₁ : Bijective (Prod.fstProd.fst ∘ G.subtype)) :
    ∃ f : H →* I, G = f.graph := by
  simpa [SetLike.ext_iff] using Submonoid.exists_eq_mgraph hG₁

Graph Characterization of Subgroups via Bijective Projection

Informal description

Let $G$ be a subgroup of the direct product $H \times I$ of two groups. If the projection map $\pi_1 \colon G \to H$ (restricted to $G$) is bijective, then there exists a group homomorphism $f \colon H \to I$ such that $G$ is equal to the graph of $f$, i.e., $G = \{(h, f(h)) \mid h \in H\}$.

Subgroup.exists_mulEquiv_eq_graph theorem

 {G : Subgroup (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.snd ∘ G.subtype)) :
  ∃ e : H ≃* I, G = e.toMonoidHom.graph

Full source

/-- **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`. -/
@[to_additive "**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`."]
lemma Subgroup.exists_mulEquiv_eq_graph {G : Subgroup (H × I)}
    (hG₁ : Bijective (Prod.fstProd.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.sndProd.snd ∘ G.subtype)) :
    ∃ e : H ≃* I, G = e.toMonoidHom.graph := by
  simpa [SetLike.ext_iff] using Submonoid.exists_mulEquiv_eq_mgraph hG₁ hG₂

Goursat's Lemma for Group Isomorphisms via Bijective Projections

Informal description

Let $G$ be a subgroup of the direct product $H \times I$ of two groups. If the projection maps $\pi_1 \colon G \to H$ and $\pi_2 \colon G \to I$ (restricted to $G$) are both bijective, then there exists a group isomorphism $e \colon H \simeq I$ such that $G$ is equal to the graph of $e$, i.e., $G = \{(h, e(h)) \mid h \in H\}$.