Documentation

Mathlib.Algebra.GroupWithZero.Hom

Monoid with zero and group with zero homomorphisms #

This file defines homomorphisms of monoids with zero.

We also define coercion to a function, and usual operations: composition, identity homomorphism, pointwise multiplication and pointwise inversion.

Notations #

Implementation notes #

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type MonoidHom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Tags #

monoid homomorphism

theorem NeZero.of_map {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] {a : α} (f : F) [neZero : NeZero (f a)] :
theorem NeZero.of_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] {a : α} {f : F} (hf : Function.Injective f) [NeZero a] :
NeZero (f a)
class MonoidWithZeroHomClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] extends MonoidHomClass , ZeroHomClass :

MonoidWithZeroHomClass F α β states that F is a type of MonoidWithZero-preserving homomorphisms.

You should also extend this typeclass when you extend MonoidWithZeroHom.

    Instances
      structure MonoidWithZeroHom (α : Type u_7) (β : Type u_8) [MulZeroOneClass α] [MulZeroOneClass β] extends ZeroHom :
      Type (max u_7 u_8)

      α →*₀ β is the type of functions α → β that preserve the MonoidWithZero structure.

      MonoidWithZeroHom is also used for group homomorphisms.

      When possible, instead of parametrizing results over (f : α →*₀ β), you should parametrize over (F : Type*) [MonoidWithZeroHomClass F α β] (f : F).

      When you extend this structure, make sure to extend MonoidWithZeroHomClass.

      • toFun : αβ
      • map_zero' : (↑self).toFun 0 = 0
      • map_one' : (↑self).toFun 1 = 1

        The proposition that the function preserves 1

      • map_mul' : ∀ (x y : α), (↑self).toFun (x * y) = (↑self).toFun x * (↑self).toFun y

        The proposition that the function preserves multiplication

      Instances For

        α →*₀ β denotes the type of zero-preserving monoid homomorphisms from α to β.

        Equations
        Instances For
          def MonoidWithZeroHomClass.toMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) :
          α →*₀ β

          Turn an element of a type F satisfying MonoidWithZeroHomClass F α β into an actual MonoidWithZeroHom. This is declared as the default coercion from F to α →*₀ β.

          Equations
          • f = let __src := f; let __src_1 := f; { toFun := (↑__src).toFun, map_zero' := , map_one' := , map_mul' := }
          Instances For
            instance instCoeTCMonoidWithZeroHomOfMonoidWithZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [MonoidWithZeroHomClass F α β] :
            CoeTC F (α →*₀ β)

            Any type satisfying MonoidWithZeroHomClass can be cast into MonoidWithZeroHom via MonoidWithZeroHomClass.toMonoidWithZeroHom.

            Equations
            • instCoeTCMonoidWithZeroHomOfMonoidWithZeroHomClass = { coe := MonoidWithZeroHomClass.toMonoidWithZeroHom }
            instance MonoidWithZeroHom.funLike {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
            FunLike (α →*₀ β) α β
            Equations
            • MonoidWithZeroHom.funLike = { coe := fun (f : α →*₀ β) => (↑f).toFun, coe_injective' := }
            Equations
            • =
            Equations
            • =
            @[simp]
            theorem MonoidWithZeroHom.coe_coe {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) :
            f = f

            Bundled morphisms can be down-cast to weaker bundlings

            instance MonoidWithZeroHom.coeToMonoidHom {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
            Coe (α →*₀ β) (α →* β)

            MonoidWithZeroHom down-cast to a MonoidHom, forgetting the 0-preserving property.

            Equations
            • MonoidWithZeroHom.coeToMonoidHom = { coe := MonoidWithZeroHom.toMonoidHom }
            instance MonoidWithZeroHom.coeToZeroHom {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
            Coe (α →*₀ β) (ZeroHom α β)

            MonoidWithZeroHom down-cast to a ZeroHom, forgetting the monoidal property.

            Equations
            • MonoidWithZeroHom.coeToZeroHom = { coe := MonoidWithZeroHom.toZeroHom }
            @[simp]
            theorem MonoidWithZeroHom.coe_mk {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : ZeroHom α β) (h1 : f.toFun 1 = 1) (hmul : ∀ (x y : α), f.toFun (x * y) = f.toFun x * f.toFun y) :
            { toZeroHom := f, map_one' := h1, map_mul' := hmul } = f
            @[simp]
            theorem MonoidWithZeroHom.toZeroHom_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
            f = f
            theorem MonoidWithZeroHom.toMonoidHom_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
            (↑f).toFun = f
            theorem MonoidWithZeroHom.ext_iff {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] {f : α →*₀ β} {g : α →*₀ β} :
            f = g ∀ (x : α), f x = g x
            theorem MonoidWithZeroHom.ext {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] ⦃f : α →*₀ β ⦃g : α →*₀ β (h : ∀ (x : α), f x = g x) :
            f = g
            @[simp]
            theorem MonoidWithZeroHom.mk_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (h1 : (↑f).toFun 1 = 1) (hmul : ∀ (x y : α), (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y) :
            { toZeroHom := f, map_one' := h1, map_mul' := hmul } = f
            def MonoidWithZeroHom.copy {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : αβ) (h : f' = f) :
            α →* β

            Copy of a MonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

            Equations
            • f.copy f' h = let __src := (↑f).copy f' h; let __src_1 := (↑f).copy f' h; { toFun := __src.toFun, map_one' := , map_mul' := }
            Instances For
              @[simp]
              theorem MonoidWithZeroHom.coe_copy {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : αβ) (h : f' = f) :
              (f.copy f' h) = f'
              theorem MonoidWithZeroHom.copy_eq {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : αβ) (h : f' = f) :
              f.copy f' h = f
              theorem MonoidWithZeroHom.map_one {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
              f 1 = 1
              theorem MonoidWithZeroHom.map_zero {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
              f 0 = 0
              theorem MonoidWithZeroHom.map_mul {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (a : α) (b : α) :
              f (a * b) = f a * f b
              @[simp]
              theorem MonoidWithZeroHom.id_apply (α : Type u_7) [MulZeroOneClass α] (x : α) :

              The identity map from a MonoidWithZero to itself.

              Equations
              • MonoidWithZeroHom.id α = { toFun := fun (x : α) => x, map_zero' := , map_one' := , map_mul' := }
              Instances For
                def MonoidWithZeroHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (hnp : β →*₀ γ) (hmn : α →*₀ β) :
                α →*₀ γ

                Composition of MonoidWithZeroHoms as a MonoidWithZeroHom.

                Equations
                • hnp.comp hmn = { toFun := hnp hmn, map_zero' := , map_one' := , map_mul' := }
                Instances For
                  @[simp]
                  theorem MonoidWithZeroHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β) :
                  (g.comp f) = g f
                  theorem MonoidWithZeroHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β) (x : α) :
                  (g.comp f) x = g (f x)
                  theorem MonoidWithZeroHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] [MulZeroOneClass δ] (f : α →*₀ β) (g : β →*₀ γ) (h : γ →*₀ δ) :
                  (h.comp g).comp f = h.comp (g.comp f)
                  theorem MonoidWithZeroHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g₁ : β →*₀ γ} {g₂ : β →*₀ γ} {f : α →*₀ β} (hf : Function.Surjective f) :
                  g₁.comp f = g₂.comp f g₁ = g₂
                  theorem MonoidWithZeroHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g : β →*₀ γ} {f₁ : α →*₀ β} {f₂ : α →*₀ β} (hg : Function.Injective g) :
                  g.comp f₁ = g.comp f₂ f₁ = f₂
                  theorem MonoidWithZeroHom.toMonoidHom_injective {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
                  Function.Injective MonoidWithZeroHom.toMonoidHom
                  theorem MonoidWithZeroHom.toZeroHom_injective {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
                  Function.Injective MonoidWithZeroHom.toZeroHom
                  @[simp]
                  theorem MonoidWithZeroHom.comp_id {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
                  f.comp (MonoidWithZeroHom.id α) = f
                  @[simp]
                  theorem MonoidWithZeroHom.id_comp {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
                  (MonoidWithZeroHom.id β).comp f = f
                  Equations
                  instance MonoidWithZeroHom.instMul {α : Type u_2} [MulZeroOneClass α] {β : Type u_7} [CommMonoidWithZero β] :
                  Mul (α →*₀ β)

                  Given two monoid with zero morphisms f, g to a commutative monoid with zero, f * g is the monoid with zero morphism sending x to f x * g x.

                  Equations
                  • MonoidWithZeroHom.instMul = { mul := fun (f g : α →*₀ β) => let __src := f * g; { toFun := (↑__src).toFun, map_zero' := , map_one' := , map_mul' := } }
                  def powMonoidWithZeroHom {M₀ : Type u_6} [CommMonoidWithZero M₀] {n : } (hn : n 0) :
                  M₀ →*₀ M₀

                  We define x ↦ x^n (for positive n : ℕ) as a MonoidWithZeroHom

                  Equations
                  Instances For
                    @[simp]
                    theorem coe_powMonoidWithZeroHom {M₀ : Type u_6} [CommMonoidWithZero M₀] {n : } (hn : n 0) :
                    (powMonoidWithZeroHom hn) = fun (x : M₀) => x ^ n
                    @[simp]
                    theorem powMonoidWithZeroHom_apply {M₀ : Type u_6} [CommMonoidWithZero M₀] {n : } (hn : n 0) (a : M₀) :

                    Equivalences #

                    @[instance 100]
                    instance MulEquivClass.toZeroHomClass {F : Type u_7} {α : Type u_8} {β : Type u_9} [EquivLike F α β] [MulZeroClass α] [MulZeroClass β] [MulEquivClass F α β] :
                    ZeroHomClass F α β
                    Equations
                    • =
                    @[instance 100]
                    instance MulEquivClass.toMonoidWithZeroHomClass {F : Type u_7} {α : Type u_8} {β : Type u_9} [EquivLike F α β] [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] :
                    Equations
                    • =