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.

Main definitions #

instance WithZero.one {α : Type u_1} [One α] :
Equations
  • WithZero.one = { one := One.one }
@[simp]
theorem WithZero.coe_one {α : Type u_1} [One α] :
1 = 1
instance WithZero.mulZeroClass {α : 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 : WithZero α} {y : WithZero α} (hxy : x * y 0) :
instance WithZero.noZeroDivisors {α : Type u_1} [Mul α] :
Equations
  • =
Equations
Equations
Equations
@[simp]
theorem WithZero.coeMonoidHom_apply {α : Type u_1} [MulOneClass α] :
∀ (a : α), WithZero.coeMonoidHom a = a

Coercion as a monoid hom.

Equations
  • WithZero.coeMonoidHom = { toFun := WithZero.coe, map_one' := , map_mul' := }
Instances For
    theorem WithZero.monoidWithZeroHom_ext_iff {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] {f : WithZero α →*₀ β} {g : WithZero α →*₀ β} :
    f = g (↑f).comp WithZero.coeMonoidHom = (↑g).comp WithZero.coeMonoidHom
    theorem WithZero.monoidWithZeroHom_ext {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] ⦃f : WithZero α →*₀ β ⦃g : WithZero α →*₀ β (h : (↑f).comp WithZero.coeMonoidHom = (↑g).comp WithZero.coeMonoidHom) :
    f = g
    @[simp]
    theorem WithZero.lift'_symm_apply_apply {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (F : WithZero α →*₀ β) :
    ∀ (a : α), (WithZero.lift'.symm F) a = F a
    noncomputable 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
      theorem WithZero.lift'_zero {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) :
      (WithZero.lift' f) 0 = 0
      @[simp]
      theorem WithZero.lift'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : α →* β) (x : α) :
      (WithZero.lift' f) x = f x
      theorem WithZero.lift'_unique {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulZeroOneClass β] (f : WithZero α →*₀ β) :
      f = WithZero.lift' ((↑f).comp WithZero.coeMonoidHom)
      noncomputable 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 : α →* β) :
        @[simp]
        theorem WithZero.map'_coe {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (x : α) :
        (WithZero.map' f) x = (f x)
        theorem WithZero.map'_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) (x : WithZero α) :
        (WithZero.map' g) ((WithZero.map' f) x) = (WithZero.map' (g.comp f)) x
        @[simp]
        theorem WithZero.map'_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →* β) (g : β →* γ) :
        WithZero.map' (g.comp f) = (WithZero.map' g).comp (WithZero.map' f)
        instance WithZero.pow {α : Type u_1} [One α] [Pow α ] :
        Equations
        • WithZero.pow = { pow := fun (x : WithZero α) (n : ) => match x, n with | none, 0 => 1 | none, n.succ => 0 | some x, n => (x ^ n) }
        @[simp]
        theorem WithZero.coe_pow {α : Type u_1} [One α] [Pow α ] (a : α) (n : ) :
        (a ^ n) = a ^ n
        Equations
        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
        Equations
        Equations
        Equations
        Equations
        instance WithZero.groupWithZero {α : Type u_1} [Group α] :

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

        Equations

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

        Equations
        • WithZero.unitsWithZeroEquiv = { toFun := fun (a : (WithZero α)ˣ) => WithZero.unzero , invFun := fun (a : α) => Units.mk0 a , left_inv := , right_inv := , map_mul' := }
        Instances For
          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
            noncomputable def MulEquiv.withZero {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : α ≃* β) :

            A version of Equiv.optionCongr for WithZero.

            Equations
            • e.withZero = { toFun := (WithZero.map' e.toMonoidHom), invFun := (WithZero.map' e.symm.toMonoidHom), left_inv := , right_inv := , map_mul' := }
            Instances For
              noncomputable def MulEquiv.unzero {α : Type u_1} {β : Type u_2} [Group α] [Group β] (e : WithZero α ≃* WithZero β) :
              α ≃* β

              The inverse of MulEquiv.withZero.

              Equations
              • e.unzero = { toFun := fun (x : α) => WithZero.unzero , invFun := fun (x : β) => WithZero.unzero , left_inv := , right_inv := , map_mul' := }
              Instances For
                Equations
                Equations