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

source

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

Instances

source

theorem RingHomId.eq_id {R : Type u_4} :

∀ {inst : Semiring R} {σ : R →+* R} [self : RingHomId σ], σ = RingHom.id R

source

instance instRingHomIdId {R : Type u_4} [Semiring R] :

RingHomId (RingHom.id R)

Equations

⋯ = ⋯

source

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

Instances

source

@[simp]

theorem RingHomCompTriple.comp_eq {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} :

∀ {inst : Semiring R₁} {inst_1 : Semiring R₂} {inst_2 : Semiring R₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : outParam (R₁ →+* R₃)} [self : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃], σ₂₃.comp σ₁₂ = σ₁₃

The morphisms form a commutative triangle

source

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

source

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 σ'

Instances

source

theorem RingHomInvPair.comp_eq {R₁ : Type u_1} {R₂ : Type u_2} :

∀ {inst : Semiring R₁} {inst_1 : Semiring R₂} {σ : R₁ →+* R₂} {σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'], RingHom.comp σ' σ = RingHom.id R₁

σ' is a left inverse of σ

source

theorem RingHomInvPair.comp_eq₂ {R₁ : Type u_1} {R₂ : Type u_2} :

∀ {inst : Semiring R₁} {inst_1 : Semiring R₂} {σ : R₁ →+* R₂} {σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'], σ.comp σ' = RingHom.id R₂

σ' is a left inverse of σ'

source

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

source

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

source

instance RingHomInvPair.ids {R₁ : Type u_1} [Semiring R₁] :

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

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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.

source

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.

source

instance RingHomCompTriple.ids {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} :

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

Equations

⋯ = ⋯

source

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

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

Equations

⋯ = ⋯

source

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

Instances

source

theorem RingHomSurjective.is_surjective {R₁ : Type u_1} {R₂ : Type u_2} :

∀ {inst : Semiring R₁} {inst_1 : Semiring R₂} {σ : R₁ →+* R₂} [self : RingHomSurjective σ], Function.Surjective ⇑σ

The ring homomorphism is surjective

source

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

Function.Surjective ⇑σ

source

@[instance 100]

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

RingHomSurjective σ₁

Equations

⋯ = ⋯

source

instance RingHomSurjective.ids {R₁ : Type u_1} [Semiring R₁] :

RingHomSurjective (RingHom.id R₁)

Equations

⋯ = ⋯

source

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

source

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

RingHomSurjective ↑σ

Equations

⋯ = ⋯

Documentation

Mathlib.Algebra.Ring.CompTypeclasses

Propositional typeclasses on several ring homs #

Implementation notes #

Tags #