Documentation

Mathlib.Algebra.Group.Submonoid.Pointwise

Pointwise instances on Submonoids and AddSubmonoids #

This file provides:

and the actions

which matches the action of Set.mulActionSet.

These are all available in the Pointwise locale.

Additionally, it provides various degrees of monoid structure:

Implementation notes #

Most of the lemmas in this file are direct copies of lemmas from Algebra/Pointwise.lean. While the statements of these lemmas are defeq, we repeat them here due to them not being syntactically equal. Before adding new lemmas here, consider if they would also apply to the action on Sets.

Some lemmas about pointwise multiplication and submonoids. Ideally we put these in GroupTheory.Submonoid.Basic, but currently we cannot because that file is imported by this.

theorem AddSubmonoid.add_subset {M : Type u_3} [AddMonoid M] {s : Set M} {t : Set M} {S : AddSubmonoid M} (hs : s S) (ht : t S) :
s + t S
theorem Submonoid.mul_subset {M : Type u_3} [Monoid M] {s : Set M} {t : Set M} {S : Submonoid M} (hs : s S) (ht : t S) :
s * t S
theorem AddSubmonoid.add_subset_closure {M : Type u_3} [AddMonoid M] {s : Set M} {t : Set M} {u : Set M} (hs : s u) (ht : t u) :
theorem Submonoid.mul_subset_closure {M : Type u_3} [Monoid M] {s : Set M} {t : Set M} {u : Set M} (hs : s u) (ht : t u) :
theorem AddSubmonoid.coe_add_self_eq {M : Type u_3} [AddMonoid M] (s : AddSubmonoid M) :
s + s = s
theorem Submonoid.coe_mul_self_eq {M : Type u_3} [Monoid M] (s : Submonoid M) :
s * s = s
abbrev AddSubmonoid.closure_add_le.match_1 {M : Type u_1} [AddMonoid M] (S : Set M) (T : Set M) (_x : M) (motive : _x S + TProp) :
∀ (x : _x S + T), (∀ (_s : M) (hs : _s S) (_t : M) (ht : _t T) (hx : (fun (x x_1 : M) => x + x_1) _s _t = _x), motive )motive x
Equations
  • =
