Finite-index normal subgroups

This file builds the lattice FiniteIndexNormalSubgroup G of finite-index normal subgroups of a group G, and its additive version FiniteIndexNormalAddSubgroup.

This is used primarily in the definition of the profinite completion of a group.

structure FiniteIndexNormalSubgroup (G : Type u_1) [Group G] extends Subgroup G : Type u_1

The type of finite-index normal subgroups of a group.

• carrier : Set G
• mul_mem' {a b : G} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• inv_mem' {x : G} : x ∈ self.carrier → x⁻¹ ∈ self.carrier
• isNormal' : self.Normal
• isFiniteIndex' : self.FiniteIndex

theorem FiniteIndexNormalSubgroup.ext {G : Type u_1} {inst✝ : Group G} {x y : FiniteIndexNormalSubgroup G} (carrier : x.carrier = y.carrier) : x = y

theorem FiniteIndexNormalSubgroup.ext_iff {G : Type u_1} {inst✝ : Group G} {x y : FiniteIndexNormalSubgroup G} : x = y ↔ x.carrier = y.carrier

structure FiniteIndexNormalAddSubgroup (G : Type u_1) [AddGroup G] extends AddSubgroup G : Type u_1

The type of finite-index normal additive subgroups of an additive group.

• carrier : Set G
• add_mem' {a b : G} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• neg_mem' {x : G} : x ∈ self.carrier → -x ∈ self.carrier
• isNormal' : self.Normal
• isFiniteIndex' : self.FiniteIndex

theorem FiniteIndexNormalAddSubgroup.ext {G : Type u_1} {inst✝ : AddGroup G} {x y : FiniteIndexNormalAddSubgroup G} (carrier : x.carrier = y.carrier) : x = y

theorem FiniteIndexNormalAddSubgroup.ext_iff {G : Type u_1} {inst✝ : AddGroup G} {x y : FiniteIndexNormalAddSubgroup G} : x = y ↔ x.carrier = y.carrier

theorem FiniteIndexNormalSubgroup.toSubgroup_injective {G : Type u_1} [Group G] : Function.Injective fun (H : FiniteIndexNormalSubgroup G) => H.toSubgroup

