Documentation

Mathlib.Algebra.GroupWithZero.WithZero

Adjoining a zero to a group #

This file proves that one can adjoin a new zero element to a group and get a group with zero.

In valuation theory, valuations have codomain {0} ∪ {c ^ n | n : ℤ} for some c > 1, which we can formalise as ℤᵐ⁰ := WithZero (Multiplicative ℤ). It is important to be able to talk about the maps n ↦ c ^ n and c ^ n ↦ n. We define these as exp : ℤ → ℤᵐ⁰ and log : ℤᵐ⁰ → ℤ with junk value log 0 = 0. Junkless versions are defined as expEquiv : ℤ ≃ ℤᵐ⁰ˣ and logEquiv : ℤᵐ⁰ˣ ≃ ℤ.

Notation #

In locale WithZero:

Main definitions #

instance WithZero.one {α : Type u_1} [One α] :
Equations
@[simp]
theorem WithZero.coe_one {α : Type u_1} [One α] :
1 = 1
@[simp]
theorem WithZero.recZeroCoe_one {M : Type u_4} {N : Type u_5} [One M] (f : MN) (z : N) :
recZeroCoe z f 1 = f 1
instance WithZero.instMulZeroClass {α : Type u_1} [Mul α] :
Equations
@[simp]
theorem WithZero.coe_mul {α : Type u_1} [Mul α] (a b : α) :
↑(a * b) = a * b
theorem WithZero.unzero_mul {α : Type u_1} [Mul α] {x y : WithZero α} (hxy : x * y 0) :
unzero hxy = unzero * unzero
Equations
Equations
  • One or more equations did not get rendered due to their size.

Coercion as a monoid hom.

