Documentation

Mathlib.Algebra.Group.WithOne.Basic

More operations on WithOne and WithZero #

This file defines various bundled morphisms on WithOne and WithZero that were not available in Algebra/Group/WithOne/Defs.

Main definitions #

source
@[implicit_reducible]
instance WithOne.instInvolutiveInv {α : Type u} [InvolutiveInv α] :
InvolutiveInv (WithOne α)
source
@[implicit_reducible]
instance WithZero.instInvolutiveNeg {α : Type u} [InvolutiveNeg α] :
InvolutiveNeg (WithZero α)
source
def WithOne.coeMulHom {α : Type u} [Mul α] :
α →ₙ* WithOne α

WithOne.coe as a bundled morphism

Instances For
    source
    def WithZero.coeAddHom {α : Type u} [Add α] :
    α →ₙ+ WithZero α

    WithZero.coe as a bundled morphism

    Instances For
      source
      @[simp]
      theorem WithZero.coeAddHom_apply {α : Type u} [Add α] (a✝ : α) :
      coeAddHom a✝ = ↑a✝
      source
      @[simp]
      theorem WithOne.coeMulHom_apply {α : Type u} [Mul α] (a✝ : α) :
      coeMulHom a✝ = ↑a✝
      source
      def WithOne.lift {α : Type u} {β : Type v} [Mul α] [MulOneClass β] :
      (α →ₙ* β) ≃ (WithOne α →* β)

      Lift a semigroup homomorphism f to a bundled monoid homomorphism.

      Instances For
        source
        def WithZero.lift {α : Type u} {β : Type v} [Add α] [AddZeroClass β] :
        (α →ₙ+ β) ≃ (WithZero α →+ β)

        Lift an additive semigroup homomorphism f to a bundled additive monoid homomorphism.

        Instances For
          source
          @[simp]
          theorem WithOne.lift_coe {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) (x : α) :
          (lift f) ↑x = f x
          source
          @[simp]
          theorem WithZero.lift_coe {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : α →ₙ+ β) (x : α) :
          (lift f) ↑x = f x
          source
          @[simp]
          theorem WithOne.lift_one {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) :
          (lift f) 1 = 1
          source
          @[simp]
          theorem WithZero.lift_zero {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : α →ₙ+ β) :
          (lift f) 0 = 0
          source
          theorem WithOne.lift_unique {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : WithOne α →* β) :
          f = lift ((↑f).comp coeMulHom)
          source
          theorem WithZero.lift_unique {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : WithZero α →+ β) :
          f = lift ((↑f).comp coeAddHom)
          source
          @[simp]
          theorem WithOne.lift_symm_apply {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : WithOne α →* β) (x : α) :
          (lift.symm f) x = f ↑x
          source
          @[simp]
          theorem WithZero.lift_symm_apply {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : WithZero α →+ β) (x : α) :
          (lift.symm f) x = f ↑x
          source
          def WithOne.mapMulHom {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) :
          WithOne α →* WithOne β

          Given a multiplicative map from α → β returns a monoid homomorphism from WithOne α to WithOne β

          Instances For
            source
            def WithZero.mapAddHom {α : Type u} {β : Type v} [Add α] [Add β] (f : α →ₙ+ β) :
            WithZero α →+ WithZero β

            Given an additive map from α → β returns an additive monoid homomorphism from WithZero α to WithZero β

            Instances For
              source
              @[simp]
              theorem WithOne.mapMulHom_coe {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) (a : α) :
              (mapMulHom f) ↑a = ↑(f a)
              source
              @[simp]
              theorem WithZero.mapAddHom_coe {α : Type u} {β : Type v} [Add α] [Add β] (f : α →ₙ+ β) (a : α) :
              (mapAddHom f) ↑a = ↑(f a)
              source
              @[simp]
              theorem WithOne.mapMulHom_id {α : Type u} [Mul α] :
              mapMulHom (MulHom.id α) = MonoidHom.id (WithOne α)
              source
              @[simp]
              theorem WithZero.mapAddHom_id {α : Type u} [Add α] :
              mapAddHom (AddHom.id α) = AddMonoidHom.id (WithZero α)
              source
              theorem WithOne.mapMulHom_injective {α : Type u} {β : Type v} [Mul α] [Mul β] {f : α →ₙ* β} (hf : Function.Injective ⇑f) :
              Function.Injective ⇑(mapMulHom f)
              source
              theorem WithZero.mapAddHom_injective {α : Type u} {β : Type v} [Add α] [Add β] {f : α →ₙ+ β} (hf : Function.Injective ⇑f) :
              Function.Injective ⇑(mapAddHom f)
              source
              theorem WithOne.mapMulHom_injective' {α : Type u} {β : Type v} [Mul α] [Mul β] :
              Function.Injective mapMulHom
              source
              theorem WithZero.mapAddHom_injective' {α : Type u} {β : Type v} [Add α] [Add β] :
              Function.Injective mapAddHom
              source
              @[simp]
              theorem WithOne.mapMulHom_inj {α : Type u} {β : Type v} [Mul α] [Mul β] {f g : α →ₙ* β} :
              mapMulHom f = mapMulHom g ↔ f = g
              source
              @[simp]
              theorem WithZero.mapAddHom_inj {α : Type u} {β : Type v} [Add α] [Add β] {f g : α →ₙ+ β} :
              mapAddHom f = mapAddHom g ↔ f = g
              source
              theorem WithOne.mapMulHom_mapMulHom {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : WithOne α) :
              (mapMulHom g) ((mapMulHom f) x) = (mapMulHom (g.comp f)) x
              source
              theorem WithZero.mapAddHom_mapAddHom {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ) (x : WithZero α) :
              (mapAddHom g) ((mapAddHom f) x) = (mapAddHom (g.comp f)) x
              source
              @[simp]
              theorem WithOne.mapMulHom_comp {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) :
              mapMulHom (g.comp f) = (mapMulHom g).comp (mapMulHom f)
              source
              @[simp]
              theorem WithZero.mapAddHom_comp {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ) :
              mapAddHom (g.comp f) = (mapAddHom g).comp (mapAddHom f)
              source
              def MulEquiv.withOneCongr {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) :
              WithOne α ≃* WithOne β

              A version of Equiv.optionCongr for WithOne.

              Instances For
                source
                def AddEquiv.withZeroCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                WithZero α ≃+ WithZero β

                A version of Equiv.optionCongr for WithZero.

                Instances For
                  source
                  @[simp]
                  theorem AddEquiv.withZeroCongr_apply {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) (a : WithZero α) :
                  e.withZeroCongr a = (WithZero.mapAddHom e.toAddHom) a
                  source
                  @[simp]
                  theorem MulEquiv.withOneCongr_apply {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) (a : WithOne α) :
                  e.withOneCongr a = (WithOne.mapMulHom e.toMulHom) a
                  source
                  @[simp]
                  theorem MulEquiv.withOneCongr_refl {α : Type u} [Mul α] :
                  (refl α).withOneCongr = refl (WithOne α)
                  source
                  @[simp]
                  theorem AddEquiv.withZeroCongr_refl {α : Type u} [Add α] :
                  (refl α).withZeroCongr = refl (WithZero α)
                  source
                  @[simp]
                  theorem MulEquiv.withOneCongr_symm {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) :
                  e.withOneCongr.symm = e.symm.withOneCongr
                  source
                  @[simp]
                  theorem AddEquiv.withZeroCongr_symm {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
                  e.withZeroCongr.symm = e.symm.withZeroCongr
                  source
                  @[simp]
                  theorem MulEquiv.withOneCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (e₁ : α ≃* β) (e₂ : β ≃* γ) :
                  e₁.withOneCongr.trans e₂.withOneCongr = (e₁.trans e₂).withOneCongr
                  source
                  @[simp]
                  theorem AddEquiv.withZeroCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) :
                  e₁.withZeroCongr.trans e₂.withZeroCongr = (e₁.trans e₂).withZeroCongr