Evaluating the first isomorphism theorem on a class

Mathlib packages the first isomorphism theorem for a surjective homomorphism φ : G →* M as QuotientGroup.quotientKerEquivOfSurjective φ hφ : G ⧸ φ.ker ≃* M. It is defined through QuotientGroup.quotientKerEquivOfRightInverse applied to a right inverse extracted from hφ by choice, so evaluating it on a class otherwise means unfolding that noncomputable implementation. Likewise, QuotientGroup.quotientKerEquivRange φ : G ⧸ φ.ker ≃* φ.range is built with MulEquiv.ofBijective from QuotientGroup.rangeKerLift, and Mathlib states no evaluation rule for it.

This file records the computation rules on classes, so that users never have to. The first is the group-theoretic counterpart of Mathlib's RingHom.quotientKerEquivOfSurjective_apply_mk; both belong beside their definitions in Mathlib.

Main statements

• TauCeti.QuotientGroup.quotientKerEquivOfSurjective_apply_mk: the isomorphism G ⧸ φ.ker ≃* M sends the class of g to φ g; its additive counterpart is TauCeti.QuotientAddGroup.quotientKerEquivOfSurjective_apply_mk.
• TauCeti.QuotientGroup.quotientKerEquivRange_apply_mk: the isomorphism G ⧸ φ.ker ≃* φ.range sends the class of g to φ g; its additive counterpart is TauCeti.QuotientAddGroup.quotientKerEquivRange_apply_mk.

@[simp]

theorem TauCeti.QuotientGroup.quotientKerEquivOfSurjective_apply_mk {G : Type u_1} {M : Type u_2} [Group G] [Group M] (φ : G →* M) (hφ : Function.Surjective ⇑φ) (g : G) : (QuotientGroup.quotientKerEquivOfSurjective φ hφ) ↑g = φ g

The first isomorphism theorem for a surjective homomorphism sends the class of g to φ g.

@[simp]

theorem TauCeti.QuotientAddGroup.quotientKerEquivOfSurjective_apply_mk {G : Type u_1} {M : Type u_2} [AddGroup G] [AddGroup M] (φ : G →+ M) (hφ : Function.Surjective ⇑φ) (g : G) : (QuotientAddGroup.quotientKerEquivOfSurjective φ hφ) ↑g = φ g

The first isomorphism theorem for a surjective additive homomorphism sends the class of g to φ g.

@[simp]

theorem TauCeti.QuotientGroup.quotientKerEquivRange_apply_mk {G : Type u_1} {M : Type u_2} [Group G] [Group M] (φ : G →* M) (g : G) : (QuotientGroup.quotientKerEquivRange φ) ↑g = ⟨φ g, ⋯⟩

The first isomorphism theorem onto the range sends the class of g to φ g.

@[simp]

theorem TauCeti.QuotientAddGroup.quotientKerEquivRange_apply_mk {G : Type u_1} {M : Type u_2} [AddGroup G] [AddGroup M] (φ : G →+ M) (g : G) : (QuotientAddGroup.quotientKerEquivRange φ) ↑g = ⟨φ g, ⋯⟩

The first isomorphism theorem onto the range of an additive homomorphism sends the class of g to φ g.