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
    theorem RingHomId.eq_id {R : Type u_4} [Semiring R] {σ : R →+* R} [self : RingHomId σ] :
    instance instRingHomIdId {R : Type u_4} [Semiring R] :
    Equations
    • =
    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 : σ₂₃.comp σ₁₂ = σ₁₃

      The morphisms form a commutative triangle

    Instances
      @[simp]
      theorem RingHomCompTriple.comp_eq {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₃)} [self : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] :
      σ₂₃.comp σ₁₂ = σ₁₃

      The morphisms form a commutative triangle

      @[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_eq {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ : R₁ →+* R₂} {σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'] :

        σ' is a left inverse of σ

        theorem RingHomInvPair.comp_eq₂ {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ : R₁ →+* R₂} {σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'] :
        σ.comp σ' = RingHom.id R₂

        σ' is a left inverse of σ'

        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
        • =
        theorem RingHomInvPair.of_ringEquiv {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (e : R₁ ≃+* R₂) :
        RingHomInvPair e e.symm

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

        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 RingHomSurjective.is_surjective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ : R₁ →+* R₂} [self : RingHomSurjective σ] :

          The ring homomorphism is surjective

          theorem RingHom.surjective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ →+* R₂) [t : RingHomSurjective σ] :
          @[instance 100]
          instance RingHomSurjective.invPair {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁} [RingHomInvPair σ₁ σ₂] :
          Equations
          • =
          instance RingHomSurjective.ids {R₁ : Type u_1} [Semiring R₁] :
          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 σ₂₃.

          instance RingHomSurjective.instToRingHomRingEquiv {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ ≃+* R₂) :
          Equations
          • =