Add ideals and quotient rings

[Taneb]

Add definition of ideals and quotient rings. Based on #2854. Taken from #2729

[jamesmckinna]

All looks good. Lots of stylistic nitpicking though!

[jamesmckinna]

I'd put the comment above the record declaration, and even embellish it to:

Suggested change

	record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
	field
	-- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself
	------------------------------------------------------------------------
	-- Definition
	-- a (two-sided) ideal is exactly a sub-bimodule of R considered as a bimodule over itself
	record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
	field

[jamesmckinna]

I personally find the parametrisation in TensorUnit to make this kind of thing more ugly to read than is wholly necessary (I'd perhaps downstream even reconsider some of the implicit vs. explicit quantification there), and, because Subbimodule already takes an {R : Ring _ _} parameter, I'd be tempted to write instead:

Suggested change

	subbimodule : Subbimodule (TU.bimodule {R = R}) c′ ℓ′
	subbimodule : Subbimodule {R = R} (TU.bimodule) c′ ℓ′

which would then permit the earlier import of TU to actually be handled in place as

open import Algebra.Module.Construct.TensorUnit using (bimodule)

I'd even be tempted to go further: conventionally, the canonical name for the tensor unit (wrt whatever tensor product structure) is \bI, so I'd even make this a renaming import

open import Algebra.Module.Construct.TensorUnit renaming (bimodule to 𝕀)

but this is being hyper-nitpicky! (maybe!?)

[jamesmckinna]

Given that any Algebra.Construct.Quotient module is going to take two explicit parameters

• the thing-to-be-quotiented
• the thing-to-be-quotiented-by

I'd like it if each such module declared for public export a binary infix

module _/_ = ...

with definiens the bundle being defined, so that one could instead here write

Suggested change

	open Ring R
	private module I = Ideal I
	open I using (ι; normalSubgroup)
	open import Algebra.Construct.Quotient.Group +-group normalSubgroup public
	using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup; project; project-surjective)
	renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong)
	open import Algebra.Construct.Quotient.Group using (module _/_)
	private
	module R = Ring R
	module I = Ideal I
	module R/I = R.+-group / I.normalSubgroup
	open R
	open I using (ι)
	open R/I public
	using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup; project; project-surjective)
	renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong)

etc.
(obviously some further nitpicking need to localise what else of R gets used, so maybe the full open R is not actually called for?)

[JacquesCarette]

I support that idea.

[jamesmckinna]

A pity that we don't (yet) have it so that the second presupposes the first cf. #2804 ?

[jamesmckinna]

Ditto. should this be part of the API exported by Algebra.Properties.X? Do we ever invoke algebraic properties not in a context where we have access to equational reasoning wrt that algebra?

[jamesmckinna]

Unused, AFAICT?

[jamesmckinna]

Should be bumped up above the private block?

[JacquesCarette]

We're a picky bunch... nice stuff!

[JacquesCarette]

I would be tempted to use a local module (I forget the syntax for doing just inside the proof part) where I is opened so that all these qualifiers can go away. It's an idiom used a lot in 1lab that I need to integrate into my own Agda.

[JacquesCarette]

as this is 'just' a pair, use _,_ instead of a record? And maybe also eta contract?

[JacquesCarette]

_,_ would work here too (but not eta)

[jamesmckinna]

You can, somewhat counterintuitively, simplify this to

Suggested change

	private module I = Ideal I
	open I using (ι; normalSubgroup)
	private open module I = Ideal I using (ι; normalSubgroup)