Mathlib.Algebra.Group.Subgroup.Ker

MonoidHom.range definition

(f : G →* N) : Subgroup N

Full source

/-- The range of a monoid homomorphism from a group is a subgroup. -/
@[to_additive "The range of an `AddMonoidHom` from an `AddGroup` is an `AddSubgroup`."]
def range (f : G →* N) : Subgroup N :=
  Subgroup.copy ((⊤ : Subgroup G).map f) (Set.range f) (by simp [Set.ext_iff])

Range of a group homomorphism

Informal description

Given a group homomorphism $ f \colon G \to N $, the range of $ f $ is the subgroup of $ N $ consisting of all elements $ y \in N $ such that there exists an $ x \in G $ with $ f(x) = y $.

MonoidHom.coe_range theorem

(f : G →* N) : (f.range : Set N) = Set.range f

Full source

@[to_additive (attr := simp)]
theorem coe_range (f : G →* N) : (f.range : Set N) = Set.range f :=
  rfl

Range of a Group Homomorphism as a Set

Informal description

For any group homomorphism $f \colon G \to N$, the underlying set of the range subgroup of $f$ is equal to the range of $f$ as a function, i.e., $\{y \in N \mid \exists x \in G, f(x) = y\}$.

MonoidHom.mem_range theorem

{f : G →* N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y

Full source

@[to_additive (attr := simp)]
theorem mem_range {f : G →* N} {y : N} : y ∈ f.rangey ∈ f.range ↔ ∃ x, f x = y :=
  Iff.rfl

Characterization of Elements in the Range of a Group Homomorphism

Informal description

Let $f \colon G \to N$ be a group homomorphism. For any element $y \in N$, $y$ belongs to the range of $f$ if and only if there exists an element $x \in G$ such that $f(x) = y$.

MonoidHom.range_eq_map theorem

(f : G →* N) : f.range = (⊤ : Subgroup G).map f

Full source

@[to_additive]
theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f := by ext; simp

Range of a Group Homomorphism as Image of the Entire Group

Informal description

For any group homomorphism $f \colon G \to N$, the range of $f$ is equal to the image of the entire group $G$ (considered as the top subgroup $\top$) under $f$.

MonoidHom.range_isMulCommutative instance

{G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) : IsMulCommutative f.range

Full source

@[to_additive]
instance range_isMulCommutative {G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) :
    IsMulCommutative f.range :=
  range_eq_map f ▸ Subgroup.map_isMulCommutative ⊤ f

Commutativity of the Range of a Group Homomorphism from a Commutative Group

Informal description

For any commutative group $G$, group $N$, and group homomorphism $f \colon G \to N$, the range of $f$ is a commutative subgroup of $N$.

MonoidHom.restrict_range theorem

(f : G →* N) : (f.restrict K).range = K.map f

Full source

@[to_additive (attr := simp)]
theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by
  simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]

Range of Restricted Homomorphism Equals Image of Subgroup

Informal description

Let $G$ and $N$ be groups, $f \colon G \to N$ a group homomorphism, and $K$ a subgroup of $G$. Then the range of the restriction of $f$ to $K$ is equal to the image of $K$ under $f$, i.e., $$ \text{range}(f|_K) = f(K). $$

MonoidHom.rangeRestrict definition

(f : G →* N) : G →* f.range

Full source

