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

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

• eq_id : σ = RingHom.id R

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

instance instRingHomIdIdToNonAssocSemiring {R : Type u_4} [Semiring R] : RingHomId (RingHom.id R)

Equations

• @instRingHomIdIdToNonAssocSemiring = @instRingHomIdIdToNonAssocSemiring.proof_1

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₃)) : Prop

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

  The morphisms form a commutative triangle

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

@[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₁)) : Prop

• comp_eq : RingHom.comp σ' σ = RingHom.id R₁

  σ' is a left inverse of σ

• comp_eq₂ : RingHom.comp σ σ' = RingHom.id R₂

  σ' is a left inverse of σ'

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

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₁] : RingHomInvPair (RingHom.id R₁) (RingHom.id R₁)

Equations

• @RingHomInvPair.ids = @RingHomInvPair.ids.proof_1

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

• @RingHomInvPair.triples = @RingHomInvPair.triples.proof_1

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

• @RingHomInvPair.triples₂ = @RingHomInvPair.triples₂.proof_1

@[reducible]

theorem RingHomInvPair.of_ringEquiv {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (e : R₁ ≃+* R₂) : RingHomInvPair ↑e ↑(RingEquiv.symm e)

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

• @RingHomCompTriple.ids = @RingHomCompTriple.ids.proof_1

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

Equations

• @RingHomCompTriple.right_ids = @RingHomCompTriple.right_ids.proof_1

class RingHomSurjective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ →+* R₂) : Prop

• is_surjective : Function.Surjective ↑σ

  The ring homomorphism is surjective

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

theorem RingHom.surjective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ →+* R₂) [t : RingHomSurjective σ] : Function.Surjective ↑σ

instance RingHomSurjective.invPair {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁} [RingHomInvPair σ₁ σ₂] : RingHomSurjective σ₁

Equations

• @RingHomSurjective.invPair = @RingHomSurjective.invPair.proof_1

instance RingHomSurjective.ids {R₁ : Type u_1} [Semiring R₁] : RingHomSurjective (RingHom.id R₁)

Equations

• @RingHomSurjective.ids = @RingHomSurjective.ids.proof_1

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 σ₂₃] : RingHomSurjective σ₁₃

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