mathlib3 documentation

algebra.ring.comp_typeclasses

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:

Instances of these typeclasses mostly involving ring_hom.id are also provided:

Implementation notes #

Tags #

ring_hom_comp_triple, ring_hom_inv_pair, ring_hom_surjective

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

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
@[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
@[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
@[protected, instance]
def ring_hom_inv_pair.ids {R₁ : Type u_1} [semiring R₁] :
@[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₁)
@[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₂)
@[reducible]
theorem ring_hom_inv_pair.of_ring_equiv {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (e : R₁ ≃+* R₂) :

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].

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

@[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₁) σ₁₂ σ₁₂
@[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₂) σ₁₂
@[class]
structure ring_hom_surjective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (σ : R₁ →+* R₂) :
Prop

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
theorem ring_hom.is_surjective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] (σ : R₁ →+* R₂) [t : ring_hom_surjective σ] :
@[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 σ₁ σ₂] :
@[protected, instance]
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 σ₂₃] :

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