quotientMapSubgroupOfOfLe — Mathlib

English

If A' ≤ B' and A ≤ B, there is an induced map from A/(A'⊓A) to B/(B'⊓B).

Русский

Если A' ≤ B' и A ≤ B, то существует индуцированное отображение A/(A'⊓A) → B/(B'⊓B).

LaTeX

$$A ⧸ A'.subgroupOf A →* B ⧸ B'.subgroupOf B$$

Lean4

/-- Let `A', A, B', B` be subgroups of `G`. If `A' ≤ B'` and `A ≤ B`,
then there is a map `A / (A' ⊓ A) →* B / (B' ⊓ B)` induced by the inclusions. -/
@[to_additive /-- Let `A', A, B', B` be subgroups of `G`. If `A' ≤ B'` and `A ≤ B`, then there is a
    map `A / (A' ⊓ A) →+ B / (B' ⊓ B)` induced by the inclusions. -/
    ]
def quotientMapSubgroupOfOfLe {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal]
    [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) : A ⧸ A'.subgroupOf A →* B ⧸ B'.subgroupOf B :=
  map _ _ (Subgroup.inclusion h) <| Subgroup.comap_mono h'

Похожие утверждения