Instances For
    theorem Submonoid.sup_eq_closure_mul {M : Type u_3} [Monoid M] (H : Submonoid M) (K : Submonoid M) :
    H K = Submonoid.closure (H * K)
    theorem AddSubmonoid.nsmul_vadd_mem_closure_vadd {M : Type u_3} [AddMonoid M] {N : Type u_6} [AddCommMonoid N] [AddAction M N] [VAddAssocClass M N N] (r : M) (s : Set N) {x : N} (hx : x AddSubmonoid.closure s) :
    ∃ (n : ), n r +ᵥ x AddSubmonoid.closure (r +ᵥ s)
    theorem Submonoid.pow_smul_mem_closure_smul {M : Type u_3} [Monoid M] {N : Type u_6} [CommMonoid N] [MulAction M N] [IsScalarTower M N N] (r : M) (s : Set N) {x : N} (hx : x Submonoid.closure s) :
    ∃ (n : ), r ^ n x Submonoid.closure (r s)
    theorem AddSubmonoid.neg.proof_1 {G : Type u_1} [AddGroup G] (S : AddSubmonoid G) :
    ∀ {a b : G}, a -Sb -Sa + b -S
    theorem AddSubmonoid.neg.proof_2 {G : Type u_1} [AddGroup G] (S : AddSubmonoid G) :
    0 -S

    The additive submonoid with every element negated.

    Equations
    • AddSubmonoid.neg = { neg := fun (S : AddSubmonoid G) => { carrier := -S, add_mem' := , zero_mem' := } }
    Instances For
      def Submonoid.inv {G : Type u_2} [Group G] :

      The submonoid with every element inverted.

      Equations
      • Submonoid.inv = { inv := fun (S : Submonoid G) => { carrier := (S)⁻¹, mul_mem' := , one_mem' := } }
      Instances For
        @[simp]
        theorem AddSubmonoid.coe_neg {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) :
        (-S) = -S
        @[simp]
        theorem Submonoid.coe_inv {G : Type u_2} [Group G] (S : Submonoid G) :
        S⁻¹ = (S)⁻¹
        @[simp]
        theorem AddSubmonoid.mem_neg {G : Type u_2} [AddGroup G] {g : G} {S : AddSubmonoid G} :
        g -S -g S
        @[simp]
        theorem Submonoid.mem_inv {G : Type u_2} [Group G] {g : G} {S : Submonoid G} :

        Inversion is involutive on additive submonoids.

        Equations
        Instances For
          theorem AddSubmonoid.involutiveNeg.proof_2 {G : Type u_1} [AddGroup G] :
          ∀ (x : AddSubmonoid G), (-x) = (-x)

          Inversion is involutive on submonoids.

          Equations
          Instances For
            @[simp]
            theorem AddSubmonoid.neg_le_neg {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) (T : AddSubmonoid G) :
            -S -T S T
            @[simp]
            theorem Submonoid.inv_le_inv {G : Type u_2} [Group G] (S : Submonoid G) (T : Submonoid G) :
            theorem AddSubmonoid.neg_le {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) (T : AddSubmonoid G) :
            -S T S -T
            theorem Submonoid.inv_le {G : Type u_2} [Group G] (S : Submonoid G) (T : Submonoid G) :

            Pointwise negation of additive submonoids as an order isomorphism

            Equations
            Instances For
              @[simp]
              theorem AddSubmonoid.negOrderIso_apply_coe {G : Type u_2} [AddGroup G] :
              ∀ (a : AddSubmonoid G), (AddSubmonoid.negOrderIso a) = -a
              @[simp]
              theorem AddSubmonoid.negOrderIso_symm_apply_coe {G : Type u_2} [AddGroup G] :
              ∀ (a : AddSubmonoid G), ((RelIso.symm AddSubmonoid.negOrderIso) a) = -a
              @[simp]
              theorem Submonoid.invOrderIso_apply_coe {G : Type u_2} [Group G] :
              ∀ (a : Submonoid G), (Submonoid.invOrderIso a) = (a)⁻¹
              @[simp]
              theorem Submonoid.invOrderIso_symm_apply_coe {G : Type u_2} [Group G] :
              ∀ (a : Submonoid G), ((RelIso.symm Submonoid.invOrderIso) a) = (a)⁻¹

              Pointwise inversion of submonoids as an order isomorphism.

              Equations
              Instances For
                @[simp]
                theorem AddSubmonoid.neg_inf {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) (T : AddSubmonoid G) :
                -(S T) = -S -T
                @[simp]
                theorem Submonoid.inv_inf {G : Type u_2} [Group G] (S : Submonoid G) (T : Submonoid G) :
                @[simp]
                theorem AddSubmonoid.neg_sup {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) (T : AddSubmonoid G) :
                -(S T) = -S -T
                @[simp]
                theorem Submonoid.inv_sup {G : Type u_2} [Group G] (S : Submonoid G) (T : Submonoid G) :
                @[simp]
                theorem AddSubmonoid.neg_bot {G : Type u_2} [AddGroup G] :
                @[simp]
                theorem Submonoid.inv_bot {G : Type u_2} [Group G] :
                @[simp]
                theorem AddSubmonoid.neg_top {G : Type u_2} [AddGroup G] :
                @[simp]
                theorem Submonoid.inv_top {G : Type u_2} [Group G] :
                @[simp]
                theorem AddSubmonoid.neg_iInf {G : Type u_2} [AddGroup G] {ι : Sort u_6} (S : ιAddSubmonoid G) :
                -⨅ (i : ι), S i = ⨅ (i : ι), -S i
                @[simp]
                theorem Submonoid.inv_iInf {G : Type u_2} [Group G] {ι : Sort u_6} (S : ιSubmonoid G) :
                (⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹
                @[simp]
                theorem AddSubmonoid.neg_iSup {G : Type u_2} [AddGroup G] {ι : Sort u_6} (S : ιAddSubmonoid G) :
                -⨆ (i : ι), S i = ⨆ (i : ι), -S i
                @[simp]
                theorem Submonoid.inv_iSup {G : Type u_2} [Group G] {ι : Sort u_6} (S : ιSubmonoid G) :
                (⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹

                The action on a submonoid corresponding to applying the action to every element.

                This is available as an instance in the Pointwise locale.

                Equations
                Instances For
                  @[simp]
                  theorem Submonoid.coe_pointwise_smul {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (S : Submonoid M) :
                  (a S) = a S
                  theorem Submonoid.smul_mem_pointwise_smul {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (m : M) (a : α) (S : Submonoid M) :
                  m Sa m a S
                  instance Submonoid.instCovariantClassHSMulLe {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] :
                  CovariantClass α (Submonoid M) HSMul.hSMul LE.le
                  Equations
                  • =
                  theorem Submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (m : M) (a : α) (S : Submonoid M) :
                  m a S sS, a s = m
                  @[simp]
                  theorem Submonoid.smul_bot {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) :
                  theorem Submonoid.smul_sup {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (S : Submonoid M) (T : Submonoid M) :
                  a (S T) = a S a T
                  theorem Submonoid.smul_closure {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (s : Set M) :
                  @[simp]
                  theorem Submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :
                  a x a S x S
                  theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :
                  x a S a⁻¹ x S
                  theorem Submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :
                  x a⁻¹ S a x S
                  @[simp]
                  theorem Submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {T : Submonoid M} :
                  a S a T S T
                  theorem Submonoid.pointwise_smul_subset_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {T : Submonoid M} :
                  a S T S a⁻¹ T
                  theorem Submonoid.subset_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {T : Submonoid M} :
                  S a T a⁻¹ S T
                  @[simp]
                  theorem Submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) (S : Submonoid M) (x : M) :
                  a x a S x S
                  theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) (S : Submonoid M) (x : M) :
                  x a S a⁻¹ x S
                  theorem Submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) (S : Submonoid M) (x : M) :
                  x a⁻¹ S a x S
                  @[simp]
                  theorem Submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) {S : Submonoid M} {T : Submonoid M} :
                  a S a T S T
                  theorem Submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) {S : Submonoid M} {T : Submonoid M} :
                  a S T S a⁻¹ T
                  theorem Submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero α] [MulDistribMulAction α M] {a : α} (ha : a 0) {S : Submonoid M} {T : Submonoid M} :
                  S a T a⁻¹ S T

                  The action on an additive submonoid corresponding to applying the action to every element.

                  This is available as an instance in the Pointwise locale.

                  Equations
                  Instances For
                    @[simp]
                    theorem AddSubmonoid.coe_pointwise_smul {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) (S : AddSubmonoid A) :
                    (a S) = a S
                    theorem AddSubmonoid.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (m : A) (a : α) (S : AddSubmonoid A) :
                    m Sa m a S
                    theorem AddSubmonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (m : A) (a : α) (S : AddSubmonoid A) :
                    m a S sS, a s = m
                    @[simp]
                    theorem AddSubmonoid.smul_bot {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) :
                    theorem AddSubmonoid.smul_sup {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) (S : AddSubmonoid A) (T : AddSubmonoid A) :
                    a (S T) = a S a T
                    @[simp]
                    theorem AddSubmonoid.smul_closure {α : Type u_1} {A : Type u_5} [AddMonoid A] [Monoid α] [DistribMulAction α A] (a : α) (s : Set A) :
                    @[simp]
                    theorem AddSubmonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {x : A} :
                    a x a S x S
                    theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {x : A} :
                    x a S a⁻¹ x S
                    theorem AddSubmonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {x : A} :
                    x a⁻¹ S a x S
                    @[simp]
                    theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {T : AddSubmonoid A} :
                    a S a T S T
                    theorem AddSubmonoid.pointwise_smul_le_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {T : AddSubmonoid A} :
                    a S T S a⁻¹ T
                    theorem AddSubmonoid.le_pointwise_smul_iff {α : Type u_1} {A : Type u_5} [AddMonoid A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubmonoid A} {T : AddSubmonoid A} :
                    S a T a⁻¹ S T
                    @[simp]
                    theorem AddSubmonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) (S : AddSubmonoid A) (x : A) :
                    a x a S x S
                    theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) (S : AddSubmonoid A) (x : A) :
                    x a S a⁻¹ x S
                    theorem AddSubmonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) (S : AddSubmonoid A) (x : A) :
                    x a⁻¹ S a x S
                    @[simp]
                    theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) {S : AddSubmonoid A} {T : AddSubmonoid A} :
                    a S a T S T
                    theorem AddSubmonoid.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) {S : AddSubmonoid A} {T : AddSubmonoid A} :
                    a S T S a⁻¹ T
                    theorem AddSubmonoid.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_5} [AddMonoid A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a 0) {S : AddSubmonoid A} {T : AddSubmonoid A} :
                    S a T a⁻¹ S T

                    Elementwise monoid structure of additive submonoids #

                    These definitions are a cut-down versions of the ones around Submodule.mul, as that API is usually more useful.

                    If R is an additive monoid with one (e.g., a semiring), then 1 : AddSubmonoid R is the range of Nat.cast : ℕ → R.

                    Equations
                    Instances For
                      theorem AddSubmonoid.natCast_mem_one {R : Type u_4} [AddMonoidWithOne R] (n : ) :
                      n 1
                      @[simp]
                      theorem AddSubmonoid.mem_one {R : Type u_4} [AddMonoidWithOne R] {x : R} :
                      x 1 ∃ (n : ), n = x

                      Multiplication of additive submonoids of a semiring R. The additive submonoid S * T is the smallest R-submodule of R containing the elements s * t for s ∈ S and t ∈ T.

                      Equations
                      Instances For
                        theorem AddSubmonoid.mul_mem_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {m : R} {n : R} (hm : m M) (hn : n N) :
                        m * n M * N
                        theorem AddSubmonoid.mul_le {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {P : AddSubmonoid R} :
                        M * N P mM, nN, m * n P
                        theorem AddSubmonoid.mul_induction_on {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {C : RProp} {r : R} (hr : r M * N) (hm : mM, nN, C (m * n)) (ha : ∀ (x y : R), C xC yC (x + y)) :
                        C r
                        theorem AddSubmonoid.mul_le_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {P : AddSubmonoid R} {Q : AddSubmonoid R} (hmp : M P) (hnq : N Q) :
                        M * N P * Q
                        theorem AddSubmonoid.mul_le_mul_left {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {P : AddSubmonoid R} (h : M N) :
                        M * P N * P
                        theorem AddSubmonoid.mul_le_mul_right {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} {P : AddSubmonoid R} (h : N P) :
                        M * N M * P
                        theorem AddSubmonoid.mul_subset_mul {R : Type u_4} [NonUnitalNonAssocSemiring R] {M : AddSubmonoid R} {N : AddSubmonoid R} :
                        M * N (M * N)

                        AddSubmonoid.neg distributes over multiplication.

                        This is available as an instance in the Pointwise locale.

                        Equations
                        • AddSubmonoid.hasDistribNeg = let __src := AddSubmonoid.involutiveNeg; HasDistribNeg.mk
                        Instances For

                          A MulOneClass structure on additive submonoids of a (possibly, non-associative) semiring.

                          Equations
                          Instances For

                            Semigroup structure on additive submonoids of a (possibly, non-unital) semiring.

                            Equations
                            Instances For

                              Monoid structure on additive submonoids of a semiring.

                              Equations
                              • AddSubmonoid.monoid = let __src := AddSubmonoid.semigroup; let __src_1 := AddSubmonoid.mulOneClass; Monoid.mk npowRec
                              Instances For
                                theorem AddSubmonoid.pow_subset_pow {R : Type u_4} [Semiring R] {s : AddSubmonoid R} {n : } :
                                s ^ n (s ^ n)
                                theorem Set.IsPWO.addSubmonoid_closure {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} (hpos : xs, 0 x) (h : s.IsPWO) :
                                ((AddSubmonoid.closure s)).IsPWO
                                theorem Set.IsPWO.submonoid_closure {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} (hpos : xs, 1 x) (h : s.IsPWO) :
                                ((Submonoid.closure s)).IsPWO