Documentation

Mathlib.Deprecated.Ring

Unbundled semiring and ring homomorphisms (deprecated) #

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled semiring and ring homomorphisms. Instead of using this file, please use RingHom, defined in Algebra.Hom.Ring, with notation →+*→+*, for morphisms between semirings or rings. For example use φ : A →+* B→+* B to represent a ring homomorphism.

Main Definitions #

IsSemiringHom (deprecated), IsRingHom (deprecated)

Tags #

IsSemiringHom, IsRingHom

source
ink
structure IsSemiringHom {α : Type u} {β : Type v} [inst : Semiring α] [inst : Semiring β] (f : α → β) :
Prop

  • The proposition that f preserves the additive identity.

    map_zero : f 0 = 0

  • The proposition that f preserves the multiplicative identity.

    map_one : f 1 = 1

  • The proposition that f preserves addition.

    map_add : ∀ (x y : α), f (x + y) = f x + f y

  • The proposition that f preserves multiplication.

    map_mul : ∀ (x y : α), f (x * y) = f x * f y

Predicate for semiring homomorphisms (deprecated -- use the bundled RingHom version).

Instances For
    source
    ink
    theorem IsSemiringHom.id {α : Type u} [inst : Semiring α] :
    IsSemiringHom id

    The identity map is a semiring homomorphism.

    source
    ink
    theorem IsSemiringHom.comp {α : Type u} {β : Type v} [inst : Semiring α] [inst : Semiring β] {f : α → β} (hf : IsSemiringHom f) {γ : Type u_1} [inst : Semiring γ] {g : β → γ} (hg : IsSemiringHom g) :
    IsSemiringHom (g ∘ f)

    The composition of two semiring homomorphisms is a semiring homomorphism.

    source
    ink
    theorem IsSemiringHom.to_isAddMonoidHom {α : Type u} {β : Type v} [inst : Semiring α] [inst : Semiring β] {f : α → β} (hf : IsSemiringHom f) :
    IsAddMonoidHom f

    A semiring homomorphism is an additive monoid homomorphism.

    source
    ink
    theorem IsSemiringHom.to_isMonoidHom {α : Type u} {β : Type v} [inst : Semiring α] [inst : Semiring β] {f : α → β} (hf : IsSemiringHom f) :
    IsMonoidHom f

    A semiring homomorphism is a monoid homomorphism.

    source
    ink
    structure IsRingHom {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] (f : α → β) :
    Prop

    • The proposition that f preserves the multiplicative identity.

      map_one : f 1 = 1

    • The proposition that f preserves multiplication.

      map_mul : ∀ (x y : α), f (x * y) = f x * f y

    • The proposition that f preserves addition.

      map_add : ∀ (x y : α), f (x + y) = f x + f y

    Predicate for ring homomorphisms (deprecated -- use the bundled RingHom version).

    Instances For
      source
      ink
      theorem IsRingHom.of_semiring {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] {f : α → β} (H : IsSemiringHom f) :
      IsRingHom f

      A map of rings that is a semiring homomorphism is also a ring homomorphism.

      source
      ink
      theorem IsRingHom.map_zero {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] {f : α → β} (hf : IsRingHom f) :
      f 0 = 0

      Ring homomorphisms map zero to zero.

      source
      ink
      theorem IsRingHom.map_neg {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] {f : α → β} {x : α} (hf : IsRingHom f) :
      f (-x) = -f x

      Ring homomorphisms preserve additive inverses.

      source
      ink
      theorem IsRingHom.map_sub {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] {f : α → β} {x : α} {y : α} (hf : IsRingHom f) :
      f (x - y) = f x - f y

      Ring homomorphisms preserve subtraction.

      source
      ink
      theorem IsRingHom.id {α : Type u} [inst : Ring α] :
      IsRingHom id

      The identity map is a ring homomorphism.

      source
      ink
      theorem IsRingHom.comp {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] {f : α → β} (hf : IsRingHom f) {γ : Type u_1} [inst : Ring γ] {g : β → γ} (hg : IsRingHom g) :
      IsRingHom (g ∘ f)

      The composition of two ring homomorphisms is a ring homomorphism.

      source
      ink
      theorem IsRingHom.to_isSemiringHom {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] {f : α → β} (hf : IsRingHom f) :
      IsSemiringHom f

      A ring homomorphism is also a semiring homomorphism.

      source
      ink
      theorem IsRingHom.to_isAddGroupHom {α : Type u} {β : Type v} [inst : Ring α] [inst : Ring β] {f : α → β} (hf : IsRingHom f) :
      IsAddGroupHom f
      source
      ink
      def RingHom.of {α : Type u} {β : Type v} {rα : Semiring α} {rβ : Semiring β} {f : α → β} (hf : IsSemiringHom f) :
      α →+* β

      Interpret f : α → β→ β with IsSemiringHom f as a ring homomorphism.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      @[simp]
      theorem RingHom.coe_of {α : Type u} {β : Type v} {rα : Semiring α} {rβ : Semiring β} {f : α → β} (hf : IsSemiringHom f) :
      ↑(RingHom.of hf) = f
      source
      ink
      theorem RingHom.to_isSemiringHom {α : Type u} {β : Type v} {rα : Semiring α} {rβ : Semiring β} (f : α →+* β) :
      IsSemiringHom ↑f
      source
      ink
      theorem RingHom.to_isRingHom {α : Type u_1} {γ : Type u_2} [inst : Ring α] [inst : Ring γ] (g : α →+* γ) :
      IsRingHom ↑g