Mathlib.Algebra.Quotient

Module docstring

{"# Algebraic quotients

This file defines notation for algebraic quotients, e.g. quotient groups G ⧸ H, quotient modules M ⧸ N and ideal quotients R ⧸ I.

The actual quotient structures are defined in the following files: * quotient group: Mathlib/GroupTheory/QuotientGroup.lean * quotient module: Mathlib/LinearAlgebra/Quotient.lean * quotient ring: Mathlib/RingTheory/Ideal/Quotient.lean

Notations

The following notation is introduced:

G ⧸ H stands for the quotient of the type G by some term H (for example, H can be a normal subgroup of G). To implement this notation for other quotients, you should provide a HasQuotient instance. Note that since G can usually be inferred from H, _ ⧸ H can also be used, but this is less readable.

Tags

quotient, group quotient, quotient group, module quotient, quotient module, ring quotient, ideal quotient, quotient ring "}

HasQuotient structure

(A : outParam <| Type u) (B : Type v)

Full source

/-- `HasQuotient A B` is a notation typeclass that allows us to write `A ⧸ b` for `b : B`.
This allows the usual notation for quotients of algebraic structures,
such as groups, modules and rings.

`A` is a parameter, despite being unused in the definition below, so it appears in the notation.
-/
class HasQuotient (A : outParam <| Type u) (B : Type v) where
  /-- auxiliary quotient function, the one used will have `A` explicit -/
  quotient' : B → Type max u v

Quotient Notation Typeclass

Informal description

The structure `HasQuotient A B` provides a notation typeclass that enables the use of the notation `A ⧸ b` for `b : B`, allowing standard algebraic quotient notations for structures like groups, modules, and rings. Here, `A` is a parameter (though unused in the definition) to ensure it appears in the notation.

HasQuotient.Quotient abbrev

(A : outParam <| Type u) {B : Type v} [HasQuotient A B] (b : B) : Type max u v

Full source

/-- `HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient
 of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is
 explicit, which is necessary to make Lean show the notation in the
 goal state.
-/
abbrev HasQuotient.Quotient (A : outParam <| Type u) {B : Type v}
    [HasQuotient A B] (b : B) : Type max u v :=
  HasQuotient.quotient' b

Quotient Type Notation $A ⧸ b$

Informal description

Given a type $A$ and a type $B$ with an instance of `HasQuotient A B`, the quotient of $A$ by an element $b : B$ is denoted by $A ⧸ b$ and represents the quotient type of $A$ modulo $b$.

term_⧸_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Quotient notation based on the `HasQuotient` typeclass -/
notation:35 G " ⧸ " H:34 => HasQuotient.Quotient G H

Quotient notation $ G ⧸ H $

Informal description

The notation $ G ⧸ H $ represents the quotient of the type $ G $ by the term $ H $, where $ H $ could be, for example, a normal subgroup of $ G $ or an ideal of $ G $. This notation is implemented using the `HasQuotient` typeclass, allowing it to be used for various algebraic quotients such as quotient groups, quotient modules, and quotient rings.