Prove2Me

Proposition 11.1.4 — Basic properties of group homomorphisms

Proved
AATA.homomorphism_properties_11_1_4

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

group-theoryisomorphism-theoremsquotient-groups

Let G,HG,H be groups and let f:G→Hf:G\to H be a group homomorphism. Then

f(1)=1,f(g−1)=f(g)−1(g∈G).f(1)=1,\qquad f(g^{-1})=f(g)^{-1}\quad(g\in G).

For every subgroup K≤GK\le G, the image f(K)f(K) is a subgroup of HH. For every subgroup L≤HL\le H, the inverse image f−1(L)f^{-1}(L) is a subgroup of GG; if LL is normal in HH, then f−1(L)f^{-1}(L) is normal in GG.

These are the four clauses of Judson’s Proposition 11.1.4, kept together as one statement. They provide the subgroup constructions needed to compare groups through a homomorphism.

Formalization Note. Images and inverse images are represented by bundled subgroups, with their carrier sets explicitly equated to the corresponding set-theoretic images and inverse images. No surjectivity assumption is made.

Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
import Mathlib.Tactic

set_option autoImplicit false
set_option maxHeartbeats 200000
universe u v
Formal statement
namespace AATA
theorem homomorphism_properties_11_1_4 {G : Type u} {H : Type v} [Group G] [Group H] (f : G →* H) :
    f 1 = 1 ∧
    (∀ g : G, f g⁻¹ = (f g)⁻¹) ∧
    (∀ K : Subgroup G, ∃ L : Subgroup H, (L : Set H) = f '' (K : Set G)) ∧
    (∀ L : Subgroup H, ∃ K : Subgroup G,
      (K : Set G) = f ⁻¹' (L : Set H) ∧ (L.Normal → K.Normal)) := by sorry
end AATA
Source
Thomas W. Judson, Abstract Algebra: Theory and Applications, author-hosted HTML edition dated August 4, 2026, Proposition 11.1.4, https://judsonbooks.org/aata-files/aata-html/homomorph-section-group-homomorphisms.html
Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

For arbitrary universe levels uu and vv, arbitrary types GG in universe uu and HH in universe vv, specified group structures on GG and HH, and any group homomorphism f:G→Hf:G\to H (a function already assumed to preserve multiplication and the identity), all four following assertions hold together: f(1G)=1Hf(1_G)=1_H; for every g∈Gg\in G, f(g−1)=f(g)−1f(g^{-1})=f(g)^{-1}; for every subgroup KK of GG, there exists a subgroup LL of HH whose underlying set is exactly {f(k):k∈K}\{f(k):k\in K\}; and for every subgroup LL of HH, there exists a subgroup KK of GG whose underlying set is exactly {g∈G:f(g)∈L}\{g\in G:f(g)\in L\} and such that, if LL is normal in HH, then that same KK is normal in GG. Normality means that every conjugate hℓh−1h\ell h^{-1} of an element ℓ∈L\ell\in L by an element h∈Hh\in H belongs to LL, and correspondingly every gkg−1gkg^{-1} belongs to KK when k∈Kk\in K and g∈Gg\in G. The subgroup variables in the image clause and the inverse-image clause are quantified separately; the existential claims are existence claims, without an explicit uniqueness quantifier. When LL is not normal, the normality implication in the inverse-image clause is vacuous, while the asserted inverse-image subgroup still exists. No normality assertion is made for the image subgroup. Neither group is assumed commutative, finite, or nontrivial, and ff is not assumed injective or surjective; trivial groups and the homomorphism taking every element to 1H1_H are included. Groups and subgroups contain an identity, so empty underlying groups or empty subgroups are excluded by their structures.

Actual model identifier: unavailable in this runtime.

Human review

View graph