/-- The canonical surjective group homomorphism `G →* f(G)` induced by a group
homomorphism `G →* N`. -/
@[to_additive
      "The canonical surjective `AddGroup` homomorphism `G →+ f(G)` induced by a group
      homomorphism `G →+ N`."]
def rangeRestrict (f : G →* N) : G →* f.range :=
  codRestrict f _ fun x => ⟨x, rfl⟩

Restriction of a group homomorphism to its range

Informal description

Given a group homomorphism $ f \colon G \to N $, the function `MonoidHom.rangeRestrict` restricts the codomain of $ f $ to its range $ f(G) $, yielding a group homomorphism $ G \to f(G) $. This is defined by mapping each $ g \in G $ to $ \langle f(g), \text{proof that } f(g) \in f(G) \rangle $, preserving the group structure (identity, multiplication, and inverses).

MonoidHom.coe_rangeRestrict theorem

(f : G →* N) (g : G) : (f.rangeRestrict g : N) = f g

Full source

@[to_additive (attr := simp)]
theorem coe_rangeRestrict (f : G →* N) (g : G) : (f.rangeRestrict g : N) = f g :=
  rfl

Range-Restricted Homomorphism Preserves Images

Informal description

For any group homomorphism $f \colon G \to N$ and any element $g \in G$, the image of $g$ under the range-restricted homomorphism $f.\text{rangeRestrict}$ (when viewed as an element of $N$) equals $f(g)$. In other words, the following diagram commutes: $$(f.\text{rangeRestrict}(g) : N) = f(g).$$

MonoidHom.coe_comp_rangeRestrict theorem

(f : G →* N) : ((↑) : f.range → N) ∘ (⇑f.rangeRestrict : G → f.range) = f

Full source

@[to_additive]
theorem coe_comp_rangeRestrict (f : G →* N) :
    ((↑) : f.range → N) ∘ (⇑f.rangeRestrict : G → f.range) = f :=
  rfl

Composition of Range Restriction and Inclusion Equals Original Homomorphism

Informal description

For any group homomorphism $f \colon G \to N$, the composition of the inclusion map from the range of $f$ to $N$ with the range restriction of $f$ equals $f$ itself. In other words, if $\iota \colon f(G) \hookrightarrow N$ is the inclusion map and $\tilde{f} \colon G \to f(G)$ is the range restriction of $f$, then $\iota \circ \tilde{f} = f$.

MonoidHom.subtype_comp_rangeRestrict theorem

(f : G →* N) : f.range.subtype.comp f.rangeRestrict = f

Full source

@[to_additive]
theorem subtype_comp_rangeRestrict (f : G →* N) : f.range.subtype.comp f.rangeRestrict = f :=
  ext <| f.coe_rangeRestrict

Composition of Subgroup Inclusion with Range-Restricted Homomorphism Equals Original Homomorphism

Informal description

For any group homomorphism $f \colon G \to N$, the composition of the inclusion homomorphism of the range of $f$ (as a subgroup of $N$) with the range-restricted homomorphism of $f$ equals $f$ itself. In symbols: $$f.\text{range}.\text{subtype} \circ f.\text{rangeRestrict} = f.$$

MonoidHom.rangeRestrict_surjective theorem

(f : G →* N) : Function.Surjective f.rangeRestrict

Full source

@[to_additive]
theorem rangeRestrict_surjective (f : G →* N) : Function.Surjective f.rangeRestrict :=
  fun ⟨_, g, rfl⟩ => ⟨g, rfl⟩

Surjectivity of the Range-Restricted Group Homomorphism

Informal description

For any group homomorphism $f \colon G \to N$, the restricted homomorphism $f_{\text{range}} \colon G \to f(G)$ is surjective, where $f(G)$ denotes the range of $f$ as a subgroup of $N$.

MonoidHom.rangeRestrict_injective_iff theorem

{f : G →* N} : Injective f.rangeRestrict ↔ Injective f

Full source

@[to_additive (attr := simp)]
lemma rangeRestrict_injective_iff {f : G →* N} : InjectiveInjective f.rangeRestrict ↔ Injective f := by
  convert Set.injective_codRestrict _

Injectivity of Range-Restricted Homomorphism $\leftrightarrow$ Injectivity of Original Homomorphism

Informal description

For a group homomorphism $f \colon G \to N$, the restriction of $f$ to its range, $f_{\text{range}} \colon G \to f(G)$, is injective if and only if $f$ is injective.

MonoidHom.map_range theorem

(g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range

Full source

@[to_additive]
theorem map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range := by
  rw [range_eq_map, range_eq_map]; exact (⊤ : Subgroup G).map_map g f

Image of Range under Composition Equals Range of Composition for Group Homomorphisms

Informal description

Let $G$, $N$, and $P$ be groups, and let $f \colon G \to N$ and $g \colon N \to P$ be group homomorphisms. Then the image of the range of $f$ under $g$ is equal to the range of the composition $g \circ f$. In symbols: $$g(f(G)) = (g \circ f)(G).$$

MonoidHom.range_comp theorem

(g : N →* P) (f : G →* N) : (g.comp f).range = f.range.map g

Full source

@[to_additive]
lemma range_comp (g : N →* P) (f : G →* N) : (g.comp f).range = f.range.map g := (map_range ..).symm

Range of Composition Equals Image of Range under Homomorphism

Informal description

Let $G$, $N$, and $P$ be groups, and let $f \colon G \to N$ and $g \colon N \to P$ be group homomorphisms. Then the range of the composition $g \circ f$ is equal to the image of the range of $f$ under $g$. In symbols: $$(g \circ f)(G) = g(f(G)).$$

MonoidHom.range_eq_top theorem

{N} [Group N] {f : G →* N} : f.range = (⊤ : Subgroup N) ↔ Function.Surjective f

Full source

@[to_additive]
theorem range_eq_top {N} [Group N] {f : G →* N} :
    f.range = (⊤ : Subgroup N) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ

Range Equals Full Group iff Homomorphism is Surjective

Informal description

For a group homomorphism $f \colon G \to N$ between groups $G$ and $N$, the range of $f$ is equal to the entire group $N$ (i.e., $f.range = \top$) if and only if $f$ is surjective.

MonoidHom.range_eq_top_of_surjective theorem

{N} [Group N] (f : G →* N) (hf : Function.Surjective f) : f.range = (⊤ : Subgroup N)

Full source

/-- The range of a surjective monoid homomorphism is the whole of the codomain. -/
@[to_additive (attr := simp)
  "The range of a surjective `AddMonoid` homomorphism is the whole of the codomain."]
theorem range_eq_top_of_surjective {N} [Group N] (f : G →* N) (hf : Function.Surjective f) :
    f.range = (⊤ : Subgroup N) :=
  range_eq_top.2 hf

Range of Surjective Group Homomorphism is Full Group

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a surjective group homomorphism. Then the range of $f$ is equal to the entire group $N$.

MonoidHom.range_one theorem

: (1 : G →* N).range = ⊥

Full source

@[to_additive (attr := simp)]
theorem range_one : (1 : G →* N).range = ⊥ :=
  SetLike.ext fun x => by simpa using @comm _ (· = ·) _ 1 x

Range of Trivial Homomorphism is Trivial Subgroup

Informal description

The range of the trivial group homomorphism $1 \colon G \to N$ (which sends every element of $G$ to the identity element of $N$) is the trivial subgroup $\{1\}$ of $N$.

Subgroup.range_subtype theorem

(H : Subgroup G) : H.subtype.range = H

Full source

@[to_additive (attr := simp)]
theorem _root_.Subgroup.range_subtype (H : Subgroup G) : H.subtype.range = H :=
  SetLike.coe_injective <| (coe_range _).trans <| Subtype.range_coe

Range of Subgroup Inclusion Equals Subgroup

Informal description

For any subgroup $H$ of a group $G$, the range of the inclusion homomorphism $H \hookrightarrow G$ is equal to $H$ itself.

Subgroup.inclusion_range theorem

{H K : Subgroup G} (h_le : H ≤ K) : (inclusion h_le).range = H.subgroupOf K

Full source

@[to_additive (attr := simp)]
theorem _root_.Subgroup.inclusion_range {H K : Subgroup G} (h_le : H ≤ K) :
    (inclusion h_le).range = H.subgroupOf K :=
  Subgroup.ext fun g => Set.ext_iff.mp (Set.range_inclusion h_le) g

Range of Subgroup Inclusion Equals Intersection as Subgroup of Larger Subgroup

Informal description

Let $G$ be a group and $H, K$ be subgroups of $G$ such that $H \leq K$. Then the range of the inclusion homomorphism $\text{inclusion}(h_\text{le}) : H \to K$ is equal to the subgroup $H \cap K$ viewed as a subgroup of $K$.

MonoidHom.subgroupOf_range_eq_of_le theorem

 {G₁ G₂ : Type*} [Group G₁] [Group G₂] {K : Subgroup G₂} (f : G₁ →* G₂) (h : f.range ≤ K) :
  f.range.subgroupOf K = (f.codRestrict K fun x => h ⟨x, rfl⟩).range

Full source

@[to_additive]
theorem subgroupOf_range_eq_of_le {G₁ G₂ : Type*} [Group G₁] [Group G₂] {K : Subgroup G₂}
    (f : G₁ →* G₂) (h : f.range ≤ K) :
    f.range.subgroupOf K = (f.codRestrict K fun x => h ⟨x, rfl⟩).range := by
  ext k
  refine exists_congr ?_
  simp [Subtype.ext_iff]

Range of Codomain-Restricted Homomorphism Equals Intersection with Subgroup

Informal description

Let $G_1$ and $G_2$ be groups, and let $K$ be a subgroup of $G_2$. Given a group homomorphism $f \colon G_1 \to G_2$ such that the range of $f$ is contained in $K$, the subgroup of $K$ obtained by intersecting $K$ with the range of $f$ is equal to the range of the codomain-restricted homomorphism $f \colon G_1 \to K$.

MonoidHom.ofLeftInverse definition

{f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) : G ≃* f.range

Full source

/-- Computable alternative to `MonoidHom.ofInjective`. -/
@[to_additive "Computable alternative to `AddMonoidHom.ofInjective`."]
def ofLeftInverse {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) : G ≃* f.range :=
  { f.rangeRestrict with
    toFun := f.rangeRestrict
    invFun := g ∘ f.range.subtype
    left_inv := h
    right_inv := by
      rintro ⟨x, y, rfl⟩
      apply Subtype.ext
      rw [coe_rangeRestrict, Function.comp_apply, Subgroup.coe_subtype, Subtype.coe_mk, h] }

Multiplicative equivalence induced by a left-invertible group homomorphism

Informal description

Given group homomorphisms $ f \colon G \to N $ and $ g \colon N \to G $ such that $ g $ is a left inverse of $ f $ (i.e., $ g(f(x)) = x $ for all $ x \in G $), the function `MonoidHom.ofLeftInverse` constructs a multiplicative equivalence (isomorphism) between $ G $ and the range of $ f $. Specifically, it defines a bijection $ G \cong f(G) $ where: - The forward map is the restriction of $ f $ to its range (i.e., $ f \colon G \to f(G) $). - The inverse map is the composition of $ g $ with the inclusion $ f(G) \hookrightarrow N $. This equivalence preserves the group structure, meaning it respects multiplication, identity, and inverses.

MonoidHom.ofLeftInverse_apply theorem

{f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : G) : ↑(ofLeftInverse h x) = f x

Full source

@[to_additive (attr := simp)]
theorem ofLeftInverse_apply {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : G) :
    ↑(ofLeftInverse h x) = f x :=
  rfl

Image under left-inverse-induced isomorphism equals original homomorphism value

Informal description

Let $f \colon G \to N$ and $g \colon N \to G$ be group homomorphisms such that $g$ is a left inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in G$). Then for any $x \in G$, the image of $x$ under the isomorphism $\text{ofLeftInverse}\ h \colon G \cong f.\text{range}$ equals $f(x)$.

MonoidHom.ofLeftInverse_symm_apply theorem

{f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : f.range) : (ofLeftInverse h).symm x = g x

Full source

@[to_additive (attr := simp)]
theorem ofLeftInverse_symm_apply {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f)
    (x : f.range) : (ofLeftInverse h).symm x = g x :=
  rfl

Inverse of left-inverse-induced isomorphism equals restriction of left inverse

Informal description

Let $f \colon G \to N$ and $g \colon N \to G$ be group homomorphisms such that $g$ is a left inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in G$). For any element $x$ in the range of $f$, the inverse of the isomorphism $\text{ofLeftInverse}\, h$ maps $x$ to $g(x)$. In other words, the inverse of the isomorphism $G \cong f(G)$ induced by $f$ and $g$ is given by the restriction of $g$ to the range of $f$.

