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

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

• eq_id : σ = RingHom.id R

theorem instRingHomIdId {R : Type u_4} [Semiring R] : RingHomId (RingHom.id R)

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

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

@[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

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

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

  σ' is a left inverse of σ

• comp_eq₂ : σ.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

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

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

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

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.

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

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

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

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

• is_surjective : Function.Surjective ⇑σ

  The ring homomorphism is surjective

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

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

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

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 σ₂₃.

theorem RingHomSurjective.instToRingHomRingEquiv {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] (σ : R₁ ≃+* R₂) : RingHomSurjective ↑σ