Normal subgroups and quotient groups

[Taneb]

Builds off #2852, continuing towards #2729 in bitesize chunks.

[jamesmckinna]

This all looks great. I've made suggestions, but nothing is a deal-breaker.

[jamesmckinna]

My personal preference is for π (for projection), echoing ι (for inclusion), but I won't fight for it...
... maybe I should?

[Taneb]

I've got no strong feeling here

[jamesmckinna]

Can simplify this to:

Suggested change

	private
	module N = NormalSubgroup N
	open NormalSubgroup N using (ι; module ι; conjugate; normal)
	private
	open module N = NormalSubgroup N using (ι; module ι; conjugate; normal)

[jamesmckinna]

I'd maybe be tempted to lift this out to Algebra.Construct.Quotient.AbelianGroup to bundle up the quotient-out-of-any-subgroup construction, and simplify the downstream imports in #2855 ?

[jamesmckinna]

Typo

Suggested change

	* `Algebra.Cosntruct.Quotient.Group` for the definition of quotient groups.
	* `Algebra.Construct.Quotient.Group` for the definition of quotient groups.

[jamesmckinna]

Naming?

Suggested change

	project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project
	project-isHomomorphism = record
	project-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project
	project-isGroupHomomorphism = record

Twofold reasons:

• Subsequently, for Ring R / Ideal I, you also define project-isHomomorphism : IsRingHomomorphism, and maybe that's enough (let the X path context of the algebra determine what kind of IsXHomomorphism is defined
• BUT, for Ring, what you actually need is to separate out the isMonoidHomomorphism field, so why not also isGroupHomomorphism?

[jamesmckinna]

This should be lifted out as a separate (prior) definition

project-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) project
project-isMagmaHomomorphism = record
  { isRelHomomorphism = record
    { cong = ≈⇒≋
    }
  ; homo = λ _ _ → ≋-refl
  }

project-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) project
project-isMonoidHomomorphism = record
  { isMagmaHomomorphism = project-isMagmaHomomorphism
  ; ε-homo = ≋-refl
  }

project-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project
project-isGroupHomomorphism = record
  { isMonoidHomomorphism = project-isMonoidHomomorphism
  ; ⁻¹-homo = λ _ → ≋-refl
  }

[jamesmckinna]

Unused!

[jamesmckinna]

Suggested change

	≈⇒≋ : _≈_ ⇒ _≋_
	≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y)

In view of the above refactoring of reflexivity...

[jamesmckinna]

Suggested change

	≋-refl : Reflexive _≋_
	≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x)
	≈⇒≋ : _≈_ ⇒ _≋_
	≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y)
	≋-refl : Reflexive _≋_
	≋-refl = ≈⇒≋ refl

Unsurprisingly, these proofs are definitionally equal to the previous versions, but put ≈⇒≋ ('abstract' reflexivity...) higher up the food chain.