MonoidHom.ofInjective definition

{f : G →* N} (hf : Function.Injective f) : G ≃* f.range

Full source

/-- The range of an injective group homomorphism is isomorphic to its domain. -/
@[to_additive "The range of an injective additive group homomorphism is isomorphic to its
domain."]
noncomputable def ofInjective {f : G →* N} (hf : Function.Injective f) : G ≃* f.range :=
  MulEquiv.ofBijective (f.codRestrict f.range fun x => ⟨x, rfl⟩)
    ⟨fun _ _ h => hf (Subtype.ext_iff.mp h), by
      rintro ⟨x, y, rfl⟩
      exact ⟨y, rfl⟩⟩

Isomorphism between domain and range of an injective group homomorphism

Informal description

Given an injective group homomorphism $ f \colon G \to N $, the function `MonoidHom.ofInjective` constructs a multiplicative isomorphism $ G \simeq^* \text{range}(f) $ between $ G $ and the range of $ f $. This isomorphism maps each $ x \in G $ to $ f(x) $ in the range of $ f $, and its inverse maps each $ y $ in the range of $ f $ to the unique $ x \in G $ such that $ f(x) = y $.

MonoidHom.ofInjective_apply theorem

{f : G →* N} (hf : Function.Injective f) {x : G} : ↑(ofInjective hf x) = f x

Full source

@[to_additive]
theorem ofInjective_apply {f : G →* N} (hf : Function.Injective f) {x : G} :
    ↑(ofInjective hf x) = f x :=
  rfl

Image under injective homomorphism isomorphism equals original image

Informal description

Let $f \colon G \to N$ be an injective group homomorphism. For any $x \in G$, the image of $x$ under the isomorphism $\text{ofInjective}\, hf \colon G \simeq^* \text{range}(f)$ is equal to $f(x)$ when viewed as an element of $N$.

MonoidHom.apply_ofInjective_symm theorem

{f : G →* N} (hf : Function.Injective f) (x : f.range) : f ((ofInjective hf).symm x) = x

Full source

@[to_additive (attr := simp)]
theorem apply_ofInjective_symm {f : G →* N} (hf : Function.Injective f) (x : f.range) :
    f ((ofInjective hf).symm x) = x :=
  Subtype.ext_iff.1 <| (ofInjective hf).apply_symm_apply x

Inverse Image Recovery under Injective Group Homomorphism: $f(f^{-1}(x)) = x$

Informal description

Let $f \colon G \to N$ be an injective group homomorphism. For any element $x$ in the range of $f$, applying $f$ to the inverse image of $x$ under the isomorphism $G \simeq^* \text{range}(f)$ recovers $x$, i.e., $f((f^{-1})(x)) = x$.

MonoidHom.coe_toAdditive_range theorem

(f : G →* G') : (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range

Full source

@[simp]
theorem coe_toAdditive_range (f : G →* G') :
    (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range := rfl

Range Preservation under Monoid-to-Additive Conversion: $\text{range}(\text{toAdditive}\, f) = \text{toAddSubgroup}(\text{range}\, f)$

Informal description

For any group homomorphism $f \colon G \to G'$, the range of the additive version of $f$ (denoted $\text{toAdditive}\, f$) is equal to the additive subgroup corresponding to the range of $f$ under the canonical order isomorphism between subgroups and additive subgroups.

MonoidHom.coe_toMultiplicative_range theorem

 {A A' : Type*} [AddGroup A] [AddGroup A'] (f : A →+ A') :
  (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range

Full source

@[simp]
theorem coe_toMultiplicative_range {A A' : Type*} [AddGroup A] [AddGroup A'] (f : A →+ A') :
    (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range := rfl

Range Conversion between Additive and Multiplicative Group Homomorphisms

Informal description

Let $A$ and $A'$ be additive groups, and let $f : A \to A'$ be an additive group homomorphism. Then the range of the multiplicative group homomorphism obtained by converting $f$ (via `AddMonoidHom.toMultiplicative`) is equal to the multiplicative subgroup obtained by converting the range of $f$ (via `AddSubgroup.toSubgroup`). In other words, the following equality holds: $$(\text{toMultiplicative } f).\text{range} = \text{toSubgroup } (f.\text{range})$$

MonoidHom.ker definition

(f : G →* M) : Subgroup G

Full source

/-- The multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that
`f x = 1` -/
@[to_additive
      "The additive kernel of an `AddMonoid` homomorphism is the `AddSubgroup` of elements
      such that `f x = 0`"]
def ker (f : G →* M) : Subgroup G :=
  { MonoidHom.mker f with
    inv_mem' := fun {x} (hx : f x = 1) =>
      calc
        f x⁻¹ = f x * f x⁻¹ := by rw [hx, one_mul]
        _ = 1 := by rw [← map_mul, mul_inv_cancel, map_one] }

Kernel of a group homomorphism

Informal description

The kernel of a group homomorphism $ f \colon G \to M $ is the subgroup of $ G $ consisting of all elements $ x \in G $ such that $ f(x) = 1 $, where $ 1 $ is the identity element of $ M $.

MonoidHom.ker_toSubmonoid theorem

(f : G →* M) : f.ker.toSubmonoid = MonoidHom.mker f

Full source

@[to_additive (attr := simp)]
theorem ker_toSubmonoid (f : G →* M) : f.ker.toSubmonoid = MonoidHom.mker f := rfl

Kernel as Submonoid Equals Monoid Kernel

Informal description

For any group homomorphism $f \colon G \to M$, the underlying submonoid of the kernel of $f$ is equal to the kernel of $f$ when viewed as a monoid homomorphism. In other words, $(\ker f)_{\text{submonoid}} = \text{mker} f$.

MonoidHom.mem_ker theorem

{f : G →* M} {x : G} : x ∈ f.ker ↔ f x = 1

Full source

@[to_additive (attr := simp)]
theorem mem_ker {f : G →* M} {x : G} : x ∈ f.kerx ∈ f.ker ↔ f x = 1 :=
  Iff.rfl

Characterization of Kernel Membership via Group Homomorphism Evaluation

Informal description

For a group homomorphism $f \colon G \to M$ and an element $x \in G$, $x$ belongs to the kernel of $f$ if and only if $f(x) = 1$, where $1$ is the identity element of $M$.

MonoidHom.div_mem_ker_iff theorem

(f : G →* N) {x y : G} : x / y ∈ ker f ↔ f x = f y

Full source

@[to_additive]
theorem div_mem_ker_iff (f : G →* N) {x y : G} : x / y ∈ ker fx / y ∈ ker f ↔ f x = f y := by
  rw [mem_ker, map_div, div_eq_one]

Quotient in Kernel iff Images Are Equal: $x / y \in \ker f \leftrightarrow f(x) = f(y)$

Informal description

For any group homomorphism $f \colon G \to N$ and any elements $x, y \in G$, the quotient $x / y$ belongs to the kernel of $f$ if and only if $f(x) = f(y)$.

MonoidHom.coe_ker theorem

(f : G →* M) : (f.ker : Set G) = (f : G → M) ⁻¹' { 1 }

Full source

@[to_additive]
theorem coe_ker (f : G →* M) : (f.ker : Set G) = (f : G → M) ⁻¹' {1} :=
  rfl

Kernel as Preimage of Identity

Informal description

For a group homomorphism $f \colon G \to M$, the underlying set of the kernel of $f$ is equal to the preimage of the singleton set $\{1\}$ under $f$, i.e., $\ker(f) = f^{-1}(\{1\})$.

MonoidHom.ker_toHomUnits theorem

{M} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker

Full source

@[to_additive (attr := simp)]
theorem ker_toHomUnits {M} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker := by
  ext x
  simp [mem_ker, Units.ext_iff]

Kernel Equality for Lifted Homomorphism to Units

Informal description

For any monoid $M$ and group $G$, given a group homomorphism $f \colon G \to M$, the kernel of the lifted homomorphism $f \colon G \to M^\times$ (where $M^\times$ is the group of units of $M$) is equal to the kernel of $f$.

MonoidHom.decidableMemKer instance

[DecidableEq M] (f : G →* M) : DecidablePred (· ∈ f.ker)

Full source

@[to_additive]
instance decidableMemKer [DecidableEq M] (f : G →* M) : DecidablePred (· ∈ f.ker) := fun x =>
  decidable_of_iff (f x = 1) f.mem_ker

Decidability of Kernel Membership for Group Homomorphisms

Informal description

For any group homomorphism $f \colon G \to M$ with $M$ having decidable equality, membership in the kernel of $f$ is decidable. That is, there is an algorithm to determine whether a given element $x \in G$ satisfies $f(x) = 1$.

MonoidHom.comap_ker theorem

{P : Type*} [MulOneClass P] (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker

Full source

@[to_additive]
theorem comap_ker {P : Type*} [MulOneClass P] (g : N →* P) (f : G →* N) :
    g.ker.comap f = (g.comp f).ker :=
  rfl

Kernel of Composition Equals Preimage of Kernel

Informal description

Let $G$, $N$, and $P$ be groups, and let $f \colon G \to N$ and $g \colon N \to P$ be group homomorphisms. Then the preimage of the kernel of $g$ under $f$ is equal to the kernel of the composition $g \circ f$, i.e., \[ f^{-1}(\ker g) = \ker (g \circ f). \]

MonoidHom.comap_bot theorem

(f : G →* N) : (⊥ : Subgroup N).comap f = f.ker

Full source

@[to_additive (attr := simp)]
theorem comap_bot (f : G →* N) : (⊥ : Subgroup N).comap f = f.ker :=
  rfl

Preimage of Trivial Subgroup Equals Kernel of Homomorphism

Informal description

For any group homomorphism $f \colon G \to N$, the preimage of the trivial subgroup $\{1\}$ under $f$ is equal to the kernel of $f$. In other words, $f^{-1}(\{1\}) = \ker f$.

MonoidHom.ker_restrict theorem

(f : G →* N) : (f.restrict K).ker = f.ker.subgroupOf K

Full source

@[to_additive (attr := simp)]
theorem ker_restrict (f : G →* N) : (f.restrict K).ker = f.ker.subgroupOf K :=
  rfl

Kernel of Restricted Homomorphism Equals Kernel Intersection

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any subgroup $K$ of $G$, the kernel of the restriction of $f$ to $K$ is equal to the intersection of the kernel of $f$ with $K$, viewed as a subgroup of $K$. In other words, \[ \ker(f|_K) = \ker f \cap K. \]

MonoidHom.ker_codRestrict theorem

{S} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S) (h : ∀ x, f x ∈ s) : (f.codRestrict s h).ker = f.ker

Full source

@[to_additive (attr := simp)]
theorem ker_codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S)
    (h : ∀ x, f x ∈ s) : (f.codRestrict s h).ker = f.ker :=
  SetLike.ext fun _x => Subtype.ext_iff

Kernel Preservation under Codomain Restriction of Group Homomorphism

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any subgroup $s$ of $N$ such that $f(x) \in s$ for all $x \in G$, the kernel of the codomain-restricted homomorphism $f \colon G \to s$ is equal to the kernel of $f$.

MonoidHom.ker_rangeRestrict theorem

(f : G →* N) : ker (rangeRestrict f) = ker f

Full source

@[to_additive (attr := simp)]
theorem ker_rangeRestrict (f : G →* N) : ker (rangeRestrict f) = ker f :=
  ker_codRestrict _ _ _

Kernel Equality for Range-Restricted Group Homomorphism

Informal description

For any group homomorphism $f \colon G \to N$, the kernel of the restriction of $f$ to its range is equal to the kernel of $f$. In other words, \[ \ker(f|_{f(G)}) = \ker f. \]

MonoidHom.ker_one theorem

: (1 : G →* M).ker = ⊤

Full source

@[to_additive (attr := simp)]
theorem ker_one : (1 : G →* M).ker = ⊤ :=
  SetLike.ext fun _x => eq_self_iff_true _

Kernel of Trivial Homomorphism is the Whole Group

Informal description

The kernel of the trivial group homomorphism $1 \colon G \to M$ (which sends every element of $G$ to the identity element of $M$) is equal to the entire group $G$.

MonoidHom.ker_id theorem

: (MonoidHom.id G).ker = ⊥

Full source

@[to_additive (attr := simp)]
theorem ker_id : (MonoidHom.id G).ker = ⊥ :=
  rfl

Kernel of the Identity Homomorphism is Trivial

Informal description

The kernel of the identity homomorphism $\mathrm{id} \colon G \to G$ is the trivial subgroup $\{1\}$ of $G$.

MonoidHom.ker_eq_bot_iff theorem

(f : G →* M) : f.ker = ⊥ ↔ Function.Injective f

Full source

@[to_additive]
theorem ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ Function.Injective f :=
  ⟨fun h x y hxy => by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy, fun h =>
    bot_unique fun _ hx => h (hx.trans f.map_one.symm)⟩

Kernel Triviality and Injectivity of Group Homomorphisms: $\ker f = \{1\} \leftrightarrow f \text{ injective}$

Informal description

For a group homomorphism $f \colon G \to M$, the kernel of $f$ is the trivial subgroup $\{1\}$ if and only if $f$ is injective.

Subgroup.ker_subtype theorem

(H : Subgroup G) : H.subtype.ker = ⊥

Full source

@[to_additive (attr := simp)]
theorem _root_.Subgroup.ker_subtype (H : Subgroup G) : H.subtype.ker = ⊥ :=
  H.subtype.ker_eq_bot_iff.mpr Subtype.coe_injective

Kernel of Subgroup Inclusion is Trivial: $\ker(\text{subtype}) = \{1\}$

Informal description

For any subgroup $H$ of a group $G$, the kernel of the inclusion homomorphism $H \hookrightarrow G$ is the trivial subgroup $\{1\}$ of $H$.

Subgroup.ker_inclusion theorem

{H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥

Full source

@[to_additive (attr := simp)]
theorem _root_.Subgroup.ker_inclusion {H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥ :=
  (inclusion h).ker_eq_bot_iff.mpr (Set.inclusion_injective h)

Trivial Kernel of Subgroup Inclusion Homomorphism

Informal description

For any subgroups $H$ and $K$ of a group $G$ such that $H \leq K$, the kernel of the inclusion homomorphism $\text{inclusion}(h) : H \to K$ is the trivial subgroup $\{1\}$.

MonoidHom.ker_prod theorem

{M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) : (f.prod g).ker = f.ker ⊓ g.ker

Full source

@[to_additive ker_prod]
theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
    (f.prod g).ker = f.ker ⊓ g.ker :=
  SetLike.ext fun _ => Prod.mk_eq_one

Kernel of Product Homomorphism Equals Intersection of Kernels

Informal description

Let $G$, $M$, and $N$ be groups (or more generally, types with a multiplicative identity and multiplication operation). For any group homomorphisms $f \colon G \to M$ and $g \colon G \to N$, the kernel of the product homomorphism $f \times g \colon G \to M \times N$ (defined by $(f \times g)(x) = (f(x), g(x))$) is equal to the intersection of the kernels of $f$ and $g$. In symbols: \[ \ker(f \times g) = \ker f \cap \ker g. \]

MonoidHom.range_le_ker_iff theorem

(f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1

Full source

@[to_additive]
theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 :=
  ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y⟩

Range-Kernel Criterion for Composition of Group Homomorphisms

Informal description

Let $G, G', G''$ be groups, and let $f \colon G \to G'$ and $g \colon G' \to G''$ be group homomorphisms. The range of $f$ is contained in the kernel of $g$ if and only if the composition $g \circ f$ is the trivial homomorphism (i.e., the homomorphism that sends every element to the identity element of $G''$). In symbols: \[ \text{range}(f) \leq \ker(g) \iff g \circ f = 1. \]

MonoidHom.normal_ker instance

(f : G →* M) : f.ker.Normal

Full source

@[to_additive]
instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
  ⟨fun x hx y => by
    rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]⟩

Normality of the Kernel of a Group Homomorphism

Informal description

For any group homomorphism $f \colon G \to M$, the kernel of $f$ is a normal subgroup of $G$.

MonoidHom.coe_toAdditive_ker theorem

(f : G →* G') : (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker

Full source

@[simp]
theorem coe_toAdditive_ker (f : G →* G') :
    (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker := rfl

Kernel Correspondence Between Multiplicative and Additive Homomorphisms

Informal description

For any group homomorphism $f \colon G \to G'$, the kernel of the corresponding additive homomorphism $\text{toAdditive}(f)$ is equal to the additive subgroup obtained by applying $\text{toAddSubgroup}$ to the kernel of $f$.

MonoidHom.coe_toMultiplicative_ker theorem

 {A A' : Type*} [AddGroup A] [AddZeroClass A'] (f : A →+ A') :
  (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker

Full source

@[simp]
theorem coe_toMultiplicative_ker {A A' : Type*} [AddGroup A] [AddZeroClass A'] (f : A →+ A') :
    (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker := rfl

Equality of Kernels under Additive-to-Multiplicative Conversion

Informal description

For any additive group $A$ and additive monoid $A'$, given an additive group homomorphism $f \colon A \to A'$, the kernel of the multiplicative version of $f$ (obtained via `toMultiplicative`) is equal to the additive kernel of $f$ converted to a multiplicative subgroup.

MonoidHom.eqLocus definition

(f g : G →* M) : Subgroup G

Full source

/-- The subgroup of elements `x : G` such that `f x = g x` -/
@[to_additive "The additive subgroup of elements `x : G` such that `f x = g x`"]
def eqLocus (f g : G →* M) : Subgroup G :=
  { eqLocusM f g with inv_mem' := eq_on_inv f g }

Equalizer subgroup of group homomorphisms

Informal description

Given two group homomorphisms $ f, g \colon G \to M $, the subgroup $\text{eqLocus}(f, g)$ consists of all elements $ x \in G $ such that $ f(x) = g(x) $. This subgroup contains the identity element (since $ f(1) = g(1) $), is closed under multiplication (if $ f(x) = g(x) $ and $ f(y) = g(y) $, then $ f(xy) = g(xy) $), and is closed under taking inverses (if $ f(x) = g(x) $, then $ f(x^{-1}) = g(x^{-1}) $).

MonoidHom.eqLocus_same theorem

(f : G →* N) : f.eqLocus f = ⊤

Full source

@[to_additive (attr := simp)]
theorem eqLocus_same (f : G →* N) : f.eqLocus f = ⊤ :=
  SetLike.ext fun _ => eq_self_iff_true _

Equalizer subgroup of a homomorphism with itself is the whole group

Informal description

For any group homomorphism $f \colon G \to N$, the equalizer subgroup $\text{eqLocus}(f, f)$ (consisting of all elements $x \in G$ such that $f(x) = f(x)$) is equal to the entire group $G$.

MonoidHom.eqOn_closure theorem

{f g : G →* M} {s : Set G} (h : Set.EqOn f g s) : Set.EqOn f g (closure s)

Full source

/-- If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure. -/
@[to_additive
      "If two monoid homomorphisms are equal on a set, then they are equal on its subgroup
      closure."]
theorem eqOn_closure {f g : G →* M} {s : Set G} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocus g from (closure_le _).2 h

Agreement of Homomorphisms on Generated Subgroup

Informal description

Let $G$ and $M$ be groups, and let $f, g \colon G \to M$ be group homomorphisms. If $f$ and $g$ agree on a subset $s \subseteq G$, then they also agree on the subgroup generated by $s$.

Subgroup.map_eq_bot_iff theorem

{f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker

Full source

@[to_additive]
theorem map_eq_bot_iff {f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker :=
  (gc_map_comap f).l_eq_bot

Image of Subgroup is Trivial if and only if Subgroup is Contained in Kernel

Informal description

For a group homomorphism $f \colon G \to N$ and a subgroup $H$ of $G$, the image of $H$ under $f$ is the trivial subgroup if and only if $H$ is contained in the kernel of $f$. In other words, $f(H) = \{1\}$ if and only if $H \leq \ker f$.

Subgroup.map_eq_bot_iff_of_injective theorem

{f : G →* N} (hf : Function.Injective f) : H.map f = ⊥ ↔ H = ⊥

Full source

@[to_additive]
theorem map_eq_bot_iff_of_injective {f : G →* N} (hf : Function.Injective f) :
    H.map f = ⊥ ↔ H = ⊥ := by rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]

Triviality of Subgroup Image under Injective Homomorphism: $f(H) = \{1\} \leftrightarrow H = \{1\}$

Informal description

For a group homomorphism $f \colon G \to N$ that is injective, the image of a subgroup $H$ of $G$ under $f$ is the trivial subgroup if and only if $H$ itself is the trivial subgroup. In other words, $f(H) = \{1\}$ if and only if $H = \{1\}$.

Subgroup.map_le_range theorem

(H : Subgroup G) : map f H ≤ f.range

Full source

@[to_additive]
theorem map_le_range (H : Subgroup G) : map f H ≤ f.range :=
  (range_eq_map f).symm ▸ map_mono le_top

Image of Subgroup under Homomorphism is Contained in Range

Informal description

For any subgroup $H$ of a group $G$ and any group homomorphism $f \colon G \to N$, the image of $H$ under $f$ is contained in the range of $f$. In other words, $f(H) \leq \text{range}(f)$.

Subgroup.map_subtype_le theorem

{H : Subgroup G} (K : Subgroup H) : K.map H.subtype ≤ H

Full source

@[to_additive]
theorem map_subtype_le {H : Subgroup G} (K : Subgroup H) : K.map H.subtype ≤ H :=
  (K.map_le_range H.subtype).trans_eq H.range_subtype

Image of Subgroup Under Inclusion is Contained in Original Subgroup

Informal description

For any subgroup $H$ of a group $G$ and any subgroup $K$ of $H$, the image of $K$ under the inclusion homomorphism $H \hookrightarrow G$ is contained in $H$. In other words, if we consider $K$ as a subgroup of $G$ via the inclusion map, we have $K \leq H$.

Subgroup.ker_le_comap theorem

(H : Subgroup N) : f.ker ≤ comap f H

Full source

@[to_additive]
theorem ker_le_comap (H : Subgroup N) : f.ker ≤ comap f H :=
  comap_bot f ▸ comap_mono bot_le

Kernel is Contained in Preimage of Subgroup

Informal description

For any group homomorphism $f \colon G \to N$ and any subgroup $H$ of $N$, the kernel of $f$ is contained in the preimage of $H$ under $f$, i.e., $\ker f \leq f^{-1}(H)$.

Subgroup.map_comap_eq theorem

(H : Subgroup N) : map f (comap f H) = f.range ⊓ H

Full source

@[to_additive]
theorem map_comap_eq (H : Subgroup N) : map f (comap f H) = f.range ⊓ H :=
  SetLike.ext' <| by
    rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]

Image of Preimage Subgroup Equals Range Intersection: $f(f^{-1}(H)) = \mathrm{range}(f) \cap H$

Informal description

For any group homomorphism $f \colon G \to N$ and any subgroup $H$ of $N$, the image of the preimage of $H$ under $f$ is equal to the intersection of the range of $f$ with $H$. That is, $$ f(f^{-1}(H)) = \mathrm{range}(f) \cap H. $$

Subgroup.comap_map_eq theorem

(H : Subgroup G) : comap f (map f H) = H ⊔ f.ker

Full source

@[to_additive]
theorem comap_map_eq (H : Subgroup G) : comap f (map f H) = H ⊔ f.ker := by
  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))
  intro x hx; simp only [exists_prop, mem_map, mem_comap] at hx
  rcases hx with ⟨y, hy, hy'⟩
  rw [← mul_inv_cancel_left y x]
  exact mul_mem_sup hy (by simp [mem_ker, hy'])

Preimage of Image Subgroup Equals Join with Kernel: $f^{-1}(f(H)) = H \sqcup \ker f$

Informal description

For any group homomorphism $f \colon G \to N$ and any subgroup $H$ of $G$, the preimage of the image of $H$ under $f$ is equal to the join of $H$ and the kernel of $f$, i.e., $$ f^{-1}(f(H)) = H \sqcup \ker f. $$

Subgroup.map_comap_eq_self theorem

{f : G →* N} {H : Subgroup N} (h : H ≤ f.range) : map f (comap f H) = H

Full source

@[to_additive]
theorem map_comap_eq_self {f : G →* N} {H : Subgroup N} (h : H ≤ f.range) :
    map f (comap f H) = H := by
  rwa [map_comap_eq, inf_eq_right]

Image of Preimage Equals Subgroup When Contained in Range: $f(f^{-1}(H)) = H$ for $H \leq \mathrm{range}(f)$

Informal description

Let $f \colon G \to N$ be a group homomorphism and $H$ be a subgroup of $N$ such that $H$ is contained in the range of $f$. Then the image under $f$ of the preimage of $H$ equals $H$ itself, i.e., $$ f(f^{-1}(H)) = H. $$

Subgroup.map_comap_eq_self_of_surjective theorem

{f : G →* N} (h : Function.Surjective f) (H : Subgroup N) : map f (comap f H) = H

Full source

@[to_additive]
theorem map_comap_eq_self_of_surjective {f : G →* N} (h : Function.Surjective f) (H : Subgroup N) :
    map f (comap f H) = H :=
  map_comap_eq_self (range_eq_top.2 h ▸ le_top)

Image of Preimage Equals Subgroup for Surjective Homomorphisms: $f(f^{-1}(H)) = H$

Informal description

Let $f \colon G \to N$ be a surjective group homomorphism and $H$ be a subgroup of $N$. Then the image under $f$ of the preimage of $H$ equals $H$ itself, i.e., $$ f(f^{-1}(H)) = H. $$

Subgroup.comap_le_comap_of_le_range theorem

{f : G →* N} {K L : Subgroup N} (hf : K ≤ f.range) : K.comap f ≤ L.comap f ↔ K ≤ L

Full source

@[to_additive]
theorem comap_le_comap_of_le_range {f : G →* N} {K L : Subgroup N} (hf : K ≤ f.range) :
    K.comap f ≤ L.comap f ↔ K ≤ L :=
  ⟨(map_comap_eq_self hf).ge.trans ∘ map_le_iff_le_comap.mpr, comap_mono⟩

Preimage Subgroup Inclusion Equivalence under Range Condition: $f^{-1}(K) \leq f^{-1}(L) \leftrightarrow K \leq L$ for $K \leq \mathrm{range}(f)$

Informal description

Let $f \colon G \to N$ be a group homomorphism and $K, L$ be subgroups of $N$ such that $K$ is contained in the range of $f$. Then the preimage of $K$ under $f$ is contained in the preimage of $L$ under $f$ if and only if $K$ is contained in $L$. In symbols: \[ f^{-1}(K) \leq f^{-1}(L) \leftrightarrow K \leq L. \]

Subgroup.comap_le_comap_of_surjective theorem

{f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) : K.comap f ≤ L.comap f ↔ K ≤ L

Full source

@[to_additive]
theorem comap_le_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
    K.comap f ≤ L.comap f ↔ K ≤ L :=
  comap_le_comap_of_le_range (range_eq_top.2 hf ▸ le_top)

Preimage Subgroup Inclusion Equivalence for Surjective Homomorphisms: $f^{-1}(K) \leq f^{-1}(L) \leftrightarrow K \leq L$

Informal description

Let $f \colon G \to N$ be a surjective group homomorphism, and let $K$ and $L$ be subgroups of $N$. Then the preimage of $K$ under $f$ is contained in the preimage of $L$ under $f$ if and only if $K$ is contained in $L$. In symbols: $$ f^{-1}(K) \leq f^{-1}(L) \leftrightarrow K \leq L. $$

Subgroup.comap_lt_comap_of_surjective theorem

{f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) : K.comap f < L.comap f ↔ K < L

Full source

@[to_additive]
theorem comap_lt_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
    K.comap f < L.comap f ↔ K < L := by simp_rw [lt_iff_le_not_le, comap_le_comap_of_surjective hf]

Strict Preimage Subgroup Inclusion Equivalence for Surjective Homomorphisms: $f^{-1}(K) \subsetneq f^{-1}(L) \leftrightarrow K \subsetneq L$

Informal description

Let $f \colon G \to N$ be a surjective group homomorphism, and let $K$ and $L$ be subgroups of $N$. Then the preimage of $K$ under $f$ is strictly contained in the preimage of $L$ under $f$ if and only if $K$ is strictly contained in $L$. In symbols: $$ f^{-1}(K) \subsetneq f^{-1}(L) \leftrightarrow K \subsetneq L. $$

Subgroup.comap_injective theorem

{f : G →* N} (h : Function.Surjective f) : Function.Injective (comap f)

Full source

@[to_additive]
theorem comap_injective {f : G →* N} (h : Function.Surjective f) : Function.Injective (comap f) :=
  fun K L => by simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]

Injectivity of Subgroup Preimage Map for Surjective Homomorphisms

Informal description

Let $f \colon G \to N$ be a surjective group homomorphism. Then the preimage map $\mathrm{comap}\, f \colon \mathrm{Subgroup}\, N \to \mathrm{Subgroup}\, G$ is injective. In other words, for any two subgroups $K, L \leq N$, if $f^{-1}(K) = f^{-1}(L)$, then $K = L$.

Subgroup.comap_map_eq_self theorem

{f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) : comap f (map f H) = H

Full source

@[to_additive]
theorem comap_map_eq_self {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) :
    comap f (map f H) = H := by
  rwa [comap_map_eq, sup_eq_left]

Preimage of Image Subgroup Equals Original Subgroup When Kernel is Contained

Informal description

Let $f \colon G \to N$ be a group homomorphism and $H$ a subgroup of $G$. If the kernel of $f$ is contained in $H$, then the preimage of the image of $H$ under $f$ equals $H$, i.e., $$ f^{-1}(f(H)) = H. $$

Subgroup.comap_map_eq_self_of_injective theorem

{f : G →* N} (h : Function.Injective f) (H : Subgroup G) : comap f (map f H) = H

Full source

@[to_additive]
theorem comap_map_eq_self_of_injective {f : G →* N} (h : Function.Injective f) (H : Subgroup G) :
    comap f (map f H) = H :=
  comap_map_eq_self (((ker_eq_bot_iff _).mpr h).symm ▸ bot_le)

Preimage of Image Subgroup Equals Original Subgroup for Injective Homomorphisms

Informal description

Let $f \colon G \to N$ be an injective group homomorphism and $H$ a subgroup of $G$. Then the preimage of the image of $H$ under $f$ equals $H$, i.e., $$ f^{-1}(f(H)) = H. $$

Subgroup.map_le_map_iff theorem

{f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ≤ K ⊔ f.ker

Full source

@[to_additive]
theorem map_le_map_iff {f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ≤ K ⊔ f.ker := by
  rw [map_le_iff_le_comap, comap_map_eq]

Image Containment Criterion for Group Homomorphisms: $f(H) \leq f(K) \leftrightarrow H \leq K \sqcup \ker f$

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any subgroups $H$ and $K$ of $G$, the image of $H$ under $f$ is contained in the image of $K$ under $f$ if and only if $H$ is contained in the join of $K$ and the kernel of $f$. In symbols: \[ f(H) \leq f(K) \leftrightarrow H \leq K \sqcup \ker f. \]

Subgroup.map_le_map_iff' theorem

{f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ⊔ f.ker ≤ K ⊔ f.ker

Full source

@[to_additive]
theorem map_le_map_iff' {f : G →* N} {H K : Subgroup G} :
    H.map f ≤ K.map f ↔ H ⊔ f.ker ≤ K ⊔ f.ker := by
  simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]

Image Containment Criterion for Group Homomorphisms via Kernel Joins

Informal description

Let $G$ and $N$ be groups, and $f \colon G \to N$ be a group homomorphism. For any subgroups $H, K$ of $G$, the following are equivalent: 1. The image of $H$ under $f$ is contained in the image of $K$ under $f$ (i.e., $f(H) \leq f(K)$) 2. The join of $H$ with the kernel of $f$ is contained in the join of $K$ with the kernel of $f$ (i.e., $H \sqcup \ker f \leq K \sqcup \ker f$)

Subgroup.map_eq_map_iff theorem

{f : G →* N} {H K : Subgroup G} : H.map f = K.map f ↔ H ⊔ f.ker = K ⊔ f.ker

Full source

@[to_additive]
theorem map_eq_map_iff {f : G →* N} {H K : Subgroup G} :
    H.map f = K.map f ↔ H ⊔ f.ker = K ⊔ f.ker := by simp only [le_antisymm_iff, map_le_map_iff']

Equality of Subgroup Images via Kernel-Adjusted Joins

Informal description

Let $f \colon G \to N$ be a group homomorphism, and let $H$ and $K$ be subgroups of $G$. Then the images of $H$ and $K$ under $f$ are equal if and only if the joins of $H$ and $\ker f$ and of $K$ and $\ker f$ are equal, i.e., \[ f(H) = f(K) \leftrightarrow H \sqcup \ker f = K \sqcup \ker f. \]

Subgroup.map_eq_range_iff theorem

{f : G →* N} {H : Subgroup G} : H.map f = f.range ↔ Codisjoint H f.ker

Full source

@[to_additive]
theorem map_eq_range_iff {f : G →* N} {H : Subgroup G} :
    H.map f = f.range ↔ Codisjoint H f.ker := by
  rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]

Image Equals Range Criterion: $f(H) = \text{range}(f) \leftrightarrow H \sqcup \ker f = G$

Informal description

Let $f \colon G \to N$ be a group homomorphism and $H$ be a subgroup of $G$. The image of $H$ under $f$ equals the range of $f$ if and only if $H$ and the kernel of $f$ are codisjoint, i.e., $H \sqcup \ker f = \top$ (where $\top$ is the full group $G$).

Subgroup.map_le_map_iff_of_injective theorem

{f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ≤ K

Full source

@[to_additive]
theorem map_le_map_iff_of_injective {f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} :
    H.map f ≤ K.map f ↔ H ≤ K := by rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]

Image Subgroup Inclusion Criterion for Injective Homomorphisms

Informal description

Let $f \colon G \to N$ be an injective group homomorphism, and let $H$ and $K$ be subgroups of $G$. Then the image of $H$ under $f$ is contained in the image of $K$ under $f$ if and only if $H$ is contained in $K$. In symbols: \[ f(H) \leq f(K) \leftrightarrow H \leq K. \]

Subgroup.map_subtype_le_map_subtype theorem

{G' : Subgroup G} {H K : Subgroup G'} : H.map G'.subtype ≤ K.map G'.subtype ↔ H ≤ K

Full source

@[to_additive (attr := simp)]
theorem map_subtype_le_map_subtype {G' : Subgroup G} {H K : Subgroup G'} :
    H.map G'.subtype ≤ K.map G'.subtype ↔ H ≤ K :=
  map_le_map_iff_of_injective G'.subtype_injective

Subgroup Image Inclusion Criterion under Subgroup Inclusion Homomorphism

Informal description

Let $G'$ be a subgroup of a group $G$, and let $H$ and $K$ be subgroups of $G'$. Then the image of $H$ under the inclusion homomorphism $G' \hookrightarrow G$ is contained in the image of $K$ under the same homomorphism if and only if $H$ is contained in $K$. In symbols: \[ \text{incl}(H) \leq \text{incl}(K) \leftrightarrow H \leq K. \]

Subgroup.map_lt_map_iff_of_injective theorem

{f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} : H.map f < K.map f ↔ H < K

Full source

@[to_additive]
theorem map_lt_map_iff_of_injective {f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} :
    H.map f < K.map f ↔ H < K :=
  lt_iff_lt_of_le_iff_le' (map_le_map_iff_of_injective hf) (map_le_map_iff_of_injective hf)

Strict Image Subgroup Inclusion Criterion for Injective Homomorphisms

Informal description

Let $f \colon G \to N$ be an injective group homomorphism, and let $H$ and $K$ be subgroups of $G$. Then the image of $H$ under $f$ is strictly contained in the image of $K$ under $f$ if and only if $H$ is strictly contained in $K$. In symbols: \[ f(H) \subsetneq f(K) \leftrightarrow H \subsetneq K. \]

Subgroup.map_subtype_lt_map_subtype theorem

{G' : Subgroup G} {H K : Subgroup G'} : H.map G'.subtype < K.map G'.subtype ↔ H < K

Full source

@[to_additive (attr := simp)]
theorem map_subtype_lt_map_subtype {G' : Subgroup G} {H K : Subgroup G'} :
    H.map G'.subtype < K.map G'.subtype ↔ H < K :=
  map_lt_map_iff_of_injective G'.subtype_injective

Strict Subgroup Image Inclusion Criterion under Subgroup Inclusion Homomorphism

Informal description

Let $G'$ be a subgroup of a group $G$, and let $H$ and $K$ be subgroups of $G'$. Then the image of $H$ under the inclusion homomorphism $G' \hookrightarrow G$ is strictly contained in the image of $K$ under the same homomorphism if and only if $H$ is strictly contained in $K$. In symbols: \[ \text{incl}(H) \subsetneq \text{incl}(K) \leftrightarrow H \subsetneq K. \]

Subgroup.map_injective theorem

{f : G →* N} (h : Function.Injective f) : Function.Injective (map f)

Full source

@[to_additive]
theorem map_injective {f : G →* N} (h : Function.Injective f) : Function.Injective (map f) :=
  Function.LeftInverse.injective <| comap_map_eq_self_of_injective h

Injectivity of Subgroup Map for Injective Homomorphisms

Informal description

Let $f \colon G \to N$ be an injective group homomorphism. Then the induced map on subgroups $H \mapsto f(H)$ is also injective. That is, for any subgroups $H, K$ of $G$, if $f(H) = f(K)$, then $H = K$.

Subgroup.map_injective_of_ker_le theorem

{H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : map f H = map f K) : H = K

Full source

/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`. -/
@[to_additive "Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`."]
theorem map_injective_of_ker_le {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K)
    (hf : map f H = map f K) : H = K := by
  apply_fun comap f at hf
  rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf

Injectivity of Subgroup Map under Kernel Containment: $f(H) = f(K) \Rightarrow H = K$ when $\ker f \leq H, K$

Informal description

Let $f \colon G \to N$ be a group homomorphism, and let $H$ and $K$ be subgroups of $G$ such that the kernel of $f$ is contained in both $H$ and $K$. If the images of $H$ and $K$ under $f$ are equal, then $H = K$.

Subgroup.ker_subgroupMap theorem

: (f.subgroupMap H).ker = f.ker.subgroupOf H

Full source

@[to_additive]
theorem ker_subgroupMap : (f.subgroupMap H).ker = f.ker.subgroupOf H :=
  ext fun _ ↦ Subtype.ext_iff

Kernel of Restricted Homomorphism Equals Kernel Intersection

Informal description

Let $G$ and $N$ be groups, $f \colon G \to N$ a group homomorphism, and $H$ a subgroup of $G$. Then the kernel of the restricted homomorphism $f|_{H} \colon H \to N$ is equal to the intersection of the kernel of $f$ with $H$, i.e., $\ker(f|_{H}) = \ker(f) \cap H$.

Subgroup.closure_preimage_eq_top theorem

(s : Set G) : closure ((closure s).subtype ⁻¹' s) = ⊤

Full source

@[to_additive]
theorem closure_preimage_eq_top (s : Set G) : closure ((closure s).subtype ⁻¹' s) = ⊤ := by
  apply map_injective (closure s).subtype_injective
  rw [MonoidHom.map_closure, ← MonoidHom.range_eq_map, range_subtype,
    Set.image_preimage_eq_of_subset]
  rw [coe_subtype, Subtype.range_coe_subtype]
  exact subset_closure

Generated Subgroup of Preimage under Inclusion is Entire Group

Informal description

For any subset $s$ of a group $G$, the subgroup generated by the preimage of $s$ under the inclusion homomorphism of the subgroup generated by $s$ is the entire group $G$. In other words: \[ \langle (\langle s \rangle \hookrightarrow G)^{-1}(s) \rangle = G \]

Subgroup.comap_sup_eq_of_le_range theorem

{H K : Subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) : comap f H ⊔ comap f K = comap f (H ⊔ K)

Full source

@[to_additive]
theorem comap_sup_eq_of_le_range {H K : Subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) :
    comapcomap f H ⊔ comap f K = comap f (H ⊔ K) :=
  map_injective_of_ker_le f ((ker_le_comap f H).trans le_sup_left) (ker_le_comap f (H ⊔ K))
    (by
      rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)])

Preimage of Subgroup Join under Group Homomorphism with Range Condition: $f^{-1}(H) \sqcup f^{-1}(K) = f^{-1}(H \sqcup K)$ when $H, K \subseteq \mathrm{range}(f)$

Informal description

Let $f \colon G \to N$ be a group homomorphism, and let $H$ and $K$ be subgroups of $N$ such that $H$ and $K$ are contained in the range of $f$. Then the supremum of the preimages of $H$ and $K$ under $f$ is equal to the preimage of the supremum of $H$ and $K$: $$ f^{-1}(H) \sqcup f^{-1}(K) = f^{-1}(H \sqcup K). $$

Subgroup.comap_sup_eq theorem

(H K : Subgroup N) (hf : Function.Surjective f) : comap f H ⊔ comap f K = comap f (H ⊔ K)

Full source

@[to_additive]
theorem comap_sup_eq (H K : Subgroup N) (hf : Function.Surjective f) :
    comapcomap f H ⊔ comap f K = comap f (H ⊔ K) :=
  comap_sup_eq_of_le_range f (range_eq_top.2 hf ▸ le_top) (range_eq_top.2 hf ▸ le_top)

Preimage of Subgroup Join under Surjective Group Homomorphism: $f^{-1}(H) \sqcup f^{-1}(K) = f^{-1}(H \sqcup K)$

Informal description

Let $f \colon G \to N$ be a surjective group homomorphism, and let $H$ and $K$ be subgroups of $N$. Then the supremum of the preimages of $H$ and $K$ under $f$ is equal to the preimage of the supremum of $H$ and $K$: $$ f^{-1}(H) \sqcup f^{-1}(K) = f^{-1}(H \sqcup K). $$

Subgroup.sup_subgroupOf_eq theorem

{H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) : H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L

Full source

@[to_additive]
theorem sup_subgroupOf_eq {H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) :
    H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L :=
  comap_sup_eq_of_le_range L.subtype (hH.trans_eq L.range_subtype.symm)
     (hK.trans_eq L.range_subtype.symm)

Join of Subgroups Relative to a Larger Subgroup: $H \sqcup_L K = (H \sqcup_G K) \cap L$ when $H, K \leq L$

Informal description

Let $G$ be a group and $H$, $K$, $L$ be subgroups of $G$ such that $H \leq L$ and $K \leq L$. Then the join of $H$ and $K$ as subgroups of $L$ is equal to the intersection of the join $H \sqcup K$ (as subgroups of $G$) with $L$: $$ H \sqcup_L K = (H \sqcup_G K) \cap L. $$

Subgroup.codisjoint_subgroupOf_sup theorem

(H K : Subgroup G) : Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Full source

@[to_additive]
theorem codisjoint_subgroupOf_sup (H K : Subgroup G) :
    Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K)) := by
  rw [codisjoint_iff, sup_subgroupOf_eq, subgroupOf_self]
  exacts [le_sup_left, le_sup_right]

Codisjointness of Subgroup Intersections in Join: $H \cap (H \sqcup K)$ and $K \cap (H \sqcup K)$ are codisjoint in $H \sqcup K$

Informal description

For any subgroups $H$ and $K$ of a group $G$, the subgroups $H \cap (H \sqcup K)$ and $K \cap (H \sqcup K)$ (viewed as subgroups of $H \sqcup K$) are codisjoint in the lattice of subgroups of $H \sqcup K$. That is, their join is the entire group $H \sqcup K$.

Subgroup.subgroupOf_sup theorem

(A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) : (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Full source

@[to_additive]
theorem subgroupOf_sup (A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
    (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B := by
  refine
    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
  simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]
  rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]

Subgroup Intersection Distributes Over Join: $(A \sqcup A') \cap B = (A \cap B) \sqcup (A' \cap B)$ when $A, A' \leq B$

Informal description

Let $G$ be a group and let $A$, $A'$, and $B$ be subgroups of $G$ such that $A \leq B$ and $A' \leq B$. Then the intersection of the join $A \sqcup A'$ with $B$ (viewed as a subgroup of $B$) is equal to the join of the intersections $A \cap B$ and $A' \cap B$ (both viewed as subgroups of $B$). In other words, $$ (A \sqcup A') \cap B = (A \cap B) \sqcup (A' \cap B) $$ as subgroups of $B$.

Mathlib.Algebra.Group.Subgroup.Ker

Main definitions

Implementation notes

Tags