theorem FiniteIndexNormalAddSubgroup.toAddSubgroup_injective {G : Type u_1} [AddGroup G] : Function.Injective fun (H : FiniteIndexNormalAddSubgroup G) => H.toAddSubgroup

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instSetLike {G : Type u_1} [Group G] : SetLike (FiniteIndexNormalSubgroup G) G

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instSetLike {G : Type u_1} [AddGroup G] : SetLike (FiniteIndexNormalAddSubgroup G) G

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instPartialOrder {G : Type u_1} [Group G] : PartialOrder (FiniteIndexNormalSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instPartialOrder {G : Type u_1} [AddGroup G] : PartialOrder (FiniteIndexNormalAddSubgroup G)

instance FiniteIndexNormalSubgroup.instSubgroupClass {G : Type u_1} [Group G] : SubgroupClass (FiniteIndexNormalSubgroup G) G

instance FiniteIndexNormalAddSubgroup.instAddSubgroupClass {G : Type u_1} [AddGroup G] : AddSubgroupClass (FiniteIndexNormalAddSubgroup G) G

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instCoeSubgroup {G : Type u_1} [Group G] : Coe (FiniteIndexNormalSubgroup G) (Subgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instCoeAddSubgroup {G : Type u_1} [AddGroup G] : Coe (FiniteIndexNormalAddSubgroup G) (AddSubgroup G)

instance FiniteIndexNormalSubgroup.instNormal {G : Type u_1} [Group G] (H : FiniteIndexNormalSubgroup G) : H.Normal

instance FiniteIndexNormalAddSubgroup.instNormal {G : Type u_1} [AddGroup G] (H : FiniteIndexNormalAddSubgroup G) : H.Normal

instance FiniteIndexNormalSubgroup.instFiniteIndex {G : Type u_1} [Group G] (H : FiniteIndexNormalSubgroup G) : H.FiniteIndex

instance FiniteIndexNormalAddSubgroup.instFiniteIndex {G : Type u_1} [AddGroup G] (H : FiniteIndexNormalAddSubgroup G) : H.FiniteIndex

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instPartialOrderFiniteIndexNormalSubgroup {G : Type u_1} [Group G] : PartialOrder (FiniteIndexNormalSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instPartialOrderFiniteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] : PartialOrder (FiniteIndexNormalAddSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instInfFiniteIndexNormalSubgroup {G : Type u_1} [Group G] : Min (FiniteIndexNormalSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instInfFiniteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] : Min (FiniteIndexNormalAddSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instSemilatticeInfFiniteIndexNormalSubgroup {G : Type u_1} [Group G] : SemilatticeInf (FiniteIndexNormalSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instSemilatticeInfFiniteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] : SemilatticeInf (FiniteIndexNormalAddSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instMax {G : Type u_1} [Group G] : Max (FiniteIndexNormalSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instMax {G : Type u_1} [AddGroup G] : Max (FiniteIndexNormalAddSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instSemilatticeSupFiniteIndexNormalSubgroup {G : Type u_1} [Group G] : SemilatticeSup (FiniteIndexNormalSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instSemilatticeSupFiniteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] : SemilatticeSup (FiniteIndexNormalAddSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalSubgroup.instLattice {G : Type u_1} [Group G] : Lattice (FiniteIndexNormalSubgroup G)

@[implicit_reducible]

instance FiniteIndexNormalAddSubgroup.instLattice {G : Type u_1} [AddGroup G] : Lattice (FiniteIndexNormalAddSubgroup G)

theorem FiniteIndexNormalSubgroup.mem_toSubgroup_iff {G : Type u_1} [Group G] {H : FiniteIndexNormalSubgroup G} {g : G} : g ∈ H.toSubgroup ↔ g ∈ H

theorem FiniteIndexNormalAddSubgroup.mem_toAddSubgroup_iff {G : Type u_1} [AddGroup G] {H : FiniteIndexNormalAddSubgroup G} {g : G} : g ∈ H.toAddSubgroup ↔ g ∈ H

def FiniteIndexNormalSubgroup.ofSubgroup {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [H.FiniteIndex] : FiniteIndexNormalSubgroup G

Bundle a subgroup with typeclass assumptions of normality and finite index.

def FiniteIndexNormalAddSubgroup.ofAddSubgroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] [H.FiniteIndex] : FiniteIndexNormalAddSubgroup G

Bundle an additive subgroup with typeclass assumptions of normality and finite index.

@[simp]

theorem FiniteIndexNormalSubgroup.toSubgroup_ofSubgroup {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [H.FiniteIndex] : (ofSubgroup H).toSubgroup = H

@[simp]

theorem FiniteIndexNormalAddSubgroup.toAddSubgroup_ofAddSubgroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] [H.FiniteIndex] : (ofAddSubgroup H).toAddSubgroup = H

def FiniteIndexNormalSubgroup.comap {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (K : FiniteIndexNormalSubgroup H) : FiniteIndexNormalSubgroup G

The preimage of a finite-index normal subgroup under a group homomorphism.

def FiniteIndexNormalAddSubgroup.comap {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) (K : FiniteIndexNormalAddSubgroup H) : FiniteIndexNormalAddSubgroup G

The preimage of a finite-index normal additive subgroup under an additive homomorphism.

@[simp]

theorem FiniteIndexNormalSubgroup.toSubgroup_comap {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (K : FiniteIndexNormalSubgroup H) : (comap f K).toSubgroup = Subgroup.comap f K.toSubgroup

@[simp]

theorem FiniteIndexNormalAddSubgroup.toAddSubgroup_comap {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) (K : FiniteIndexNormalAddSubgroup H) : (comap f K).toAddSubgroup = AddSubgroup.comap f K.toAddSubgroup

theorem FiniteIndexNormalSubgroup.comap_mono {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) {K L : FiniteIndexNormalSubgroup H} (h : K ≤ L) : comap f K ≤ comap f L

theorem FiniteIndexNormalAddSubgroup.comap_mono {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) {K L : FiniteIndexNormalAddSubgroup H} (h : K ≤ L) : comap f K ≤ comap f L

@[simp]

theorem FiniteIndexNormalSubgroup.comap_id {G : Type u_1} [Group G] (K : FiniteIndexNormalSubgroup G) : comap (MonoidHom.id G) K = K

@[simp]

theorem FiniteIndexNormalAddSubgroup.comap_id {G : Type u_1} [AddGroup G] (K : FiniteIndexNormalAddSubgroup G) : comap (AddMonoidHom.id G) K = K

@[simp]

theorem FiniteIndexNormalSubgroup.comap_comp {G : Type u_1} [Group G] {H : Type u_2} {N : Type u_3} [Group H] [Group N] (f : G →* H) (g : H →* N) (K : FiniteIndexNormalSubgroup N) : comap (g.comp f) K = comap f (comap g K)

@[simp]

theorem FiniteIndexNormalAddSubgroup.comap_comp {G : Type u_1} [AddGroup G] {H : Type u_2} {N : Type u_3} [AddGroup H] [AddGroup N] (f : G →+ H) (g : H →+ N) (K : FiniteIndexNormalAddSubgroup N) : comap (g.comp f) K = comap f (comap g K)