quotientToQuotientOfLE — Mathlib

English

Instance of MulAction on the carrier of X in Action.FintypeCat, induced by the underlying MulAction on X.

Русский

Инстанс MulAction на носителе X в Action.FintypeCat, индуцированный базовым MulAction на X.

LaTeX

$$$\text{MulAction } G\ (X.V)$$$

Lean4

/-- If `N` and `H` are subgroups of a group `G` with `N ≤ H`, this is the canonical
`G`-morphism `G ⧸ N ⟶ G ⧸ H`. -/
def quotientToQuotientOfLE [Fintype (G ⧸ H)] (h : N ≤ H) : (G ⧸ₐ N) ⟶ (G ⧸ₐ H)
    where
  hom :=
    Quotient.lift _ <| fun _ _ hab ↦
      Quotient.sound <| (QuotientGroup.leftRel_apply).mpr (h <| (QuotientGroup.leftRel_apply).mp hab)
  comm
    g := by
    ext (x : G ⧸ N)
    induction x using Quotient.inductionOn
    rfl

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