Mathlib.Algebra.Group.Subgroup.Map

Subgroup.comap definition

{N : Type*} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup G

Full source

/-- The preimage of a subgroup along a monoid homomorphism is a subgroup. -/
@[to_additive
      "The preimage of an `AddSubgroup` along an `AddMonoid` homomorphism
      is an `AddSubgroup`."]
def comap {N : Type*} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup G :=
  { H.toSubmonoid.comap f with
    carrier := f ⁻¹' H
    inv_mem' := fun {a} ha => show f a⁻¹ ∈ H by rw [f.map_inv]; exact H.inv_mem ha }

Preimage of a subgroup under a group homomorphism

Informal description

Given a group homomorphism $ f \colon G \to N $ and a subgroup $ H $ of $ N $, the preimage $ f^{-1}(H) $ forms a subgroup of $ G $. This subgroup consists of all elements $ x \in G $ such that $ f(x) \in H $, and it inherits the group structure from $ G $.

Subgroup.coe_comap theorem

(K : Subgroup N) (f : G →* N) : (K.comap f : Set G) = f ⁻¹' K

Full source

@[to_additive (attr := simp)]
theorem coe_comap (K : Subgroup N) (f : G →* N) : (K.comap f : Set G) = f ⁻¹' K :=
  rfl

Preimage Subgroup as Set Preimage

Informal description

For any subgroup $K$ of a group $N$ and any group homomorphism $f \colon G \to N$, the underlying set of the preimage subgroup $K.\text{comap}\, f$ is equal to the preimage of $K$ under $f$, i.e., $$(K.\text{comap}\, f) = f^{-1}(K).$$

Subgroup.mem_comap theorem

{K : Subgroup N} {f : G →* N} {x : G} : x ∈ K.comap f ↔ f x ∈ K

Full source

@[to_additive (attr := simp)]
theorem mem_comap {K : Subgroup N} {f : G →* N} {x : G} : x ∈ K.comap fx ∈ K.comap f ↔ f x ∈ K :=
  Iff.rfl

Characterization of Elements in the Preimage Subgroup

Informal description

Let $G$ and $N$ be groups, $f \colon G \to N$ a group homomorphism, and $K$ a subgroup of $N$. For any element $x \in G$, $x$ belongs to the preimage subgroup $K.\text{comap}\, f$ if and only if $f(x) \in K$.

Subgroup.comap_mono theorem

{f : G →* N} {K K' : Subgroup N} : K ≤ K' → comap f K ≤ comap f K'

Full source

@[to_additive]
theorem comap_mono {f : G →* N} {K K' : Subgroup N} : K ≤ K' → comap f K ≤ comap f K' :=
  preimage_mono

Monotonicity of Subgroup Preimage under Homomorphism

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any subgroups $K$ and $K'$ of $N$, if $K \leq K'$, then the preimage subgroup $f^{-1}(K)$ is contained in the preimage subgroup $f^{-1}(K')$, i.e., $f^{-1}(K) \leq f^{-1}(K')$.

Subgroup.comap_comap theorem

(K : Subgroup P) (g : N →* P) (f : G →* N) : (K.comap g).comap f = K.comap (g.comp f)

Full source

@[to_additive]
theorem comap_comap (K : Subgroup P) (g : N →* P) (f : G →* N) :
    (K.comap g).comap f = K.comap (g.comp f) :=
  rfl

Preimage of Subgroup under Composition of 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. For any subgroup $K$ of $P$, the preimage of the preimage of $K$ under $g$ and $f$ is equal to the preimage of $K$ under the composition $g \circ f$, i.e., $$(g^{-1}(K)) \cap f^{-1}(N) = (g \circ f)^{-1}(K).$$

Subgroup.comap_id theorem

(K : Subgroup N) : K.comap (MonoidHom.id _) = K

Full source

@[to_additive (attr := simp)]
theorem comap_id (K : Subgroup N) : K.comap (MonoidHom.id _) = K := by
  ext
  rfl

Preimage of Subgroup under Identity Homomorphism is Itself

Informal description

For any subgroup $K$ of a group $N$, the preimage of $K$ under the identity group homomorphism $\mathrm{id} \colon N \to N$ is equal to $K$ itself, i.e., $\mathrm{id}^{-1}(K) = K$.

Subgroup.toAddSubgroup_comap theorem

 {G₂ : Type*} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) :
  s.toAddSubgroup.comap (MonoidHom.toAdditive f) = Subgroup.toAddSubgroup (s.comap f)

Full source

@[simp]
theorem toAddSubgroup_comap {G₂ : Type*} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) :
    s.toAddSubgroup.comap (MonoidHom.toAdditive f) = Subgroup.toAddSubgroup (s.comap f) := rfl

Compatibility of Subgroup Preimages with Additive Conversion

Informal description

Let $G$ and $G_2$ be groups, $f \colon G \to G_2$ a group homomorphism, and $s$ a subgroup of $G_2$. Then the preimage of the additive subgroup corresponding to $s$ under the additive version of $f$ is equal to the additive subgroup corresponding to the preimage of $s$ under $f$.

AddSubgroup.toSubgroup_comap theorem

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

Full source

@[simp]
theorem _root_.AddSubgroup.toSubgroup_comap {A A₂ : Type*} [AddGroup A] [AddGroup A₂]
    (f : A →+ A₂) (s : AddSubgroup A₂) :
    s.toSubgroup.comap (AddMonoidHom.toMultiplicative f) = AddSubgroup.toSubgroup (s.comap f) := rfl

Compatibility of Preimage and Additive-Multiplicative Conversion for Subgroups

Informal description

Let $A$ and $A_2$ be additive groups, and let $f \colon A \to A_2$ be an additive group homomorphism. For any additive subgroup $s$ of $A_2$, the preimage of $s$ under $f$ in the multiplicative setting (via the conversion `AddMonoidHom.toMultiplicative`) is equal to the multiplicative subgroup obtained by converting the preimage of $s$ under $f$ in the additive setting (via `AddSubgroup.toSubgroup`). In other words, the following equality holds: \[ s.\text{toSubgroup}.\text{comap}(f.\text{toMultiplicative}) = (s.\text{comap}(f)).\text{toSubgroup} \]

Subgroup.map definition

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

Full source

/-- The image of a subgroup along a monoid homomorphism is a subgroup. -/
@[to_additive
      "The image of an `AddSubgroup` along an `AddMonoid` homomorphism
      is an `AddSubgroup`."]
def map (f : G →* N) (H : Subgroup G) : Subgroup N :=
  { H.toSubmonoid.map f with
    carrier := f '' H
    inv_mem' := by
      rintro _ ⟨x, hx, rfl⟩
      exact ⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩ }

Image of a subgroup under a group homomorphism

Informal description

Given a group homomorphism $ f \colon G \to N $ and a subgroup $ H $ of $ G $, the image of $ H $ under $ f $ is the subgroup of $ N $ consisting of all elements of the form $ f(x) $ for $ x \in H $.

Subgroup.coe_map theorem

(f : G →* N) (K : Subgroup G) : (K.map f : Set N) = f '' K

Full source

@[to_additive (attr := simp)]
theorem coe_map (f : G →* N) (K : Subgroup G) : (K.map f : Set N) = f '' K :=
  rfl

Image of Subgroup Under Homomorphism as Set Image

Informal description

For any group homomorphism $f \colon G \to N$ and any subgroup $K$ of $G$, the underlying set of the image subgroup $K.map f$ is equal to the image of the set $K$ under the function $f$, i.e., $(K.map f : \text{Set } N) = f '' K$.

Subgroup.map_toSubmonoid theorem

(f : G →* G') (K : Subgroup G) : (Subgroup.map f K).toSubmonoid = Submonoid.map f K.toSubmonoid

Full source

@[to_additive (attr := simp)]
theorem map_toSubmonoid (f : G →* G') (K : Subgroup G):
  (Subgroup.map f K).toSubmonoid = Submonoid.map f K.toSubmonoid := rfl

Image of Subgroup's Submonoid Under Homomorphism Equals Submonoid of Image Subgroup

Informal description

Let $G$ and $G'$ be groups, $f \colon G \to G'$ a group homomorphism, and $K$ a subgroup of $G$. Then the underlying submonoid of the image subgroup $f(K)$ is equal to the image of the underlying submonoid of $K$ under $f$. In other words, $(f(K))_{\text{monoid}} = f(K_{\text{monoid}})$.

Subgroup.mem_map theorem

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

Full source

@[to_additive (attr := simp)]
theorem mem_map {f : G →* N} {K : Subgroup G} {y : N} : y ∈ K.map fy ∈ K.map f ↔ ∃ x ∈ K, f x = y := Iff.rfl

Characterization of Elements in the Image of a Subgroup under a Group Homomorphism

Informal description

Let $G$ and $N$ be groups, $f \colon G \to N$ a group homomorphism, and $K$ a subgroup of $G$. For any element $y \in N$, we have $y \in f(K)$ if and only if there exists $x \in K$ such that $f(x) = y$.

Subgroup.mem_map_of_mem theorem

(f : G →* N) {K : Subgroup G} {x : G} (hx : x ∈ K) : f x ∈ K.map f

Full source

@[to_additive]
theorem mem_map_of_mem (f : G →* N) {K : Subgroup G} {x : G} (hx : x ∈ K) : f x ∈ K.map f :=
  mem_image_of_mem f hx

Image of Subgroup Element under Homomorphism Belongs to Image Subgroup

Informal description

Let $f \colon G \to N$ be a group homomorphism, $K$ a subgroup of $G$, and $x \in G$ an element such that $x \in K$. Then the image of $x$ under $f$ belongs to the image of $K$ under $f$, i.e., $f(x) \in f(K)$.

Subgroup.apply_coe_mem_map theorem

(f : G →* N) (K : Subgroup G) (x : K) : f x ∈ K.map f

Full source

@[to_additive]
theorem apply_coe_mem_map (f : G →* N) (K : Subgroup G) (x : K) : f x ∈ K.map f :=
  mem_map_of_mem f x.prop

Image of Subgroup Element under Homomorphism Belongs to Image Subgroup

Informal description

Let $f \colon G \to N$ be a group homomorphism, $K$ a subgroup of $G$, and $x$ an element of $K$ (viewed as an element of $G$ via the canonical inclusion). Then the image of $x$ under $f$ belongs to the image of $K$ under $f$, i.e., $f(x) \in f(K)$.

Subgroup.map_mono theorem

{f : G →* N} {K K' : Subgroup G} : K ≤ K' → map f K ≤ map f K'

Full source

@[to_additive]
theorem map_mono {f : G →* N} {K K' : Subgroup G} : K ≤ K' → map f K ≤ map f K' :=
  image_subset _

Monotonicity of Subgroup Image under Group Homomorphism

Informal description

Let $f \colon G \to N$ be a group homomorphism, and let $K$ and $K'$ be subgroups of $G$ such that $K \leq K'$. Then the image of $K$ under $f$ is a subgroup of the image of $K'$ under $f$, i.e., $f(K) \leq f(K')$.

Subgroup.map_id theorem

: K.map (MonoidHom.id G) = K

Full source

@[to_additive (attr := simp)]
theorem map_id : K.map (MonoidHom.id G) = K :=
  SetLike.coe_injective <| image_id _

Image of Subgroup under Identity Homomorphism is Itself

Informal description

For any subgroup $K$ of a group $G$, the image of $K$ under the identity group homomorphism $\mathrm{id} \colon G \to G$ is equal to $K$ itself, i.e., $\mathrm{id}(K) = K$.

Subgroup.map_map theorem

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

Full source

@[to_additive]
theorem map_map (g : N →* P) (f : G →* N) : (K.map f).map g = K.map (g.comp f) :=
  SetLike.coe_injective <| image_image _ _ _

Image of Subgroup under Composition of Homomorphisms Equals Composition of Images

Informal description

Let $G$, $N$, and $P$ be groups, and let $K$ be a subgroup of $G$. For any group homomorphisms $f \colon G \to N$ and $g \colon N \to P$, the image of $K$ under $g \circ f$ equals the image under $g$ of the image of $K$ under $f$. In symbols: $$g(f(K)) = (g \circ f)(K).$$

Subgroup.map_one_eq_bot theorem

: K.map (1 : G →* N) = ⊥

Full source

@[to_additive (attr := simp)]
theorem map_one_eq_bot : K.map (1 : G →* N) = ⊥ :=
  eq_bot_iff.mpr <| by
    rintro x ⟨y, _, rfl⟩
    simp

Image of Subgroup under Trivial Homomorphism is Trivial Subgroup

Informal description

For any subgroup $K$ of a group $G$, the image of $K$ under the trivial homomorphism $1 \colon G \to N$ (which sends every element to the identity of $N$) is the trivial subgroup $\bot$ of $N$.

Subgroup.mem_map_equiv theorem

{f : G ≃* N} {K : Subgroup G} {x : N} : x ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K

Full source

@[to_additive]
theorem mem_map_equiv {f : G ≃* N} {K : Subgroup G} {x : N} :
    x ∈ K.map f.toMonoidHomx ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K :=
  Set.mem_image_equiv

Characterization of Image Subgroup Membership via Isomorphism Inverse

Informal description

Let $G$ and $N$ be groups, $f \colon G \simeq^* N$ a multiplicative isomorphism, $K$ a subgroup of $G$, and $x$ an element of $N$. Then $x$ belongs to the image subgroup $f(K)$ if and only if $f^{-1}(x)$ belongs to $K$. In symbols: \[ x \in f(K) \leftrightarrow f^{-1}(x) \in K. \]

Subgroup.mem_map_iff_mem theorem

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

Full source

@[to_additive (attr := simp 1100, nolint simpNF)]
theorem mem_map_iff_mem {f : G →* N} (hf : Function.Injective f) {K : Subgroup G} {x : G} :
    f x ∈ K.map ff x ∈ K.map f ↔ x ∈ K :=
  hf.mem_set_image

Injectivity Criterion for Subgroup Membership under Homomorphism

Informal description

Let $f \colon G \to N$ be an injective group homomorphism, $K$ a subgroup of $G$, and $x$ an element of $G$. Then $f(x)$ belongs to the image subgroup $f(K)$ if and only if $x$ belongs to $K$. In symbols: \[ f(x) \in f(K) \leftrightarrow x \in K. \]

Subgroup.map_equiv_eq_comap_symm' theorem

(f : G ≃* N) (K : Subgroup G) : K.map f.toMonoidHom = K.comap f.symm.toMonoidHom

Full source

@[to_additive]
theorem map_equiv_eq_comap_symm' (f : G ≃* N) (K : Subgroup G) :
    K.map f.toMonoidHom = K.comap f.symm.toMonoidHom :=
  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)

Image-Preimage Duality for Subgroups under Group Isomorphism

Informal description

Let $f \colon G \simeq^* N$ be a multiplicative isomorphism between groups $G$ and $N$, and let $K$ be a subgroup of $G$. Then the image of $K$ under the group homomorphism $f$ is equal to the preimage of $K$ under the inverse isomorphism $f^{-1}$. In symbols: \[ f(K) = f^{-1}^{-1}(K). \]

Subgroup.map_equiv_eq_comap_symm theorem

(f : G ≃* N) (K : Subgroup G) : K.map f = K.comap (G := N) f.symm

Full source

@[to_additive]
theorem map_equiv_eq_comap_symm (f : G ≃* N) (K : Subgroup G) :
    K.map f = K.comap (G := N) f.symm :=
  map_equiv_eq_comap_symm' _ _

Image-Preimage Duality for Subgroups under Group Isomorphism

Informal description

Let $f \colon G \simeq^* N$ be a group isomorphism between groups $G$ and $N$, and let $K$ be a subgroup of $G$. Then the image of $K$ under $f$ is equal to the preimage of $K$ under the inverse isomorphism $f^{-1}$. In symbols: \[ f(K) = f^{-1}^{-1}(K). \]

Subgroup.comap_equiv_eq_map_symm theorem

(f : N ≃* G) (K : Subgroup G) : K.comap (G := N) f = K.map f.symm

Full source

@[to_additive]
theorem comap_equiv_eq_map_symm (f : N ≃* G) (K : Subgroup G) :
    K.comap (G := N) f = K.map f.symm :=
  (map_equiv_eq_comap_symm f.symm K).symm

Preimage-Image Duality for Subgroups under Group Isomorphism

Informal description

Let $f \colon N \simeq^* G$ be a group isomorphism between groups $N$ and $G$, and let $K$ be a subgroup of $G$. Then the preimage of $K$ under $f$ is equal to the image of $K$ under the inverse isomorphism $f^{-1}$. In symbols: \[ f^{-1}(K) = f^{-1}(K). \]

Subgroup.comap_equiv_eq_map_symm' theorem

(f : N ≃* G) (K : Subgroup G) : K.comap f.toMonoidHom = K.map f.symm.toMonoidHom

Full source

@[to_additive]
theorem comap_equiv_eq_map_symm' (f : N ≃* G) (K : Subgroup G) :
    K.comap f.toMonoidHom = K.map f.symm.toMonoidHom :=
  (map_equiv_eq_comap_symm f.symm K).symm

Preimage-Image Duality for Subgroups under Group Isomorphism via Monoid Homomorphisms

Informal description

Let $f \colon N \simeq^* G$ be a group isomorphism between groups $N$ and $G$, and let $K$ be a subgroup of $G$. Then the preimage of $K$ under the monoid homomorphism associated to $f$ is equal to the image of $K$ under the monoid homomorphism associated to the inverse isomorphism $f^{-1}$. In symbols: \[ f^{-1}(K) = f^{-1}(K). \]

Subgroup.map_symm_eq_iff_map_eq theorem

{H : Subgroup N} {e : G ≃* N} : H.map ↑e.symm = K ↔ K.map ↑e = H

Full source

@[to_additive]
theorem map_symm_eq_iff_map_eq {H : Subgroup N} {e : G ≃* N} :
    H.map ↑e.symm = K ↔ K.map ↑e = H := by
  constructor <;> rintro rfl
  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]
  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
      MulEquiv.coe_monoidHom_refl, map_id]

Subgroup Image Symmetry under Isomorphism: $e^{-1}(H) = K \leftrightarrow e(K) = H$

Informal description

Let $G$ and $N$ be groups, $K$ a subgroup of $G$, $H$ a subgroup of $N$, and $e : G \simeq^* N$ a multiplicative isomorphism. Then the image of $H$ under the inverse isomorphism $e^{-1}$ equals $K$ if and only if the image of $K$ under $e$ equals $H$. In symbols: \[ e^{-1}(H) = K \leftrightarrow e(K) = H. \]

Subgroup.map_le_iff_le_comap theorem

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

Full source

@[to_additive]
theorem map_le_iff_le_comap {f : G →* N} {K : Subgroup G} {H : Subgroup N} :
    K.map f ≤ H ↔ K ≤ H.comap f :=
  image_subset_iff

Image-Preimage Subgroup Inclusion Equivalence

Informal description

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

Subgroup.gc_map_comap theorem

(f : G →* N) : GaloisConnection (map f) (comap f)

Full source

@[to_additive]
theorem gc_map_comap (f : G →* N) : GaloisConnection (map f) (comap f) := fun _ _ =>
  map_le_iff_le_comap

Galois Connection Between Subgroup Map and Preimage

Informal description

For any group homomorphism $f \colon G \to N$, the pair of functions $\text{map}(f)$ and $\text{comap}(f)$ forms a Galois connection between the lattices of subgroups of $G$ and $N$. Specifically, for any subgroup $K$ of $G$ and any subgroup $H$ of $N$, we have $\text{map}(f)(K) \leq H$ if and only if $K \leq \text{comap}(f)(H)$.

Subgroup.map_sup theorem

(H K : Subgroup G) (f : G →* N) : (H ⊔ K).map f = H.map f ⊔ K.map f

Full source

@[to_additive]
theorem map_sup (H K : Subgroup G) (f : G →* N) : (H ⊔ K).map f = H.map f ⊔ K.map f :=
  (gc_map_comap f).l_sup

Image of Subgroup Join Equals Join of Images under Group Homomorphism

Informal description

Let $G$ and $N$ be groups, $H$ and $K$ subgroups of $G$, and $f \colon G \to N$ a group homomorphism. Then the image of the join (supremum) of $H$ and $K$ under $f$ equals the join of their images: \[ f(H \sqcup K) = f(H) \sqcup f(K). \]

Subgroup.map_iSup theorem

{ι : Sort*} (f : G →* N) (s : ι → Subgroup G) : (iSup s).map f = ⨆ i, (s i).map f

Full source

@[to_additive]
theorem map_iSup {ι : Sort*} (f : G →* N) (s : ι → Subgroup G) :
    (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

Image of Subgroup Join under Homomorphism Equals Join of Images

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any indexed family of subgroups $\{s_i\}_{i \in \iota}$ of $G$, the image of the supremum (join) of the subgroups under $f$ equals the supremum of the images of the subgroups. That is, \[ f\left(\bigsqcup_{i \in \iota} s_i\right) = \bigsqcup_{i \in \iota} f(s_i). \]

Subgroup.map_inf theorem

(H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) : (H ⊓ K).map f = H.map f ⊓ K.map f

Full source

@[to_additive]
theorem map_inf (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
    (H ⊓ K).map f = H.map f ⊓ K.map f := SetLike.coe_injective (Set.image_inter hf)

Image of Subgroup Intersection under Injective Homomorphism Equals Intersection of Images

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be an injective group homomorphism. For any two subgroups $H$ and $K$ of $G$, the image of their intersection under $f$ equals the intersection of their images, i.e., \[ f(H \cap K) = f(H) \cap f(K). \]

Subgroup.map_iInf theorem

 {ι : Sort*} [Nonempty ι] (f : G →* N) (hf : Function.Injective f) (s : ι → Subgroup G) :
  (iInf s).map f = ⨅ i, (s i).map f

Full source

@[to_additive]
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : G →* N) (hf : Function.Injective f)
    (s : ι → Subgroup G) : (iInf s).map f = ⨅ i, (s i).map f := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coeSetLike.coe ∘ s)

Image of Subgroup Intersection under Injective Homomorphism Equals Intersection of Images

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be an injective group homomorphism. Given a nonempty index set $\iota$ and a family of subgroups $\{s_i\}_{i \in \iota}$ of $G$, the image of the infimum (intersection) of the subgroups under $f$ equals the infimum of the images of the subgroups. That is, \[ f\left(\bigcap_{i \in \iota} s_i\right) = \bigcap_{i \in \iota} f(s_i). \]

Subgroup.comap_sup_comap_le theorem

(H K : Subgroup N) (f : G →* N) : comap f H ⊔ comap f K ≤ comap f (H ⊔ K)

Full source

@[to_additive]
theorem comap_sup_comap_le (H K : Subgroup N) (f : G →* N) :
    comapcomap f H ⊔ comap f K ≤ comap f (H ⊔ K) :=
  Monotone.le_map_sup (fun _ _ => comap_mono) H K

Preimage of Supremum of Subgroups Contains Supremum of Preimages

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 $N$, the supremum (join) of the preimages $f^{-1}(H)$ and $f^{-1}(K)$ is contained in the preimage of the supremum of $H$ and $K$, i.e., \[ f^{-1}(H) \sqcup f^{-1}(K) \leq f^{-1}(H \sqcup K). \]

Subgroup.iSup_comap_le theorem

{ι : Sort*} (f : G →* N) (s : ι → Subgroup N) : ⨆ i, (s i).comap f ≤ (iSup s).comap f

Full source

@[to_additive]
theorem iSup_comap_le {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) :
    ⨆ i, (s i).comap f ≤ (iSup s).comap f :=
  Monotone.le_map_iSup fun _ _ => comap_mono

Supremum of Preimages is Contained in Preimage of Supremum for Group Homomorphisms

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any family of subgroups $\{s_i\}_{i \in \iota}$ of $N$, the supremum of the preimages $f^{-1}(s_i)$ is contained in the preimage of the supremum of the subgroups $s_i$. That is, \[ \bigsqcup_{i \in \iota} f^{-1}(s_i) \leq f^{-1}\left(\bigsqcup_{i \in \iota} s_i\right). \]

Subgroup.comap_inf theorem

(H K : Subgroup N) (f : G →* N) : (H ⊓ K).comap f = H.comap f ⊓ K.comap f

Full source

@[to_additive]
theorem comap_inf (H K : Subgroup N) (f : G →* N) : (H ⊓ K).comap f = H.comap f ⊓ K.comap f :=
  (gc_map_comap f).u_inf

Preimage of Subgroup Intersection Equals Intersection of Preimages

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any two subgroups $H$ and $K$ of $N$, the preimage of their intersection $H \cap K$ under $f$ is equal to the intersection of their preimages, i.e., \[ f^{-1}(H \cap K) = f^{-1}(H) \cap f^{-1}(K). \]

Subgroup.comap_iInf theorem

{ι : Sort*} (f : G →* N) (s : ι → Subgroup N) : (iInf s).comap f = ⨅ i, (s i).comap f

Full source

@[to_additive]
theorem comap_iInf {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) :
    (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

Preimage of Infimum of Subgroups Equals Infimum of Preimages

Informal description

Let $G$ and $N$ be groups, $f \colon G \to N$ be a group homomorphism, and $\{s_i\}_{i \in \iota}$ be a family of subgroups of $N$. Then the preimage of the infimum of the subgroups $s_i$ under $f$ equals the infimum of the preimages of the subgroups $s_i$ under $f$. In other words, \[ f^{-1}\left(\bigsqcap_{i \in \iota} s_i\right) = \bigsqcap_{i \in \iota} f^{-1}(s_i). \]

Subgroup.map_inf_le theorem

(H K : Subgroup G) (f : G →* N) : map f (H ⊓ K) ≤ map f H ⊓ map f K

Full source

@[to_additive]
theorem map_inf_le (H K : Subgroup G) (f : G →* N) : map f (H ⊓ K) ≤ mapmap f H ⊓ map f K :=
  le_inf (map_mono inf_le_left) (map_mono inf_le_right)

Image of Subgroup Intersection is Contained in Intersection of Images

Informal description

For any subgroups $H$ and $K$ of a group $G$ and any group homomorphism $f \colon G \to N$, the image of the intersection $H \cap K$ under $f$ is contained in the intersection of the images of $H$ and $K$ under $f$, i.e., $f(H \cap K) \leq f(H) \cap f(K)$.

Subgroup.map_inf_eq theorem

(H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) : map f (H ⊓ K) = map f H ⊓ map f K

Full source

@[to_additive]
theorem map_inf_eq (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
    map f (H ⊓ K) = mapmap f H ⊓ map f K := by
  rw [← SetLike.coe_set_eq]
  simp [Set.image_inter hf]

Image of Subgroup Intersection Equals Intersection of Images for Injective Homomorphisms

Informal description

Let $G$ and $N$ be groups, $H$ and $K$ be subgroups of $G$, and $f \colon G \to N$ be an injective group homomorphism. Then the image of the intersection $H \cap K$ under $f$ equals the intersection of the images of $H$ and $K$ under $f$, i.e., \[ f(H \cap K) = f(H) \cap f(K). \]

Subgroup.map_bot theorem

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

Full source

@[to_additive (attr := simp)]
theorem map_bot (f : G →* N) : (⊥ : Subgroup G).map f = ⊥ :=
  (gc_map_comap f).l_bot

Image of Trivial Subgroup is Trivial

Informal description

For any group homomorphism $f \colon G \to N$, the image of the trivial subgroup $\bot$ of $G$ under $f$ is the trivial subgroup $\bot$ of $N$, i.e., $f(\bot) = \bot$.

Subgroup.map_top_of_surjective theorem

(f : G →* N) (h : Function.Surjective f) : Subgroup.map f ⊤ = ⊤

Full source

@[to_additive (attr := simp)]
theorem map_top_of_surjective (f : G →* N) (h : Function.Surjective f) : Subgroup.map f ⊤ = ⊤ := by
  rw [eq_top_iff]
  intro x _
  obtain ⟨y, hy⟩ := h x
  exact ⟨y, trivial, hy⟩

Image of Trivial Subgroup under Surjective Homomorphism is Trivial

Informal description

Let $f \colon G \to N$ be a surjective group homomorphism. Then the image of the trivial subgroup $\top$ of $G$ under $f$ is the trivial subgroup $\top$ of $N$, i.e., $f(\top) = \top$.

Subgroup.comap_top theorem

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

Full source

@[to_additive (attr := simp)]
theorem comap_top (f : G →* N) : (⊤ : Subgroup N).comap f = ⊤ :=
  (gc_map_comap f).u_top

Preimage of Trivial Subgroup is Trivial

Informal description

For any group homomorphism $f \colon G \to N$, the preimage of the trivial subgroup $\top$ of $N$ under $f$ is the trivial subgroup $\top$ of $G$, i.e., $f^{-1}(\top) = \top$.

Subgroup.subgroupOf definition

(H K : Subgroup G) : Subgroup K

Full source

/-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`. -/
@[to_additive "For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`."]
def subgroupOf (H K : Subgroup G) : Subgroup K :=
  H.comap K.subtype

Intersection of subgroups as a subgroup of the smaller subgroup

Informal description

For any subgroups $ H $ and $ K $ of a group $ G $, the structure `H.subgroupOf K` represents the intersection $ H \cap K $ viewed as a subgroup of $ K $. This is constructed as the preimage of $ H $ under the canonical inclusion homomorphism $ K \hookrightarrow G $.

Subgroup.subgroupOfEquivOfLe definition

{G : Type*} [Group G] {H K : Subgroup G} (h : H ≤ K) : H.subgroupOf K ≃* H

Full source

/-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`. -/
@[to_additive (attr := simps) "If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`."]
def subgroupOfEquivOfLe {G : Type*} [Group G] {H K : Subgroup G} (h : H ≤ K) :
    H.subgroupOf K ≃* H where
  toFun g := ⟨g.1, g.2⟩
  invFun g := ⟨⟨g.1, h g.2⟩, g.2⟩
  left_inv _g := Subtype.ext (Subtype.ext rfl)
  right_inv _g := Subtype.ext rfl
  map_mul' _g _h := rfl

Isomorphism between a subgroup and its intersection with a larger subgroup

Informal description

Given a group $G$ and subgroups $H$ and $K$ of $G$ such that $H \leq K$, the subgroup $H \cap K$ (viewed as a subgroup of $K$) is multiplicatively isomorphic to $H$ itself. The isomorphism maps an element $g \in H \cap K$ to its underlying element in $H$, and its inverse maps an element $h \in H$ to the pair $\langle h, \text{witness that } h \in K \rangle$ in $H \cap K$.

Subgroup.comap_subtype theorem

(H K : Subgroup G) : H.comap K.subtype = H.subgroupOf K

Full source

@[to_additive (attr := simp)]
theorem comap_subtype (H K : Subgroup G) : H.comap K.subtype = H.subgroupOf K :=
  rfl

Preimage of Subgroup Under Inclusion Equals Intersection Subgroup

Informal description

For any subgroups $H$ and $K$ of a group $G$, the preimage of $H$ under the canonical inclusion homomorphism $K \hookrightarrow G$ is equal to the intersection $H \cap K$ viewed as a subgroup of $K$.

Subgroup.comap_inclusion_subgroupOf theorem

 {K₁ K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G) : (H.subgroupOf K₂).comap (inclusion h) = H.subgroupOf K₁

Full source

@[to_additive (attr := simp)]
theorem comap_inclusion_subgroupOf {K₁ K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G) :
    (H.subgroupOf K₂).comap (inclusion h) = H.subgroupOf K₁ :=
  rfl

Preimage of Intersection Under Subgroup Inclusion

Informal description

Let $G$ be a group with subgroups $K_1 \leq K_2 \leq G$ and $H \leq G$. Then the preimage of $H \cap K_2$ under the inclusion homomorphism $\text{inclusion}(h) : K_1 \hookrightarrow K_2$ equals $H \cap K_1$. In other words, we have: $$(\text{inclusion}(h))^{-1}(H \cap K_2) = H \cap K_1$$ where $\text{inclusion}(h)$ is the canonical inclusion map induced by $K_1 \leq K_2$.

Subgroup.coe_subgroupOf theorem

(H K : Subgroup G) : (H.subgroupOf K : Set K) = K.subtype ⁻¹' H

Full source

@[to_additive]
theorem coe_subgroupOf (H K : Subgroup G) : (H.subgroupOf K : Set K) = K.subtype ⁻¹' H :=
  rfl

Preimage Characterization of Subgroup Intersection

Informal description

For any subgroups $H$ and $K$ of a group $G$, the underlying set of the subgroup $H \cap K$ (viewed as a subgroup of $K$) is equal to the preimage of $H$ under the canonical inclusion homomorphism $K \hookrightarrow G$. In other words, $(H \cap K : \text{Set } K) = \iota_K^{-1}(H)$, where $\iota_K$ is the inclusion map of $K$ into $G$.

Subgroup.mem_subgroupOf theorem

{H K : Subgroup G} {h : K} : h ∈ H.subgroupOf K ↔ (h : G) ∈ H

Full source

@[to_additive]
theorem mem_subgroupOf {H K : Subgroup G} {h : K} : h ∈ H.subgroupOf Kh ∈ H.subgroupOf K ↔ (h : G) ∈ H :=
  Iff.rfl

Membership Criterion for Subgroup Intersection

Informal description

Let $G$ be a group with subgroups $H$ and $K$, and let $h$ be an element of $K$. Then $h$ belongs to the subgroup $H \cap K$ (viewed as a subgroup of $K$) if and only if $h$, considered as an element of $G$, belongs to $H$. In other words: $$h \in H \cap K \leftrightarrow h \in H$$

Subgroup.subgroupOf_map_subtype theorem

(H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K

Full source

@[to_additive (attr := simp)]
theorem subgroupOf_map_subtype (H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K :=
  SetLike.ext' <| by refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm

Image of Intersection Subgroup under Inclusion Equals Intersection

Informal description

For any subgroups $H$ and $K$ of a group $G$, the image of the intersection subgroup $H \cap K$ (viewed as a subgroup of $K$) under the canonical inclusion homomorphism $K \hookrightarrow G$ equals the intersection $H \cap K$ as a subgroup of $G$. In other words, $\text{map}(\iota_K)(H \cap K) = H \cap K$, where $\iota_K$ is the inclusion map of $K$ into $G$.

Subgroup.map_subgroupOf_eq_of_le theorem

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

Full source

@[to_additive]
theorem map_subgroupOf_eq_of_le {H K : Subgroup G} (h : H ≤ K) :
    (H.subgroupOf K).map K.subtype = H := by
  rwa [subgroupOf_map_subtype, inf_eq_left]

Image of Intersection Subgroup under Inclusion Equals Original Subgroup when $H \leq K$

Informal description

Let $G$ be a group with subgroups $H$ and $K$ such that $H \leq K$. Then the image of the intersection subgroup $H \cap K$ (viewed as a subgroup of $K$) under the canonical inclusion homomorphism $K \hookrightarrow G$ equals $H$.

Subgroup.bot_subgroupOf theorem

: (⊥ : Subgroup G).subgroupOf H = ⊥

Full source

@[to_additive (attr := simp)]
theorem bot_subgroupOf : (⊥ : Subgroup G).subgroupOf H = ⊥ :=
  Eq.symm (Subgroup.ext fun _g => Subtype.ext_iff)

Trivial Subgroup Intersection Property

Informal description

For any subgroup $H$ of a group $G$, the intersection of the trivial subgroup $\bot$ with $H$ is again the trivial subgroup, i.e., $\bot \cap H = \bot$.

Subgroup.top_subgroupOf theorem

: (⊤ : Subgroup G).subgroupOf H = ⊤

Full source

@[to_additive (attr := simp)]
theorem top_subgroupOf : (⊤ : Subgroup G).subgroupOf H = ⊤ :=
  rfl

Trivial Subgroup Intersection with Any Subgroup is Trivial

Informal description

For any subgroup $H$ of a group $G$, the intersection of the trivial subgroup $\top$ (the entire group $G$) with $H$ is equal to the trivial subgroup $\top$ of $H$.

Subgroup.subgroupOf_bot_eq_bot theorem

: H.subgroupOf ⊥ = ⊥

Full source

@[to_additive]
theorem subgroupOf_bot_eq_bot : H.subgroupOf ⊥ = ⊥ :=
  Subsingleton.elim _ _

Intersection with Trivial Subgroup is Trivial

Informal description

For any subgroup $H$ of a group $G$, the intersection of $H$ with the trivial subgroup $\bot$ is the trivial subgroup $\bot$ when viewed as a subgroup of $\bot$.

Subgroup.subgroupOf_bot_eq_top theorem

: H.subgroupOf ⊥ = ⊤

Full source

@[to_additive]
theorem subgroupOf_bot_eq_top : H.subgroupOf ⊥ = ⊤ :=
  Subsingleton.elim _ _

Intersection with Trivial Subgroup Yields Trivial Subgroup

Informal description

For any subgroup $H$ of a group $G$, the intersection of $H$ with the trivial subgroup $\bot$ of $G$ is equal to the trivial subgroup $\top$ of $\bot$.

Subgroup.subgroupOf_self theorem

: H.subgroupOf H = ⊤

Full source

@[to_additive (attr := simp)]
theorem subgroupOf_self : H.subgroupOf H = ⊤ :=
  top_unique fun g _hg => g.2

Self-Intersection of Subgroup is Trivial Subgroup

Informal description

For any subgroup $H$ of a group $G$, the intersection of $H$ with itself, viewed as a subgroup of $H$, is equal to the trivial subgroup $\top$ of $H$.

Subgroup.subgroupOf_inj theorem

{H₁ H₂ K : Subgroup G} : H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

Full source

@[to_additive (attr := simp)]
theorem subgroupOf_inj {H₁ H₂ K : Subgroup G} :
    H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K := by
  simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall

Injective Property of Subgroup Restriction: $H₁.\text{subgroupOf}\ K = H₂.\text{subgroupOf}\ K \leftrightarrow H₁ \cap K = H₂ \cap K$

Informal description

For any subgroups $H₁$, $H₂$, and $K$ of a group $G$, the equality $H₁.\text{subgroupOf}\ K = H₂.\text{subgroupOf}\ K$ holds if and only if the intersections $H₁ \cap K$ and $H₂ \cap K$ are equal.

Subgroup.inf_subgroupOf_right theorem

(H K : Subgroup G) : (H ⊓ K).subgroupOf K = H.subgroupOf K

Full source

@[to_additive (attr := simp)]
theorem inf_subgroupOf_right (H K : Subgroup G) : (H ⊓ K).subgroupOf K = H.subgroupOf K :=
  subgroupOf_inj.2 (inf_right_idem _ _)

Right Intersection Subgroup Equality: $(H \cap K).\text{subgroupOf}\ K = H.\text{subgroupOf}\ K$

Informal description

For any subgroups $H$ and $K$ of a group $G$, the intersection $H \cap K$ viewed as a subgroup of $K$ is equal to $H$ viewed as a subgroup of $K$. In other words, $(H \cap K).\text{subgroupOf}\ K = H.\text{subgroupOf}\ K$.

Subgroup.inf_subgroupOf_left theorem

(H K : Subgroup G) : (K ⊓ H).subgroupOf K = H.subgroupOf K

Full source

@[to_additive (attr := simp)]
theorem inf_subgroupOf_left (H K : Subgroup G) : (K ⊓ H).subgroupOf K = H.subgroupOf K := by
  rw [inf_comm, inf_subgroupOf_right]

Left Intersection Subgroup Equality: $(K \cap H).\text{subgroupOf}\ K = H.\text{subgroupOf}\ K$

Informal description

For any subgroups $H$ and $K$ of a group $G$, the intersection $K \sqcap H$ viewed as a subgroup of $K$ is equal to $H$ viewed as a subgroup of $K$. In other words, $(K \sqcap H).\text{subgroupOf}\ K = H.\text{subgroupOf}\ K$.

Subgroup.subgroupOf_eq_bot theorem

{H K : Subgroup G} : H.subgroupOf K = ⊥ ↔ Disjoint H K

Full source

@[to_additive (attr := simp)]
theorem subgroupOf_eq_bot {H K : Subgroup G} : H.subgroupOf K = ⊥ ↔ Disjoint H K := by
  rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]

Trivial Intersection Criterion for Subgroups: $H \cap K = \bot$ iff $H$ and $K$ are Disjoint

Informal description

For any subgroups $H$ and $K$ of a group $G$, the intersection $H \cap K$ is the trivial subgroup (i.e., $H.\text{subgroupOf}\ K = \bot$) if and only if $H$ and $K$ are disjoint (i.e., $H \sqcap K = \bot$ in the lattice of subgroups).

Subgroup.subgroupOf_eq_top theorem

{H K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H

Full source

@[to_additive (attr := simp)]
theorem subgroupOf_eq_top {H K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H := by
  rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]

Subgroup Intersection Equals Trivial Subgroup if and only if Inclusion Holds

Informal description

For any subgroups $H$ and $K$ of a group $G$, the intersection $H \cap K$ viewed as a subgroup of $K$ is equal to the trivial subgroup of $K$ (i.e., $K$ itself) if and only if $K$ is a subgroup of $H$.

Subgroup.map_isMulCommutative instance

(f : G →* G') [IsMulCommutative H] : IsMulCommutative (H.map f)

Full source

@[to_additive]
instance map_isMulCommutative (f : G →* G') [IsMulCommutative H] : IsMulCommutative (H.map f) :=
  ⟨⟨by
      rintro ⟨-, a, ha, rfl⟩ ⟨-, b, hb, rfl⟩
      rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← map_mul, ← map_mul]
      exact congr_arg f (Subtype.ext_iff.mp (mul_comm (⟨a, ha⟩ : H) ⟨b, hb⟩))⟩⟩

Image of Commutative Subgroup under Homomorphism is Commutative

Informal description

For any group homomorphism $f \colon G \to G'$ and any subgroup $H$ of $G$ with commutative multiplication, the image subgroup $H.map(f)$ also has commutative multiplication.

Subgroup.comap_injective_isMulCommutative theorem

{f : G' →* G} (hf : Injective f) [IsMulCommutative H] : IsMulCommutative (H.comap f)

Full source

@[to_additive]
theorem comap_injective_isMulCommutative {f : G' →* G} (hf : Injective f) [IsMulCommutative H] :
    IsMulCommutative (H.comap f) :=
  ⟨⟨fun a b =>
      Subtype.ext
        (by
          have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H)
          rwa [Subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ← map_mul, ← map_mul,
            hf.eq_iff] at this)⟩⟩

Preimage of Commutative Subgroup under Injective Homomorphism is Commutative

Informal description

Let $f \colon G' \to G$ be an injective group homomorphism and let $H$ be a subgroup of $G$ with commutative multiplication. Then the preimage subgroup $f^{-1}(H)$ in $G'$ also has commutative multiplication.

Subgroup.subgroupOf_isMulCommutative instance

[IsMulCommutative H] : IsMulCommutative (H.subgroupOf K)

Full source

@[to_additive]
instance subgroupOf_isMulCommutative [IsMulCommutative H] : IsMulCommutative (H.subgroupOf K) :=
  H.comap_injective_isMulCommutative Subtype.coe_injective

Commutativity of Subgroup Intersection

Informal description

For any subgroups $H$ and $K$ of a group $G$, if $H$ has commutative multiplication, then the intersection $H \cap K$ viewed as a subgroup of $K$ also has commutative multiplication.

MulEquiv.comapSubgroup definition

(f : G ≃* H) : Subgroup H ≃o Subgroup G

Full source

/--
An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their inverse images.

See also `MulEquiv.mapSubgroup` which maps subgroups to their forward images.
-/
@[to_additive (attr := simps)
"An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their inverse images.

See also `AddEquiv.mapAddSubgroup` which maps subgroups to their forward images."]
def comapSubgroup (f : G ≃* H) : SubgroupSubgroup H ≃o Subgroup G where
  toFun := Subgroup.comap f
  invFun := Subgroup.comap f.symm
  left_inv sg := by simp [Subgroup.comap_comap]
  right_inv sh := by simp [Subgroup.comap_comap]
  map_rel_iff' {sg1 sg2} :=
    ⟨fun h => by simpa [Subgroup.comap_comap] using
      Subgroup.comap_mono (f := (f.symm : H →* G)) h, Subgroup.comap_mono⟩

Order isomorphism of subgroup lattices induced by a group isomorphism

Informal description

Given a multiplicative isomorphism $ f : G \simeq^* H $ between groups $ G $ and $ H $, the function maps a subgroup $ K $ of $ H $ to its preimage $ f^{-1}(K) $ in $ G $, establishing an order isomorphism between the lattices of subgroups of $ H $ and $ G $. This means that for any subgroups $ K_1, K_2 $ of $ H $, we have $ K_1 \leq K_2 $ if and only if $ f^{-1}(K_1) \leq f^{-1}(K_2) $.

MulEquiv.coe_comapSubgroup theorem

(e : G ≃* H) : comapSubgroup e = Subgroup.comap e.toMonoidHom

Full source

@[to_additive (attr := simp, norm_cast)]
lemma coe_comapSubgroup (e : G ≃* H) : comapSubgroup e = Subgroup.comap e.toMonoidHom := rfl

Equality of Subgroup Preimage Operations via Group Isomorphism

Informal description

For any group isomorphism $e \colon G \simeq^* H$, the function `comapSubgroup e` is equal to the preimage of a subgroup under the group homomorphism $e$, i.e., $\text{comapSubgroup}\, e = \text{Subgroup.comap}\, e$.

MulEquiv.symm_comapSubgroup theorem

(e : G ≃* H) : (comapSubgroup e).symm = comapSubgroup e.symm

Full source

@[to_additive (attr := simp)]
lemma symm_comapSubgroup (e : G ≃* H) : (comapSubgroup e).symm = comapSubgroup e.symm := rfl

Inverse of Subgroup Lattice Isomorphism Induced by Group Isomorphism

Informal description

For any group isomorphism $e : G \simeq^* H$, the inverse of the order isomorphism between subgroup lattices induced by $e$ is equal to the order isomorphism induced by the inverse group isomorphism $e^{-1} : H \simeq^* G$. In other words, $(e^{-1})^* = (e^*)^{-1}$, where $e^*$ denotes the induced order isomorphism on subgroup lattices.

MulEquiv.mapSubgroup definition

{H : Type*} [Group H] (f : G ≃* H) : Subgroup G ≃o Subgroup H

Full source

/--
An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their forward images.

See also `MulEquiv.comapSubgroup` which maps subgroups to their inverse images.
-/
@[to_additive (attr := simps)
"An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their forward images.

See also `AddEquiv.comapAddSubgroup` which maps subgroups to their inverse images."]
def mapSubgroup {H : Type*} [Group H] (f : G ≃* H) : SubgroupSubgroup G ≃o Subgroup H where
  toFun := Subgroup.map f
  invFun := Subgroup.map f.symm
  left_inv sg := by simp [Subgroup.map_map]
  right_inv sh := by simp [Subgroup.map_map]
  map_rel_iff' {sg1 sg2} :=
    ⟨fun h => by simpa [Subgroup.map_map] using
      Subgroup.map_mono (f := (f.symm : H →* G)) h, Subgroup.map_mono⟩

Order isomorphism of subgroup lattices induced by a group isomorphism

Informal description

Given a multiplicative isomorphism $ f \colon G \simeq^* H $ between groups $ G $ and $ H $, the function `MulEquiv.mapSubgroup` induces an order isomorphism between the lattices of subgroups of $ G $ and $ H $. Specifically, it maps each subgroup $ K $ of $ G $ to its image $ f(K) $ in $ H $, and this correspondence preserves the subgroup inclusion relation.

MulEquiv.coe_mapSubgroup theorem

(e : G ≃* H) : mapSubgroup e = Subgroup.map e.toMonoidHom

Full source

@[to_additive (attr := simp, norm_cast)]
lemma coe_mapSubgroup (e : G ≃* H) : mapSubgroup e = Subgroup.map e.toMonoidHom := rfl

Equality of subgroup images under group isomorphism and its monoid homomorphism

Informal description

Given a group isomorphism $e \colon G \simeq^* H$, the image of a subgroup under $e$ is equal to the image of the subgroup under the group homomorphism corresponding to $e$. In other words, the map `mapSubgroup e` coincides with `Subgroup.map e.toMonoidHom`.

MulEquiv.symm_mapSubgroup theorem

(e : G ≃* H) : (mapSubgroup e).symm = mapSubgroup e.symm

Full source

@[to_additive (attr := simp)]
lemma symm_mapSubgroup (e : G ≃* H) : (mapSubgroup e).symm = mapSubgroup e.symm := rfl

Inverse of Subgroup Lattice Isomorphism Induced by Group Isomorphism

Informal description

For any group isomorphism $e \colon G \simeq^* H$, the inverse of the induced order isomorphism on subgroup lattices $(\text{mapSubgroup}\; e)^{-1}$ is equal to the order isomorphism induced by the inverse group isomorphism $\text{mapSubgroup}\; e^{-1}$.

Subgroup.comap_toSubmonoid theorem

(e : G ≃* N) (s : Subgroup N) : (s.comap e).toSubmonoid = s.toSubmonoid.comap e.toMonoidHom

Full source

@[to_additive (attr := simp, norm_cast)]
lemma comap_toSubmonoid (e : G ≃* N) (s : Subgroup N) :
    (s.comap e).toSubmonoid = s.toSubmonoid.comap e.toMonoidHom := rfl

Preimage of Subgroup's Submonoid under Group Isomorphism

Informal description

Let $e \colon G \simeq^* N$ be a group isomorphism and $s$ be a subgroup of $N$. Then the underlying submonoid of the preimage $s.comap\, e$ is equal to the preimage of the underlying submonoid of $s$ under the monoid homomorphism corresponding to $e$.

Subgroup.map_comap_le theorem

(H : Subgroup N) : map f (comap f H) ≤ H

Full source

@[to_additive]
theorem map_comap_le (H : Subgroup N) : map f (comap f H) ≤ H :=
  (gc_map_comap f).l_u_le _

Image of Preimage is Contained in Original Subgroup

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 contained in $H$, i.e., $f(f^{-1}(H)) \leq H$.

Subgroup.le_comap_map theorem

(H : Subgroup G) : H ≤ comap f (map f H)

Full source

@[to_additive]
theorem le_comap_map (H : Subgroup G) : H ≤ comap f (map f H) :=
  (gc_map_comap f).le_u_l _

Subgroup containment in preimage of its image under homomorphism

Informal description

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

Subgroup.map_eq_comap_of_inverse theorem

 {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f) (hr : Function.RightInverse g f) (H : Subgroup G) :
  map f H = comap g H

Full source

@[to_additive]
theorem map_eq_comap_of_inverse {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f)
    (hr : Function.RightInverse g f) (H : Subgroup G) : map f H = comap g H :=
  SetLike.ext' <| by rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]

Image Equals Preimage under Group Homomorphism Inverse

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ and $g \colon N \to G$ be group homomorphisms such that $g$ is both a left and right inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in G$ and $f(g(y)) = y$ for all $y \in N$). Then for any subgroup $H$ of $G$, the image of $H$ under $f$ equals the preimage of $H$ under $g$, i.e., $$ f(H) = g^{-1}(H). $$

Subgroup.equivMapOfInjective definition

(H : Subgroup G) (f : G →* N) (hf : Function.Injective f) : H ≃* H.map f

Full source

/-- A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use `MulEquiv.subgroupMap` for better definitional equalities. -/
@[to_additive
      "An additive subgroup is isomorphic to its image under an injective function. If you
      have an isomorphism, use `AddEquiv.addSubgroupMap` for better definitional equalities."]
noncomputable def equivMapOfInjective (H : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
    H ≃* H.map f :=
  { Equiv.Set.image f H hf with map_mul' := fun _ _ => Subtype.ext (f.map_mul _ _) }

Isomorphism between a subgroup and its image under an injective homomorphism

Informal description

Given a subgroup $ H $ of a group $ G $, a group homomorphism $ f \colon G \to N $, and the assumption that $ f $ is injective, the subgroup $ H $ is isomorphic to its image $ f(H) $ under $ f $. The isomorphism is given by the bijection between $ H $ and $ f(H) $ induced by $ f $, which preserves the group operation.

Subgroup.coe_equivMapOfInjective_apply theorem

(H : Subgroup G) (f : G →* N) (hf : Function.Injective f) (h : H) : (equivMapOfInjective H f hf h : N) = f h

Full source

@[to_additive (attr := simp)]
theorem coe_equivMapOfInjective_apply (H : Subgroup G) (f : G →* N) (hf : Function.Injective f)
    (h : H) : (equivMapOfInjective H f hf h : N) = f h :=
  rfl

Image of subgroup element under injective homomorphism equals its image under the isomorphism

Informal description

Let $G$ and $N$ be groups, $H$ a subgroup of $G$, and $f \colon G \to N$ an injective group homomorphism. For any element $h \in H$, the image of $h$ under the isomorphism $\text{equivMapOfInjective}\ H\ f\ hf$ (which maps $H$ to its image $f(H)$) equals $f(h)$ when viewed as an element of $N$.

MonoidHom.subgroupComap definition

(f : G →* G') (H' : Subgroup G') : H'.comap f →* H'

Full source

/-- The `MonoidHom` from the preimage of a subgroup to itself. -/
@[to_additive (attr := simps!) "the `AddMonoidHom` from the preimage of an
additive subgroup to itself."]
def subgroupComap (f : G →* G') (H' : Subgroup G') : H'.comap f →* H' :=
  f.submonoidComap H'.toSubmonoid

Restriction of a group homomorphism to the preimage of a subgroup

Informal description

Given a group homomorphism $ f \colon G \to G' $ and a subgroup $ H' $ of $ G' $, the function `MonoidHom.subgroupComap` constructs a group homomorphism from the preimage subgroup $ f^{-1}(H') $ to $ H' $. Specifically, it maps an element $ x $ of $ f^{-1}(H') $ to $ f(x) $ in $ H' $, preserving the group structure (identity, multiplication, and inversion).

MonoidHom.subgroupComap_surjective_of_surjective theorem

(f : G →* G') (H' : Subgroup G') (hf : Surjective f) : Surjective (f.subgroupComap H')

Full source

@[to_additive]
lemma subgroupComap_surjective_of_surjective (f : G →* G') (H' : Subgroup G') (hf : Surjective f) :
    Surjective (f.subgroupComap H') :=
  f.submonoidComap_surjective_of_surjective H'.toSubmonoid hf

Surjectivity of Restricted Homomorphism from Preimage Subgroup

Informal description

Let $f \colon G \to G'$ be a surjective group homomorphism and let $H'$ be a subgroup of $G'$. Then the restricted homomorphism $f|_{f^{-1}(H')} \colon f^{-1}(H') \to H'$ is also surjective.

MonoidHom.subgroupMap definition

(f : G →* G') (H : Subgroup G) : H →* H.map f

Full source

/-- The `MonoidHom` from a subgroup to its image. -/
@[to_additive (attr := simps!) "the `AddMonoidHom` from an additive subgroup to its image"]
def subgroupMap (f : G →* G') (H : Subgroup G) : H →* H.map f :=
  f.submonoidMap H.toSubmonoid

Image of a subgroup under a group homomorphism

Informal description

Given a group homomorphism $ f \colon G \to G' $ and a subgroup $ H $ of $ G $, the function `MonoidHom.subgroupMap` maps $ H $ to its image under $ f $, which is a subgroup of $ G' $. Specifically, it sends each element $ x \in H $ to $ f(x) $, ensuring that the image is a subgroup by preserving the identity, multiplication, and inverses.

MonoidHom.subgroupMap_surjective theorem

(f : G →* G') (H : Subgroup G) : Function.Surjective (f.subgroupMap H)

Full source

@[to_additive]
theorem subgroupMap_surjective (f : G →* G') (H : Subgroup G) :
    Function.Surjective (f.subgroupMap H) :=
  f.submonoidMap_surjective H.toSubmonoid

Surjectivity of the Subgroup Map Induced by a Group Homomorphism

Informal description

For any group homomorphism $f \colon G \to G'$ and any subgroup $H$ of $G$, the induced homomorphism $f.subgroupMap H \colon H \to H.map f$ is surjective. That is, for every element $y$ in the image subgroup $H.map f$, there exists an element $x \in H$ such that $f(x) = y$.

MulEquiv.subgroupCongr definition

(h : H = K) : H ≃* K

Full source

/-- Makes the identity isomorphism from a proof two subgroups of a multiplicative
    group are equal. -/
@[to_additive
      "Makes the identity additive isomorphism from a proof
      two subgroups of an additive group are equal."]
def subgroupCongr (h : H = K) : H ≃* K :=
  { Equiv.setCongr <| congr_arg _ h with map_mul' := fun _ _ => rfl }

Subgroup equality isomorphism

Informal description

Given two subgroups $H$ and $K$ of a group $G$ that are equal ($H = K$), the multiplicative equivalence (isomorphism) $\text{MulEquiv.subgroupCongr}\ h$ establishes an isomorphism between $H$ and $K$ as multiplicative structures. This isomorphism maps each element $x \in H$ to the corresponding element $x \in K$ (since $H = K$), and preserves the group multiplication operation.

MulEquiv.subgroupCongr_apply theorem

(h : H = K) (x) : (MulEquiv.subgroupCongr h x : G) = x

Full source

@[to_additive (attr := simp)]
lemma subgroupCongr_apply (h : H = K) (x) :
    (MulEquiv.subgroupCongr h x : G) = x := rfl

Isomorphism Application Preserves Elements in Subgroup Congruence

Informal description

Given two subgroups $H$ and $K$ of a group $G$ such that $H = K$, the multiplicative isomorphism $\text{subgroupCongr}\ h$ maps any element $x \in H$ to the same element $x \in K$ when viewed as elements of $G$.

MulEquiv.subgroupCongr_symm_apply theorem

(h : H = K) (x) : ((MulEquiv.subgroupCongr h).symm x : G) = x

Full source

@[to_additive (attr := simp)]
lemma subgroupCongr_symm_apply (h : H = K) (x) :
    ((MulEquiv.subgroupCongr h).symm x : G) = x := rfl

Inverse of Subgroup Congruence Isomorphism Preserves Elements

Informal description

Given two subgroups $H$ and $K$ of a group $G$ such that $H = K$, for any element $x \in K$, the inverse of the isomorphism $\text{subgroupCongr}\ h$ maps $x$ to the same element $x$ when viewed as an element of $G$.

MulEquiv.subgroupMap definition

(e : G ≃* G') (H : Subgroup G) : H ≃* H.map (e : G →* G')

Full source

/-- A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
use `Subgroup.equiv_map_of_injective`. -/
@[to_additive
      "An additive subgroup is isomorphic to its image under an isomorphism. If you only
      have an injective map, use `AddSubgroup.equiv_map_of_injective`."]
def subgroupMap (e : G ≃* G') (H : Subgroup G) : H ≃* H.map (e : G →* G') :=
  MulEquiv.submonoidMap (e : G ≃* G') H.toSubmonoid

Subgroup isomorphism induced by a group isomorphism

Informal description

Given a group isomorphism $ e \colon G \simeq^* G' $ and a subgroup $ H $ of $ G $, the function constructs a group isomorphism between $ H $ and the image subgroup $ e(H) $ in $ G' $. This isomorphism maps each element $ h \in H $ to $ e(h) \in e(H) $, preserving the group structure.

MulEquiv.coe_subgroupMap_apply theorem

(e : G ≃* G') (H : Subgroup G) (g : H) : ((subgroupMap e H g : H.map (e : G →* G')) : G') = e g

Full source

@[to_additive (attr := simp)]
theorem coe_subgroupMap_apply (e : G ≃* G') (H : Subgroup G) (g : H) :
    ((subgroupMap e H g : H.map (e : G →* G')) : G') = e g :=
  rfl

Image of Subgroup Element under Induced Isomorphism Equals Original Image

Informal description

Let $G$ and $G'$ be groups, $e \colon G \simeq^* G'$ a group isomorphism, and $H$ a subgroup of $G$. For any element $g \in H$, the image of $g$ under the induced isomorphism $e \colon H \simeq^* e(H)$ equals $e(g)$ when viewed as an element of $G'$.

MulEquiv.subgroupMap_symm_apply theorem

 (e : G ≃* G') (H : Subgroup G) (g : H.map (e : G →* G')) :
  (e.subgroupMap H).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩

Full source

@[to_additive (attr := simp)]
theorem subgroupMap_symm_apply (e : G ≃* G') (H : Subgroup G) (g : H.map (e : G →* G')) :
    (e.subgroupMap H).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩ :=
  rfl

Inverse of Induced Subgroup Isomorphism Applied to Image Element

Informal description

Let $e \colon G \simeq^* G'$ be a group isomorphism, $H$ a subgroup of $G$, and $g$ an element of the image subgroup $e(H)$ in $G'$. Then the inverse of the induced isomorphism $e \colon H \simeq^* e(H)$ maps $g$ to $\langle e^{-1}(g), h \rangle$, where $h$ is a proof that $e^{-1}(g)$ belongs to $H$ (obtained via the equivalence between membership in the image and preimage under $e$).

MonoidHom.closure_preimage_le theorem

(f : G →* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f

Full source

@[to_additive]
theorem closure_preimage_le (f : G →* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  (closure_le _).2 fun x hx => by rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx

Subgroup Generated by Preimage is Contained in Preimage of Generated Subgroup

Informal description

Let $G$ and $N$ be groups, and let $f \colon G \to N$ be a group homomorphism. For any subset $s \subseteq N$, the subgroup generated by the preimage $f^{-1}(s)$ is contained in the preimage of the subgroup generated by $s$ under $f$. In other words, $\langle f^{-1}(s) \rangle \leq f^{-1}(\langle s \rangle)$.

MonoidHom.map_closure theorem

(f : G →* N) (s : Set G) : (closure s).map f = closure (f '' s)

Full source

/-- The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup
generated by the image of the set. -/
@[to_additive
      "The image under an `AddMonoid` hom of the `AddSubgroup` generated by a set equals
      the `AddSubgroup` generated by the image of the set."]
theorem map_closure (f : G →* N) (s : Set G) : (closure s).map f = closure (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subgroup.gi N).gc (Subgroup.gi G).gc
    fun _ ↦ rfl

Image of Generated Subgroup Equals Generated Image Subgroup

Informal description

Let $G$ and $N$ be groups and $f \colon G \to N$ a group homomorphism. For any subset $s \subseteq G$, the image under $f$ of the subgroup generated by $s$ equals the subgroup of $N$ generated by the image $f(s)$. In other words: \[ f(\langle s \rangle) = \langle f(s) \rangle \]

Subgroup.equivMapOfInjective_coe_mulEquiv theorem

(H : Subgroup G) (e : G ≃* G') : H.equivMapOfInjective (e : G →* G') (EquivLike.injective e) = e.subgroupMap H

Full source

@[to_additive (attr := simp)]
theorem equivMapOfInjective_coe_mulEquiv (H : Subgroup G) (e : G ≃* G') :
    H.equivMapOfInjective (e : G →* G') (EquivLike.injective e) = e.subgroupMap H := by
  ext
  rfl

Equivalence of Subgroup Isomorphism Constructions via Group Isomorphism

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $e : G \simeq^* G'$ a group isomorphism. Then the isomorphism between $H$ and its image under $e$ (considered as a homomorphism) coincides with the subgroup isomorphism induced by $e$ on $H$. In other words, the following diagram commutes: $$\begin{array}{ccc} H & \xrightarrow{\text{equivMapOfInjective}} & e(H) \\ & \searrow & \uparrow \\ & & \text{subgroupMap } e \end{array}$$ where $e(H)$ denotes the image of $H$ under the group homomorphism corresponding to $e$.

Mathlib.Algebra.Group.Subgroup.Map

Main definitions

Implementation notes

Tags