Documentation

Mathlib.Algebra.GroupWithZero.InjSurj

Lifting groups with zero along injective/surjective maps #

@[reducible, inline]
abbrev Function.Injective.mulZeroClass {M₀ : Type u_1} {M₀' : Type u_3} [MulZeroClass M₀] [Mul M₀'] [Zero M₀'] (f : M₀'M₀) (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (a b : M₀'), f (a * b) = f a * f b) :

Pull back a MulZeroClass instance along an injective function. See note [reducible non-instances].

Equations
Instances For
    @[reducible, inline]
    abbrev Function.Surjective.mulZeroClass {M₀ : Type u_1} {M₀' : Type u_3} [MulZeroClass M₀] [Mul M₀'] [Zero M₀'] (f : M₀M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (mul : ∀ (a b : M₀), f (a * b) = f a * f b) :

    Push forward a MulZeroClass instance along a surjective function. See note [reducible non-instances].

    Equations
    Instances For
      theorem Function.Injective.noZeroDivisors {M₀ : Type u_1} {M₀' : Type u_3} [Mul M₀] [Zero M₀] [Mul M₀'] [Zero M₀'] (f : M₀M₀') (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) [NoZeroDivisors M₀'] :

      Pull back a NoZeroDivisors instance along an injective function.

      theorem Function.Injective.isLeftCancelMulZero {M₀ : Type u_1} {M₀' : Type u_3} [Mul M₀] [Zero M₀] [Mul M₀'] [Zero M₀'] (f : M₀M₀') (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) [IsLeftCancelMulZero M₀'] :
      theorem Function.Injective.isRightCancelMulZero {M₀ : Type u_1} {M₀' : Type u_3} [Mul M₀] [Zero M₀] [Mul M₀'] [Zero M₀'] (f : M₀M₀') (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) [IsRightCancelMulZero M₀'] :
      @[reducible, inline]
      abbrev Function.Injective.mulZeroOneClass {M₀ : Type u_1} {M₀' : Type u_3} [MulZeroOneClass M₀] [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀'M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (a b : M₀'), f (a * b) = f a * f b) :

      Pull back a MulZeroOneClass instance along an injective function. See note [reducible non-instances].

      Equations
      Instances For
        @[reducible, inline]
        abbrev Function.Surjective.mulZeroOneClass {M₀ : Type u_1} {M₀' : Type u_3} [MulZeroOneClass M₀] [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (a b : M₀), f (a * b) = f a * f b) :

        Push forward a MulZeroOneClass instance along a surjective function. See note [reducible non-instances].

        Equations
        Instances For
          @[reducible, inline]
          abbrev Function.Injective.semigroupWithZero {M₀ : Type u_1} {M₀' : Type u_3} [Zero M₀'] [Mul M₀'] [SemigroupWithZero M₀] (f : M₀'M₀) (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) :

          Pull back a SemigroupWithZero along an injective function. See note [reducible non-instances].

          Equations
          Instances For
            @[reducible, inline]
            abbrev Function.Surjective.semigroupWithZero {M₀ : Type u_1} {M₀' : Type u_3} [SemigroupWithZero M₀] [Zero M₀'] [Mul M₀'] (f : M₀M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) :

            Push forward a SemigroupWithZero along a surjective function. See note [reducible non-instances].

            Equations
            Instances For
              @[reducible, inline]
              abbrev Function.Injective.monoidWithZero {M₀ : Type u_1} {M₀' : Type u_3} [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ] [MonoidWithZero M₀] (f : M₀'M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

              Pull back a MonoidWithZero along an injective function. See note [reducible non-instances].

              Equations
              Instances For
                @[reducible, inline]
                abbrev Function.Surjective.monoidWithZero {M₀ : Type u_1} {M₀' : Type u_3} [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ] [MonoidWithZero M₀] (f : M₀M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) (npow : ∀ (x : M₀) (n : ), f (x ^ n) = f x ^ n) :

                Push forward a MonoidWithZero along a surjective function. See note [reducible non-instances].

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Function.Injective.commMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_3} [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ] [CommMonoidWithZero M₀] (f : M₀'M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

                  Pull back a CommMonoidWithZero along an injective function. See note [reducible non-instances].

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Function.Surjective.commMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_3} [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ] [CommMonoidWithZero M₀] (f : M₀M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) (npow : ∀ (x : M₀) (n : ), f (x ^ n) = f x ^ n) :

                    Push forward a CommMonoidWithZero along a surjective function. See note [reducible non-instances].

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev Function.Injective.cancelMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_3} [CancelMonoidWithZero M₀] [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ] (f : M₀'M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

                      Pull back a CancelMonoidWithZero along an injective function. See note [reducible non-instances].

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev Function.Injective.cancelCommMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_3} [CancelCommMonoidWithZero M₀] [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ] (f : M₀'M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

                        Pull back a CancelCommMonoidWithZero along an injective function. See note [reducible non-instances].

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev Function.Injective.groupWithZero {G₀ : Type u_2} {G₀' : Type u_4} [GroupWithZero G₀] [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ] [Pow G₀' ] (f : G₀'G₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀'), f (x * y) = f x * f y) (inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀'), f (x / y) = f x / f y) (npow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) :

                          Pull back a GroupWithZero along an injective function. See note [reducible non-instances].

                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev Function.Surjective.groupWithZero {G₀ : Type u_2} {G₀' : Type u_4} [GroupWithZero G₀] [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ] [Pow G₀' ] (h01 : 0 1) (f : G₀G₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀), f (x * y) = f x * f y) (inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀), f (x / y) = f x / f y) (npow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) :

                            Push forward a GroupWithZero along a surjective function. See note [reducible non-instances].

                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev Function.Injective.commGroupWithZero {G₀ : Type u_2} {G₀' : Type u_4} [CommGroupWithZero G₀] [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ] [Pow G₀' ] (f : G₀'G₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀'), f (x * y) = f x * f y) (inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀'), f (x / y) = f x / f y) (npow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) :

                              Pull back a CommGroupWithZero along an injective function. See note [reducible non-instances].

                              Equations
                              Instances For
                                def Function.Surjective.commGroupWithZero {G₀ : Type u_2} {G₀' : Type u_4} [CommGroupWithZero G₀] [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' ] [Pow G₀' ] (h01 : 0 1) (f : G₀G₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀), f (x * y) = f x * f y) (inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀), f (x / y) = f x / f y) (npow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) :

                                Push forward a CommGroupWithZero along a surjective function. See note [reducible non-instances].

                                Equations
                                Instances For