Documentation

Mathlib.Algebra.Ring.CompTypeclasses

Propositional typeclasses on several ring homs #

This file contains three typeclasses used in the definition of (semi)linear maps:

Instances of these typeclasses mostly involving RingHom.id are also provided:

Implementation notes #

Tags #

RingHomCompTriple, RingHomInvPair, RingHomSurjective

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

Class that expresses that a ring homomorphism is in fact the identity.

Instances
    class RingHomCompTriple {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] (σ₁₂ : R₁ →+* R₂) (σ₂₃ : R₂ →+* R₃) (σ₁₃ : outParam (R₁ →+* R₃)) :

    Class that expresses the fact that three ring homomorphisms form a composition triple. This is used to handle composition of semilinear maps.

    • comp_eq : RingHom.comp σ₂₃ σ₁₂ = σ₁₃

      The morphisms form a commutative triangle

    Instances
      @[simp]
      theorem RingHomCompTriple.comp_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {x : R₁} :
      σ₂₃ (σ₁₂ x) = σ₁₃ x
      class RingHomInvPair {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ →+* R₂) (σ' : outParam (R₂ →+* R₁)) :

      Class that expresses the fact that two ring homomorphisms are inverses of each other. This is used to handle symm for semilinear equivalences.

      Instances
        theorem RingHomInvPair.comp_apply_eq {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ : R₁ →+* R₂} {σ' : R₂ →+* R₁} [RingHomInvPair σ σ'] {x : R₁} :
        σ' (σ x) = x
        theorem RingHomInvPair.comp_apply_eq₂ {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ : R₁ →+* R₂} {σ' : R₂ →+* R₁} [RingHomInvPair σ σ'] {x : R₂} :
        σ (σ' x) = x
        instance RingHomInvPair.ids {R₁ : Type u_1} [Semiring R₁] :
        Equations
        instance RingHomInvPair.triples {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] :
        RingHomCompTriple σ₁₂ σ₂₁ (RingHom.id R₁)
        Equations
        instance RingHomInvPair.triples₂ {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] :
        RingHomCompTriple σ₂₁ σ₁₂ (RingHom.id R₂)
        Equations
        @[reducible]
        theorem RingHomInvPair.of_ringEquiv {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (e : R₁ ≃+* R₂) :

        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.

        See note [reducible non-instances].

        @[reducible]
        theorem RingHomInvPair.symm {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁) [RingHomInvPair σ₁₂ σ₂₁] :
        RingHomInvPair σ₂₁ σ₁₂

        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 preferrable to using this one. Indeed, this declaration is not currently used in mathlib.

        See note [reducible non-instances].

        instance RingHomCompTriple.ids {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} :
        RingHomCompTriple (RingHom.id R₁) σ₁₂ σ₁₂
        Equations
        instance RingHomCompTriple.right_ids {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} :
        RingHomCompTriple σ₁₂ (RingHom.id R₂) σ₁₂
        Equations
        class RingHomSurjective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ →+* R₂) :

        Class expressing the fact that a RingHom is surjective. This is needed in the context of semilinear maps, where some lemmas require this.

        Instances
          theorem RingHom.surjective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ →+* R₂) [t : RingHomSurjective σ] :
          instance RingHomSurjective.invPair {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁} [RingHomInvPair σ₁ σ₂] :
          Equations
          theorem RingHomSurjective.comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂] [RingHomSurjective σ₂₃] :

          This cannot be an instance as there is no way to infer σ₁₂ and σ₂₃.