quotientKerEquivOfRightInverse — Mathlib

English

Given ψ : H → G with hφ: RightInverse ψ φ, there is a MulEquiv G/ker φ ≃* H.

Русский

Дано ψ : H → G такое, что ψ является правой обратной к φ, существует мультиэквивиал между G/ker φ и H.

LaTeX

$$$G/\\ker φ \\simeq* H$ with inverse given by $mk \\circ ψ$$$

Lean4

/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a homomorphism `φ : G →* H`
with a right inverse `ψ : H → G`. -/
@[to_additive (attr := simps) /-- The canonical isomorphism `G/(ker φ) ≃+ H` induced by a
    homomorphism `φ : G →+ H` with a right inverse `ψ : H → G`. -/
    ]
def quotientKerEquivOfRightInverse (ψ : H → G) (hφ : RightInverse ψ φ) : G ⧸ ker φ ≃* H :=
  { kerLift φ with
    toFun := kerLift φ
    invFun := mk ∘ ψ
    left_inv := fun x => kerLift_injective φ (by rw [Function.comp_apply, kerLift_mk', hφ])
    right_inv := hφ }

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