English
For a family of subgroups f i of α and a fixed H, the quotient by the infimum embeds into the product over i of quotients by each (f i).subgroupOf H.
Русский
Для семейства подгрупп f_i группы α и фиксированного H, факторгруппа по инфиму embeds в произведение по i от факторгрупп по каждой (f_i).subgroupOf H.
LaTeX
$$$H \\!\\! / \\!\\! (\\bigwedge_i (f_i)) \\text{subgroupOf } H \\hookrightarrow \\prod_i (H \\!\\! / \\!\\! (f_i).subgroupOf H)$$$
Lean4
/-- The natural embedding `α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i`. -/
@[to_additive (attr := simps) /-- The natural embedding `α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i`. -/
]
def quotientiInfEmbedding {ι : Type*} (f : ι → Subgroup α) : (α ⧸ ⨅ i, f i) ↪ ∀ i, α ⧸ f i
where
toFun q i := quotientMapOfLE (iInf_le f i) q
inj' :=
Quotient.ind₂' <| by
simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self, forall_const]