Equations
Instances For
    @[simp]
    theorem WithZero.coeMonoidHom_apply {α : Type u_1} [MulOneClass α] (a✝ : α) :
    coeMonoidHom a✝ = a✝
    theorem WithZero.monoidWithZeroHom_ext {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] f g : WithZero α →*₀ β (h : (↑f).comp coeMonoidHom = (↑g).comp coeMonoidHom) :
    f = g
    theorem WithZero.monoidWithZeroHom_ext_iff {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] {f g : WithZero α →*₀ β} :
    def WithZero.lift' {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] :
    (α →* β) (WithZero α →*₀ β)

    The (multiplicative) universal property of WithZero.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem WithZero.lift'_symm_apply_apply {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (F : WithZero α →*₀ β) (a✝ : α) :
      (lift'.symm F) a✝ = F a✝
      theorem WithZero.lift'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) :
      (lift' f) 0 = 0
      @[simp]
      theorem WithZero.lift'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) (x : α) :
      (lift' f) x = f x
      theorem WithZero.lift'_unique {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : WithZero α →*₀ β) :
      def WithZero.map' {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) :

      The MonoidWithZero homomorphism WithZero α →* WithZero β induced by a monoid homomorphism f : α →* β.

      Equations
      Instances For
        theorem WithZero.map'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) :
        (map' f) 0 = 0
        @[simp]
        theorem WithZero.map'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (x : α) :
        (map' f) x = (f x)
        @[simp]
        theorem WithZero.map'_id {β : Type u_2} [MulOneClass β] :
        theorem WithZero.map'_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) (x : WithZero α) :
        (map' g) ((map' f) x) = (map' (g.comp f)) x
        @[simp]
        theorem WithZero.map'_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) :
        map' (g.comp f) = (map' g).comp (map' f)
        theorem WithZero.map'_injective_iff {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] {f : α →* β} :
        theorem WithZero.map'_injective {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] {f : α →* β} :

        Alias of the reverse direction of WithZero.map'_injective_iff.

        instance WithZero.pow {α : Type u_1} [One α] [Pow α ] :
        Equations
        @[simp]
        theorem WithZero.coe_pow {α : Type u_1} [One α] [Pow α ] (a : α) (n : ) :
        ↑(a ^ n) = a ^ n
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        instance WithZero.inv {α : Type u_1} [Inv α] :

        Extend the inverse operation on α to WithZero α by sending 0 to 0.

        Equations
        @[simp]
        theorem WithZero.coe_inv {α : Type u_1} [Inv α] (a : α) :
        a⁻¹ = (↑a)⁻¹
        @[simp]
        theorem WithZero.inv_zero {α : Type u_1} [Inv α] :
        0⁻¹ = 0
        Equations
        instance WithZero.div {α : Type u_1} [Div α] :
        Equations
        theorem WithZero.coe_div {α : Type u_1} [Div α] (a b : α) :
        ↑(a / b) = a / b
        instance WithZero.instPowInt {α : Type u_1} [One α] [Pow α ] :
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem WithZero.coe_zpow {α : Type u_1} [One α] [Pow α ] (a : α) (n : ) :
        ↑(a ^ n) = a ^ n
        Equations
        • One or more equations did not get rendered due to their size.
        Equations

        If α is a group then WithZero α is a group with zero.

        Equations
        • One or more equations did not get rendered due to their size.

        Any group is isomorphic to the units of itself adjoined with 0.

        Equations
        Instances For
          @[simp]
          @[simp]
          def WithZero.withZeroUnitsEquiv {G : Type u_4} [GroupWithZero G] [DecidablePred fun (a : G) => a = 0] :

          Any group with zero is isomorphic to adjoining 0 to the units of itself.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem WithZero.withZeroUnitsEquiv_symm_apply {G : Type u_4} [GroupWithZero G] [DecidablePred fun (a : G) => a = 0] (a : G) :
            withZeroUnitsEquiv.symm a = if h : a = 0 then 0 else (Units.mk0 a h)
            def MulEquiv.withZero {α : Type u_1} {β : Type u_2} [Group α] [Group β] :
            α ≃* β (WithZero α ≃* WithZero β)

            A version of Equiv.optionCongr for WithZero.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem MulEquiv.withZero_apply_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : α ≃* β) (a : WithZero α) :
              (withZero e) a = (WithZero.map' e) a
              @[simp]
              theorem MulEquiv.withZero_apply_symm_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : α ≃* β) (a : WithZero β) :
              @[simp]
              theorem MulEquiv.withZero_symm_apply_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) (x : α) :
              @[simp]
              theorem MulEquiv.withZero_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) (x : β) :
              @[reducible, inline]
              abbrev MulEquiv.unzero {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) :
              α ≃* β

              The inverse of MulEquiv.withZero.

              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Equations

                Exponential and logarithm #

                Mᵐ⁰ is notation for WithZero (Multiplicative M).

                This naturally shows up as the codomain of valuations in valuation theory.

                Equations
                Instances For
                  def WithZero.exp {M : Type u_4} (a : M) :

                  The exponential map as a function M → Mᵐ⁰.

                  Equations
                  Instances For
                    @[simp]
                    theorem WithZero.exp_ne_zero {M : Type u_4} {a : M} :
                    exp a 0
                    def WithZero.log {M : Type u_4} [AddMonoid M] (x : WithZero (Multiplicative M)) :
                    M

                    The logarithm as a function Mᵐ⁰ → M with junk value log 0 = 0.

                    Equations
                    Instances For
                      @[simp]
                      theorem WithZero.log_exp {M : Type u_4} [AddMonoid M] (a : M) :
                      (exp a).log = a
                      @[simp]
                      theorem WithZero.exp_log {M : Type u_4} [AddMonoid M] {x : WithZero (Multiplicative M)} (hx : x 0) :
                      exp x.log = x
                      @[simp]
                      theorem WithZero.log_zero {M : Type u_4} [AddMonoid M] :
                      log 0 = 0
                      @[simp]
                      theorem WithZero.exp_zero {M : Type u_4} [AddMonoid M] :
                      exp 0 = 1
                      @[simp]
                      theorem WithZero.log_one {M : Type u_4} [AddMonoid M] :
                      log 1 = 0
                      theorem WithZero.exp_add {M : Type u_4} [AddMonoid M] (a b : M) :
                      exp (a + b) = exp a * exp b
                      theorem WithZero.log_mul {M : Type u_4} [AddMonoid M] {x y : WithZero (Multiplicative M)} (hx : x 0) (hy : y 0) :
                      (x * y).log = x.log + y.log
                      theorem WithZero.exp_nsmul {M : Type u_4} [AddMonoid M] (n : ) (a : M) :
                      exp (n a) = exp a ^ n
                      theorem WithZero.log_pow {M : Type u_4} [AddMonoid M] (x : WithZero (Multiplicative M)) (n : ) :
                      (x ^ n).log = n x.log

                      The exponential map as an equivalence between G and (Gᵐ⁰)ˣ.

                      Equations
                      Instances For

                        The logarithm as an equivalence between (Gᵐ⁰)ˣ and G.

                        Equations
                        Instances For
                          @[simp]
                          theorem WithZero.coe_expEquiv_apply {G : Type u_5} [AddGroup G] (a : G) :
                          (expEquiv a) = exp a
                          @[simp]
                          theorem WithZero.logEquiv_apply {G : Type u_5} [AddGroup G] (x : (WithZero (Multiplicative G))ˣ) :
                          logEquiv x = (↑x).log
                          theorem WithZero.logEquiv_unitsMk0 {G : Type u_5} [AddGroup G] (x : WithZero (Multiplicative G)) (hx : x 0) :
                          theorem WithZero.exp_sub {G : Type u_5} [AddGroup G] (a b : G) :
                          exp (a - b) = exp a / exp b
                          theorem WithZero.log_div {G : Type u_5} [AddGroup G] {x y : WithZero (Multiplicative G)} (hx : x 0) (hy : y 0) :
                          (x / y).log = x.log - y.log
                          theorem WithZero.exp_neg {G : Type u_5} [AddGroup G] (a : G) :
                          exp (-a) = (exp a)⁻¹
                          theorem WithZero.exp_zsmul {G : Type u_5} [AddGroup G] (n : ) (a : G) :
                          exp (n a) = exp a ^ n
                          theorem WithZero.log_zpow {G : Type u_5} [AddGroup G] (x : WithZero (Multiplicative G)) (n : ) :
                          (x ^ n).log = n x.log
                          theorem MonoidWithZeroHom.map_eq_zero_iff {G₀ : Type u_1} {G₀' : Type u_2} [GroupWithZero G₀] [MulZeroOneClass G₀'] [Nontrivial G₀'] {f : G₀ →*₀ G₀'} {x : G₀} :
                          f x = 0 x = 0
                          @[simp]
                          theorem MonoidWithZeroHom.one_apply_val_unit {M₀ : Type u_1} {N₀ : Type u_2} [MonoidWithZero M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] (x : M₀ˣ) :
                          1 x = 1
                          @[simp]
                          theorem MonoidWithZeroHom.apply_one_apply_eq {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀] [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun (x : M₀) => x = 0] (f : N₀ →*₀ G₀) (x : M₀) :
                          f (1 x) = 1 x

                          The trivial group-with-zero hom is absorbing for composition.

                          @[simp]
                          theorem MonoidWithZeroHom.comp_one {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀] [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun (x : M₀) => x = 0] (f : N₀ →*₀ G₀) :
                          f.comp 1 = 1

                          The trivial group-with-zero hom is absorbing for composition.