Documentation

Mathlib.Algebra.Group.TransferInstance

Transfer algebraic structures across Equivs #

In this file we prove lemmas of the following form: if β has a group structure and α ≃ β then α has a group structure, and similarly for monoids, semigroups and so on.

Implementation details #

When adding new definitions that transfer type-classes across an equivalence, please use abbrev. See note [reducible non-instances].

@[reducible, inline]
abbrev Equiv.one {α : Type u_2} {β : Type u_3} (e : α β) [One β] :
One α

Transfer One across an Equiv

Equations
Instances For
    @[reducible, inline]
    abbrev Equiv.zero {α : Type u_2} {β : Type u_3} (e : α β) [Zero β] :
    Zero α

    Transfer Zero across an Equiv

    Equations
    Instances For
      theorem Equiv.one_def {α : Type u_2} {β : Type u_3} (e : α β) [One β] :
      1 = e.symm 1
      theorem Equiv.zero_def {α : Type u_2} {β : Type u_3} (e : α β) [Zero β] :
      0 = e.symm 0
      @[reducible, inline]
      abbrev Equiv.mul {α : Type u_2} {β : Type u_3} (e : α β) [Mul β] :
      Mul α

      Transfer Mul across an Equiv

      Equations
      • e.mul = { mul := fun (x y : α) => e.symm (e x * e y) }
      Instances For
        @[reducible, inline]
        abbrev Equiv.add {α : Type u_2} {β : Type u_3} (e : α β) [Add β] :
        Add α

        Transfer Add across an Equiv

        Equations
        • e.add = { add := fun (x y : α) => e.symm (e x + e y) }
        Instances For
          theorem Equiv.mul_def {α : Type u_2} {β : Type u_3} (e : α β) [Mul β] (x y : α) :
          x * y = e.symm (e x * e y)
          theorem Equiv.add_def {α : Type u_2} {β : Type u_3} (e : α β) [Add β] (x y : α) :
          x + y = e.symm (e x + e y)
          @[reducible, inline]
          abbrev Equiv.div {α : Type u_2} {β : Type u_3} (e : α β) [Div β] :
          Div α

          Transfer Div across an Equiv

          Equations
          • e.div = { div := fun (x y : α) => e.symm (e x / e y) }
          Instances For
            @[reducible, inline]
            abbrev Equiv.sub {α : Type u_2} {β : Type u_3} (e : α β) [Sub β] :
            Sub α

            Transfer Sub across an Equiv

            Equations
            • e.sub = { sub := fun (x y : α) => e.symm (e x - e y) }
            Instances For
              theorem Equiv.div_def {α : Type u_2} {β : Type u_3} (e : α β) [Div β] (x y : α) :
              x / y = e.symm (e x / e y)
              theorem Equiv.sub_def {α : Type u_2} {β : Type u_3} (e : α β) [Sub β] (x y : α) :
              x - y = e.symm (e x - e y)
              @[reducible, inline]
              abbrev Equiv.Inv {α : Type u_2} {β : Type u_3} (e : α β) [Inv β] :
              Inv α

              Transfer Inv across an Equiv

              Equations
              Instances For
                @[reducible, inline]
                abbrev Equiv.Neg {α : Type u_2} {β : Type u_3} (e : α β) [Neg β] :
                Neg α

                Transfer Neg across an Equiv

                Equations
                Instances For
                  theorem Equiv.inv_def {α : Type u_2} {β : Type u_3} (e : α β) [Inv β] (x : α) :
                  x⁻¹ = e.symm (e x)⁻¹
                  theorem Equiv.neg_def {α : Type u_2} {β : Type u_3} (e : α β) [Neg β] (x : α) :
                  -x = e.symm (-e x)
                  @[reducible, inline]
                  abbrev Equiv.smul (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α β) [SMul M β] :
                  SMul M α

                  Transfer SMul across an Equiv

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Equiv.vadd (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α β) [VAdd M β] :
                    VAdd M α

                    Transfer VAdd across an Equiv

                    Equations
                    Instances For
                      theorem Equiv.smul_def {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α β) [SMul M β] (r : M) (x : α) :
                      r x = e.symm (r e x)
                      theorem Equiv.vadd_def {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α β) [VAdd M β] (r : M) (x : α) :
                      r +ᵥ x = e.symm (r +ᵥ e x)
                      @[reducible, inline]
                      abbrev Equiv.pow (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α β) [Pow β M] :
                      Pow α M

                      Transfer Pow across an Equiv

                      Equations
                      Instances For
                        theorem Equiv.pow_def {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α β) [Pow β M] (n : M) (x : α) :
                        x ^ n = e.symm (e x ^ n)
                        def Equiv.mulEquiv {α : Type u_2} {β : Type u_3} (e : α β) [Mul β] :
                        have x := e.mul; α ≃* β

                        An equivalence e : α ≃ β gives a multiplicative equivalence α ≃* β where the multiplicative structure on α is the one obtained by transporting a multiplicative structure on β back along e.

                        Equations
                        Instances For
                          def Equiv.addEquiv {α : Type u_2} {β : Type u_3} (e : α β) [Add β] :
                          have x := e.add; α ≃+ β

                          An equivalence e : α ≃ β gives an additive equivalence α ≃+ β where the additive structure on α is the one obtained by transporting an additive structure on β back along e.

                          Equations
                          Instances For
                            @[simp]
                            theorem Equiv.mulEquiv_apply {α : Type u_2} {β : Type u_3} (e : α β) [Mul β] (a : α) :
                            e.mulEquiv a = e a
                            @[simp]
                            theorem Equiv.addEquiv_apply {α : Type u_2} {β : Type u_3} (e : α β) [Add β] (a : α) :
                            e.addEquiv a = e a
                            theorem Equiv.mulEquiv_symm_apply {α : Type u_2} {β : Type u_3} (e : α β) [Mul β] (b : β) :
                            theorem Equiv.addEquiv_symm_apply {α : Type u_2} {β : Type u_3} (e : α β) [Add β] (b : β) :
                            @[reducible, inline]
                            abbrev Equiv.semigroup {α : Type u_2} {β : Type u_3} (e : α β) [Semigroup β] :

                            Transfer Semigroup across an Equiv

                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev Equiv.addSemigroup {α : Type u_2} {β : Type u_3} (e : α β) [AddSemigroup β] :

                              Transfer add_semigroup across an Equiv

                              Equations
                              Instances For
                                @[reducible, inline]
                                abbrev Equiv.commSemigroup {α : Type u_2} {β : Type u_3} (e : α β) [CommSemigroup β] :

                                Transfer CommSemigroup across an Equiv

                                Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev Equiv.addCommSemigroup {α : Type u_2} {β : Type u_3} (e : α β) [AddCommSemigroup β] :

                                  Transfer AddCommSemigroup across an Equiv

                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev Equiv.mulOneClass {α : Type u_2} {β : Type u_3} (e : α β) [MulOneClass β] :

                                    Transfer MulOneClass across an Equiv

                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev Equiv.addZeroClass {α : Type u_2} {β : Type u_3} (e : α β) [AddZeroClass β] :

                                      Transfer AddZeroClass across an Equiv

                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev Equiv.monoid {α : Type u_2} {β : Type u_3} (e : α β) [Monoid β] :

                                        Transfer Monoid across an Equiv

                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          abbrev Equiv.addMonoid {α : Type u_2} {β : Type u_3} (e : α β) [AddMonoid β] :

                                          Transfer AddMonoid across an Equiv

                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev Equiv.commMonoid {α : Type u_2} {β : Type u_3} (e : α β) [CommMonoid β] :

                                            Transfer CommMonoid across an Equiv

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev Equiv.addCommMonoid {α : Type u_2} {β : Type u_3} (e : α β) [AddCommMonoid β] :

                                              Transfer AddCommMonoid across an Equiv

                                              Equations
                                              Instances For
                                                @[reducible, inline]
                                                abbrev Equiv.group {α : Type u_2} {β : Type u_3} (e : α β) [Group β] :

                                                Transfer Group across an Equiv

                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev Equiv.addGroup {α : Type u_2} {β : Type u_3} (e : α β) [AddGroup β] :

                                                  Transfer AddGroup across an Equiv

                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev Equiv.commGroup {α : Type u_2} {β : Type u_3} (e : α β) [CommGroup β] :

                                                    Transfer CommGroup across an Equiv

                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev Equiv.addCommGroup {α : Type u_2} {β : Type u_3} (e : α β) [AddCommGroup β] :

                                                      Transfer AddCommGroup across an Equiv

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev Equiv.mulAction (M : Type u_1) {α : Type u_2} {β : Type u_3} [Monoid M] (e : α β) [MulAction M β] :

                                                        Transfer MulAction across an Equiv

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev Equiv.addAction (M : Type u_1) {α : Type u_2} {β : Type u_3} [AddMonoid M] (e : α β) [AddAction M β] :

                                                          Transfer AddAction across an Equiv

                                                          Equations
                                                          Instances For
                                                            theorem Finite.exists_type_univ_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
                                                            ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

                                                            Any finite group in universe u is equivalent to some finite group in universe v.

                                                            theorem Finite.exists_type_univ_nonempty_addEquiv (G : Type u) [AddGroup G] [Finite G] :
                                                            ∃ (G' : Type v) (x : AddGroup G') (x_1 : Fintype G'), Nonempty (G ≃+ G')

                                                            Any finite group in universe u is equivalent to some finite group in universe v.