Mathlib.Algebra.Ring.CompTypeclasses

Module docstring

{"# Propositional typeclasses on several ring homs

This file contains three typeclasses used in the definition of (semi)linear maps: * RingHomId σ, which expresses the fact that σ₂₃ = id * RingHomCompTriple σ₁₂ σ₂₃ σ₁₃, which expresses the fact that σ₂₃.comp σ₁₂ = σ₁₃ * RingHomInvPair σ₁₂ σ₂₁, which states that σ₁₂ and σ₂₁ are inverses of each other * RingHomSurjective σ, which states that σ is surjective These typeclasses ensure that objects such as σ₂₃.comp σ₁₂ never end up in the type of a semilinear map; instead, the typeclass system directly finds the appropriate RingHom to use. A typical use-case is conjugate-linear maps, i.e. when σ = Complex.conj; this system ensures that composing two conjugate-linear maps is a linear map, and not a conj.comp conj-linear map.

Instances of these typeclasses mostly involving RingHom.id are also provided: * RingHomInvPair (RingHom.id R) (RingHom.id R) * [RingHomInvPair σ₁₂ σ₂₁] : RingHomCompTriple σ₁₂ σ₂₁ (RingHom.id R₁) * RingHomCompTriple (RingHom.id R₁) σ₁₂ σ₁₂ * RingHomCompTriple σ₁₂ (RingHom.id R₂) σ₁₂ * RingHomSurjective (RingHom.id R) * [RingHomInvPair σ₁ σ₂] : RingHomSurjective σ₁

Implementation notes

For the typeclass RingHomInvPair σ₁₂ σ₂₁, σ₂₁ is marked as an outParam, as it must typically be found via the typeclass inference system.
Likewise, for RingHomCompTriple σ₁₂ σ₂₃ σ₁₃, σ₁₃ is marked as an outParam, for the same reason.

Tags

RingHomCompTriple, RingHomInvPair, RingHomSurjective "}

RingHomId structure

{R : Type*} [Semiring R] (σ : R →+* R)

Full source

/-- Class that expresses that a ring homomorphism is in fact the identity. -/
-- This at first seems not very useful. However we need this when considering
-- modules over some diagram in the category of rings,
-- e.g. when defining presheaves over a presheaf of rings.
-- See `Mathlib.Algebra.Category.ModuleCat.Presheaf`.
class RingHomId {R : Type*} [Semiring R] (σ : R →+* R) : Prop where
  eq_id : σ = RingHom.id R

Identity Ring Homomorphism

Informal description

The structure `RingHomId σ` asserts that a given ring homomorphism $\sigma: R \to R$ is in fact the identity map on the semiring $R$.

instRingHomIdId instance

{R : Type*} [Semiring R] : RingHomId (RingHom.id R)

Full source

instance {R : Type*} [Semiring R] : RingHomId (RingHom.id R) where
  eq_id := rfl

Identity Ring Homomorphism is RingHomId

Informal description

For any semiring $R$, the identity ring homomorphism $\text{id}_R : R \to R$ satisfies the `RingHomId` property, meaning it is indeed the identity map on $R$.

RingHomCompTriple structure

(σ₁₂ : R₁ →+* R₂) (σ₂₃ : R₂ →+* R₃) (σ₁₃ : outParam (R₁ →+* R₃))

Full source

/-- Class that expresses the fact that three ring homomorphisms form a composition triple. This is
used to handle composition of semilinear maps. -/
class RingHomCompTriple (σ₁₂ : R₁ →+* R₂) (σ₂₃ : R₂ →+* R₃) (σ₁₃ : outParam (R₁ →+* R₃)) :
  Prop where
  /-- The morphisms form a commutative triangle -/
  comp_eq : σ₂₃.comp σ₁₂ = σ₁₃

Composition Triple of Ring Homomorphisms

Informal description

The structure `RingHomCompTriple` represents a composition triple of ring homomorphisms, where three ring homomorphisms $\sigma_{12} : R_1 \to R_2$, $\sigma_{23} : R_2 \to R_3$, and $\sigma_{13} : R_1 \to R_3$ satisfy the composition property $\sigma_{23} \circ \sigma_{12} = \sigma_{13}$. This is used to handle composition of semilinear maps in a way that avoids explicit composition in the type signatures.

RingHomCompTriple.comp_apply theorem

[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {x : R₁} : σ₂₃ (σ₁₂ x) = σ₁₃ x

Full source

@[simp]
theorem comp_apply [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {x : R₁} : σ₂₃ (σ₁₂ x) = σ₁₃ x :=
  RingHom.congr_fun comp_eq x

Composition Property of Ring Homomorphism Triples: $\sigma_{23}(\sigma_{12}(x)) = \sigma_{13}(x)$

Informal description

Given ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$, $\sigma_{23} \colon R_2 \to R_3$, and $\sigma_{13} \colon R_1 \to R_3$ that form a `RingHomCompTriple` (i.e., $\sigma_{23} \circ \sigma_{12} = \sigma_{13}$), then for any element $x \in R_1$, we have $\sigma_{23}(\sigma_{12}(x)) = \sigma_{13}(x)$.

RingHomInvPair structure

(σ : R₁ →+* R₂) (σ' : outParam (R₂ →+* R₁))

Full source

/-- Class that expresses the fact that two ring homomorphisms are inverses of each other. This is
used to handle `symm` for semilinear equivalences. -/
class RingHomInvPair (σ : R₁ →+* R₂) (σ' : outParam (R₂ →+* R₁)) : Prop where
  /-- `σ'` is a left inverse of `σ` -/
  comp_eq : σ'.comp σ = RingHom.id R₁
  /-- `σ'` is a left inverse of `σ'` -/
  comp_eq₂ : σ.comp σ' = RingHom.id R₂

Inverse Pair of Ring Homomorphisms

Informal description

A structure that asserts two ring homomorphisms $\sigma \colon R_1 \to R_2$ and $\sigma' \colon R_2 \to R_1$ are mutual inverses, meaning $\sigma' \circ \sigma = \text{id}_{R_1}$ and $\sigma \circ \sigma' = \text{id}_{R_2}$. This is used to handle symmetry in semilinear equivalences.

RingHomInvPair.comp_apply_eq theorem

{x : R₁} : σ' (σ x) = x

Full source

theorem comp_apply_eq {x : R₁} : σ' (σ x) = x := by
  rw [← RingHom.comp_apply, comp_eq]
  simp

Inverse Property of Ring Homomorphism Pair: $\sigma' \circ \sigma = \text{id}$

Informal description

For any element $x$ in a semiring $R_1$, if $\sigma \colon R_1 \to R_2$ and $\sigma' \colon R_2 \to R_1$ form an inverse pair of ring homomorphisms, then the composition $\sigma' \circ \sigma$ acts as the identity on $x$, i.e., $\sigma'(\sigma(x)) = x$.

RingHomInvPair.comp_apply_eq₂ theorem

{x : R₂} : σ (σ' x) = x

Full source

theorem comp_apply_eq₂ {x : R₂} : σ (σ' x) = x := by
  rw [← RingHom.comp_apply, comp_eq₂]
  simp

Inverse Property of Ring Homomorphism Pair: $\sigma \circ \sigma' = \text{id}$

Informal description

For any element $x$ in a semiring $R_2$, if $\sigma \colon R_1 \to R_2$ and $\sigma' \colon R_2 \to R_1$ form an inverse pair of ring homomorphisms, then the composition $\sigma \circ \sigma'$ acts as the identity on $x$, i.e., $\sigma(\sigma'(x)) = x$.

RingHomInvPair.ids instance

: RingHomInvPair (RingHom.id R₁) (RingHom.id R₁)

Full source

instance ids : RingHomInvPair (RingHom.id R₁) (RingHom.id R₁) :=
  ⟨rfl, rfl⟩

Identity Ring Homomorphism is Self-Inverse

Informal description

The identity ring homomorphism $\text{id}_{R_1} \colon R_1 \to R_1$ forms an inverse pair with itself. That is, $\text{id}_{R_1} \circ \text{id}_{R_1} = \text{id}_{R_1}$.

RingHomInvPair.triples instance

{σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] : RingHomCompTriple σ₁₂ σ₂₁ (RingHom.id R₁)

Full source

instance triples {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] :
    RingHomCompTriple σ₁₂ σ₂₁ (RingHom.id R₁) :=
  ⟨by simp only [comp_eq]⟩

Composition Triple from Inverse Pair of Ring Homomorphisms

Informal description

For any ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{21} \colon R_2 \to R_1$ that form an inverse pair (i.e., $\sigma_{21} \circ \sigma_{12} = \text{id}_{R_1}$ and $\sigma_{12} \circ \sigma_{21} = \text{id}_{R_2}$), the composition $\sigma_{21} \circ \sigma_{12}$ forms a composition triple with the identity homomorphism $\text{id}_{R_1}$.

RingHomInvPair.triples₂ instance

{σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] : RingHomCompTriple σ₂₁ σ₁₂ (RingHom.id R₂)

Full source

instance triples₂ {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] :
    RingHomCompTriple σ₂₁ σ₁₂ (RingHom.id R₂) :=
  ⟨by simp only [comp_eq₂]⟩

Composition of Inverse Ring Homomorphisms Yields Identity

Informal description

For any pair of ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{21} \colon R_2 \to R_1$ that are mutual inverses, the composition $\sigma_{12} \circ \sigma_{21}$ is the identity homomorphism on $R_2$.

RingHomInvPair.of_ringEquiv theorem

(e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm

Full source

/-- Construct a `RingHomInvPair` from both directions of a ring equiv.

This is not an instance, as for equivalences that are involutions, a better instance
would be `RingHomInvPair e e`. Indeed, this declaration is not currently used in mathlib.
-/
theorem of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm :=
  ⟨e.symm_toRingHom_comp_toRingHom, e.symm.symm_toRingHom_comp_toRingHom⟩

Ring Isomorphism Yields Inverse Pair of Ring Homomorphisms

Informal description

Given a ring isomorphism $e \colon R_1 \simeq^{+*} R_2$ between semirings $R_1$ and $R_2$, the pair consisting of $e$ (as a ring homomorphism) and its inverse $e^{-1}$ (as a ring homomorphism) forms an inverse pair of ring homomorphisms. That is, $e^{-1} \circ e = \text{id}_{R_1}$ and $e \circ e^{-1} = \text{id}_{R_2}$.

RingHomInvPair.symm theorem

 (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁) [RingHomInvPair σ₁₂ σ₂₁] : RingHomInvPair σ₂₁ σ₁₂

Full source

/--
Swap the direction of a `RingHomInvPair`. This is not an instance as it would loop, and better
instances are often available and may often be preferable to using this one. Indeed, this
declaration is not currently used in mathlib.
-/
theorem symm (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁) [RingHomInvPair σ₁₂ σ₂₁] :
    RingHomInvPair σ₂₁ σ₁₂ :=
  ⟨RingHomInvPair.comp_eq₂, RingHomInvPair.comp_eq⟩

Symmetry of Inverse Ring Homomorphism Pairs

Informal description

Given ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{21} \colon R_2 \to R_1$ that form an inverse pair (i.e., $\sigma_{21} \circ \sigma_{12} = \text{id}_{R_1}$ and $\sigma_{12} \circ \sigma_{21} = \text{id}_{R_2}$), then $\sigma_{21}$ and $\sigma_{12}$ also form an inverse pair.

RingHomCompTriple.ids instance

: RingHomCompTriple (RingHom.id R₁) σ₁₂ σ₁₂

Full source

instance ids : RingHomCompTriple (RingHom.id R₁) σ₁₂ σ₁₂ :=
  ⟨by
    ext
    simp⟩

Identity Ring Homomorphism in Composition Triple

Informal description

For any ring homomorphism $\sigma_{12} : R_1 \to R_2$, the composition of the identity homomorphism $\mathrm{id}_{R_1}$ with $\sigma_{12}$ is equal to $\sigma_{12}$ itself.

RingHomCompTriple.right_ids instance

: RingHomCompTriple σ₁₂ (RingHom.id R₂) σ₁₂

Full source

instance right_ids : RingHomCompTriple σ₁₂ (RingHom.id R₂) σ₁₂ :=
  ⟨by
    ext
    simp⟩

Right Identity Composition for Ring Homomorphisms

Informal description

For any ring homomorphism $\sigma_{12} : R_1 \to R_2$, the composition $\sigma_{12} \circ \text{id}_{R_2}$ equals $\sigma_{12}$ itself, where $\text{id}_{R_2}$ is the identity ring homomorphism on $R_2$.

RingHomSurjective structure

(σ : R₁ →+* R₂)

Full source

/-- Class expressing the fact that a `RingHom` is surjective. This is needed in the context
of semilinear maps, where some lemmas require this. -/
class RingHomSurjective (σ : R₁ →+* R₂) : Prop where
  /-- The ring homomorphism is surjective -/
  is_surjective : Function.Surjective σ

Surjective semiring homomorphism

Informal description

The structure `RingHomSurjective` expresses the property that a semiring homomorphism $\sigma: R_1 \to R_2$ is surjective. This is used in the context of semilinear maps where certain lemmas require surjectivity of the underlying ring homomorphism.

RingHom.surjective theorem

(σ : R₁ →+* R₂) [t : RingHomSurjective σ] : Function.Surjective σ

Full source

theorem RingHom.surjective (σ : R₁ →+* R₂) [t : RingHomSurjective σ] : Function.Surjective σ :=
  t.is_surjective

Surjectivity of Semiring Homomorphisms with `RingHomSurjective` Property

Informal description

Let $\sigma: R_1 \to R_2$ be a semiring homomorphism that is surjective (i.e., satisfies the `RingHomSurjective` property). Then $\sigma$ is a surjective function, meaning for every $y \in R_2$, there exists $x \in R_1$ such that $\sigma(x) = y$.

RingHomSurjective.invPair instance

{σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁} [RingHomInvPair σ₁ σ₂] : RingHomSurjective σ₁

Full source

instance (priority := 100) invPair {σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁} [RingHomInvPair σ₁ σ₂] :
    RingHomSurjective σ₁ :=
  ⟨fun x => ⟨σ₂ x, RingHomInvPair.comp_apply_eq₂⟩⟩

Surjectivity of Ring Homomorphisms in Inverse Pairs

Informal description

For any pair of ring homomorphisms $\sigma_1 \colon R_1 \to R_2$ and $\sigma_2 \colon R_2 \to R_1$ that are mutual inverses (i.e., $\sigma_2 \circ \sigma_1 = \text{id}_{R_1}$ and $\sigma_1 \circ \sigma_2 = \text{id}_{R_2}$), the homomorphism $\sigma_1$ is surjective.

RingHomSurjective.ids instance

: RingHomSurjective (RingHom.id R₁)

Full source

instance ids : RingHomSurjective (RingHom.id R₁) :=
  ⟨is_surjective⟩

Surjectivity of the Identity Ring Homomorphism

Informal description

The identity ring homomorphism $\text{id}_{R_1} \colon R_1 \to R_1$ is surjective.

RingHomSurjective.comp theorem

 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂] [RingHomSurjective σ₂₃] : RingHomSurjective σ₁₃

Full source

/-- This cannot be an instance as there is no way to infer `σ₁₂` and `σ₂₃`. -/
theorem comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂] [RingHomSurjective σ₂₃] :
    RingHomSurjective σ₁₃ :=
  { is_surjective := by
      have := σ₂₃.surjective.comp σ₁₂.surjective
      rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this }

Surjectivity of Composed Ring Homomorphisms

Informal description

Let $R_1$, $R_2$, and $R_3$ be semirings with ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{23} \colon R_2 \to R_3$ such that their composition $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$ is well-defined (i.e., they form a `RingHomCompTriple`). If both $\sigma_{12}$ and $\sigma_{23}$ are surjective, then their composition $\sigma_{13}$ is also surjective.

RingHomSurjective.instToRingHomRingEquiv instance

(σ : R₁ ≃+* R₂) : RingHomSurjective (σ : R₁ →+* R₂)

Full source

instance (σ : R₁ ≃+* R₂) : RingHomSurjective (σ : R₁ →+* R₂) := ⟨σ.surjective⟩

Ring Equivalences Induce Surjective Ring Homomorphisms

Informal description

For any ring equivalence $\sigma: R_1 \simeq+* R_2$ between semirings $R_1$ and $R_2$, the underlying ring homomorphism $\sigma: R_1 \to R_2$ is surjective.