English
The natural embedding sends the quotient by the infimum of a family of subgroups into the space of functions indexed by the index set, with each coordinate being a quotient by the corresponding subgroup.
Русский
Естественное вложение переводит факторгруппу по пересечению подгрупп (инфинуму) в пространство функций, индексированное индексным множеством, где каждая координата — факторгруппа по соответствующей подгруппе.
LaTeX
$$$H \\!\\! / \\!\\! (\\bigwedge_i f_i) \\text{subgroupOf } H \\hookrightarrow \\forall i, H \\!\\! / \\!\\! (f_i).subgroupOf H$$$
Lean4
/-- The natural embedding `H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H`. -/
@[to_additive (attr := simps) /-- The natural embedding
`H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H`. -/
]
def quotientiInfSubgroupOfEmbedding {ι : Type*} (f : ι → Subgroup α) (H : Subgroup α) :
H ⧸ (⨅ i, f i).subgroupOf H ↪ ∀ i, H ⧸ (f i).subgroupOf H
where
toFun q i := quotientSubgroupOfMapOfLE H (iInf_le f i) q
inj' :=
Quotient.ind₂' <| by
simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf, mem_iInf, imp_self,
forall_const]
