Propositional typeclasses on several ring homs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃, which expresses the fact that σ₂₃.comp σ₁₂ = σ₁₃
ring_hom_inv_pair σ₁₂ σ₂₁, which states that σ₁₂ and σ₂₁ are inverses of each other
ring_hom_surjective σ, 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 ring_hom 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 ring_hom.id are also provided:

ring_hom_inv_pair (ring_hom.id R) (ring_hom.id R)
[ring_hom_inv_pair σ₁₂ σ₂₁] : ring_hom_comp_triple σ₁₂ σ₂₁ (ring_hom.id R₁)
ring_hom_comp_triple (ring_hom.id R₁) σ₁₂ σ₁₂
ring_hom_comp_triple σ₁₂ (ring_hom.id R₂) σ₁₂
ring_hom_surjective (ring_hom.id R)
[ring_hom_inv_pair σ₁ σ₂] : ring_hom_surjective σ₁

Implementation notes #

For the typeclass ring_hom_inv_pair σ₁₂ σ₂₁, σ₂₁ is marked as an out_param, as it must typically be found via the typeclass inference system.
Likewise, for ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃, σ₁₃ is marked as an out_param, for the same reason.

Tags #

ring_hom_comp_triple, ring_hom_inv_pair, ring_hom_surjective

source

@[class]

structure ring_hom_comp_triple {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] (σ₁₂ : R₁ →+* R₂) (σ₂₃ : R₂ →+* R₃) (σ₁₃ : out_param (R₁ →+* R₃)) :

Prop

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

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

Instances of this typeclass

source

@[simp]

theorem ring_hom_comp_triple.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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {x : R₁} :

⇑σ₂₃ (⇑σ₁₂ x) = ⇑σ₁₃ x

source

@[class]

structure ring_hom_inv_pair {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (σ : R₁ →+* R₂) (σ' : out_param (R₂ →+* R₁)) :

Prop

comp_eq : ring_hom.comp σ' σ = ring_hom.id R₁
comp_eq₂ : σ.comp σ' = ring_hom.id 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 of this typeclass

source

@[simp]

theorem ring_hom_inv_pair.comp_apply_eq {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ : R₁ →+* R₂} {σ' : R₂ →+* R₁} [ring_hom_inv_pair σ σ'] {x : R₁} :

⇑σ' (⇑σ x) = x

source

@[simp]

theorem ring_hom_inv_pair.comp_apply_eq₂ {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ : R₁ →+* R₂} {σ' : R₂ →+* R₁} [ring_hom_inv_pair σ σ'] {x : R₂} :

⇑σ (⇑σ' x) = x

source

@[protected, instance]

def ring_hom_inv_pair.ids {R₁ : Type u_1} [semiring R₁] :

ring_hom_inv_pair (ring_hom.id R₁) (ring_hom.id R₁)

source

@[protected, instance]

def ring_hom_inv_pair.triples {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] :

ring_hom_comp_triple σ₁₂ σ₂₁ (ring_hom.id R₁)

source

@[protected, instance]

def ring_hom_inv_pair.triples₂ {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] :

ring_hom_comp_triple σ₂₁ σ₁₂ (ring_hom.id R₂)

source

@[reducible]

theorem ring_hom_inv_pair.of_ring_equiv {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (e : R₁ ≃+* R₂) :

ring_hom_inv_pair ↑e ↑(e.symm)

Construct a ring_hom_inv_pair from both directions of a ring equiv.

This is not an instance, as for equivalences that are involutions, a better instance would be ring_hom_inv_pair e e. Indeed, this declaration is not currently used in mathlib.

See note [reducible non-instances].

source

@[reducible]

theorem ring_hom_inv_pair.symm {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁) [ring_hom_inv_pair σ₁₂ σ₂₁] :

ring_hom_inv_pair σ₂₁ σ₁₂

Swap the direction of a ring_hom_inv_pair. 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].

source

@[protected, instance]

def ring_hom_comp_triple.ids {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} :

ring_hom_comp_triple (ring_hom.id R₁) σ₁₂ σ₁₂

source

@[protected, instance]

def ring_hom_comp_triple.right_ids {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} :

ring_hom_comp_triple σ₁₂ (ring_hom.id R₂) σ₁₂

source

@[class]

structure ring_hom_surjective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (σ : R₁ →+* R₂) :

Prop

is_surjective : function.surjective ⇑σ

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

Instances of this typeclass

source

theorem ring_hom.is_surjective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (σ : R₁ →+* R₂) [t : ring_hom_surjective σ] :

function.surjective ⇑σ

source

@[protected, nolint, instance]

def ring_hom_surjective.inv_pair {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁} [ring_hom_inv_pair σ₁ σ₂] :

ring_hom_surjective σ₁

source

@[protected, instance]

def ring_hom_surjective.ids {R₁ : Type u_1} [semiring R₁] :

ring_hom_surjective (ring_hom.id R₁)

source

theorem ring_hom_surjective.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₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_surjective σ₁₂] [ring_hom_surjective σ₂₃] :

ring_hom_surjective σ₁₃

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