Documentation

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Non-unital Subalgebras over Commutative Semirings #

In this file we define NonUnitalSubalgebras and the usual operations on them (map, comap).

TODO #

def NonUnitalSubalgebraClass.subtype {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) :
s →ₙₐ[R] A

Embedding of a non-unital subalgebra into the non-unital algebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem NonUnitalSubalgebraClass.coeSubtype {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) :

    A non-unital subalgebra is a sub(semi)ring that is also a submodule.

    • carrier : Set A
    • add_mem' : ∀ {a b : A}, a self.carrierb self.carriera + b self.carrier
    • zero_mem' : 0 self.carrier
    • mul_mem' : ∀ {a b : A}, a self.carrierb self.carriera * b self.carrier
    • smul_mem' : ∀ (c : R) {x : A}, x self.carrierc x self.carrier

      The carrier set is closed under scalar multiplication.

    Instances For
      @[reducible]

      Reinterpret a NonUnitalSubalgebra as a Submodule.

      Equations
      • self.toSubmodule = { toAddSubmonoid := self.toAddSubmonoid, smul_mem' := }
      Instances For
        Equations
        • NonUnitalSubalgebra.instSetLike = { coe := fun (s : NonUnitalSubalgebra R A) => s.carrier, coe_injective' := }
        theorem NonUnitalSubalgebra.mem_carrier {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s : NonUnitalSubalgebra R A} {x : A} :
        x s.carrier x s
        theorem NonUnitalSubalgebra.ext {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : ∀ (x : A), x S x T) :
        S = T
        @[simp]
        theorem NonUnitalSubalgebra.mem_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} :
        x S.toNonUnitalSubsemiring x S
        @[simp]
        theorem NonUnitalSubalgebra.coe_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) :
        S.toNonUnitalSubsemiring = S
        theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] :
        Function.Injective NonUnitalSubalgebra.toNonUnitalSubsemiring
        theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_inj {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} :
        S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring S = U
        theorem NonUnitalSubalgebra.mem_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) {x : A} :
        x S.toSubmodule x S
        @[simp]
        theorem NonUnitalSubalgebra.coe_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) :
        S.toSubmodule = S
        theorem NonUnitalSubalgebra.toSubmodule_inj {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} :
        S.toSubmodule = U.toSubmodule S = U
        def NonUnitalSubalgebra.copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = S) :

        Copy of a non-unital subalgebra with a new carrier equal to the old one. Useful to fix definitional equalities.

        Equations
        • S.copy s hs = let __src := S.copy s hs; { toNonUnitalSubsemiring := __src, smul_mem' := }
        Instances For
          @[simp]
          theorem NonUnitalSubalgebra.coe_copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = S) :
          (S.copy s hs) = s
          theorem NonUnitalSubalgebra.copy_eq {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = S) :
          S.copy s hs = S
          Equations
          • S.instInhabitedSubtypeMem = { default := 0 }

          A non-unital subalgebra over a ring is also a Subring.

          Equations
          • S.toNonUnitalSubring = { toNonUnitalSubsemiring := S.toNonUnitalSubsemiring, neg_mem' := }
          Instances For
            @[simp]
            theorem NonUnitalSubalgebra.mem_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} :
            x S.toNonUnitalSubring x S
            @[simp]
            theorem NonUnitalSubalgebra.coe_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] (S : NonUnitalSubalgebra R A) :
            S.toNonUnitalSubring = S
            theorem NonUnitalSubalgebra.toNonUnitalSubring_injective {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] :
            Function.Injective NonUnitalSubalgebra.toNonUnitalSubring
            theorem NonUnitalSubalgebra.toNonUnitalSubring_inj {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] {S : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} :
            S.toNonUnitalSubring = U.toNonUnitalSubring S = U

            NonUnitalSubalgebras inherit structure from their NonUnitalSubsemiring / Semiring coercions.

            Equations
            • S.toNonUnitalNonAssocSemiring = inferInstance
            Equations
            • S.toNonUnitalSemiring = inferInstance
            Equations
            • S.toNonUnitalCommSemiring = inferInstance
            Equations
            • S.toNonUnitalNonAssocRing = inferInstance
            Equations
            • S.toNonUnitalRing = inferInstance
            Equations
            • S.toNonUnitalCommRing = inferInstance

            The forgetful map from NonUnitalSubalgebra to Submodule as an OrderEmbedding

            Equations
            • NonUnitalSubalgebra.toSubmodule' = { toFun := fun (S : NonUnitalSubalgebra R A) => S.toSubmodule, inj' := , map_rel_iff' := }
            Instances For

              The forgetful map from NonUnitalSubalgebra to NonUnitalSubsemiring as an OrderEmbedding

              Equations
              • NonUnitalSubalgebra.toNonUnitalSubsemiring' = { toFun := fun (S : NonUnitalSubalgebra R A) => S.toNonUnitalSubsemiring, inj' := , map_rel_iff' := }
              Instances For

                The forgetful map from NonUnitalSubalgebra to NonUnitalSubsemiring as an OrderEmbedding

                Equations
                • NonUnitalSubalgebra.toNonUnitalSubring' = { toFun := fun (S : NonUnitalSubalgebra R A) => S.toNonUnitalSubring, inj' := , map_rel_iff' := }
                Instances For

                  NonUnitalSubalgebras inherit structure from their Submodule coercions. #

                  instance NonUnitalSubalgebra.instModule' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] :
                  Module R' S
                  Equations
                  Equations
                  • NonUnitalSubalgebra.instModule = NonUnitalSubalgebra.instModule'
                  instance NonUnitalSubalgebra.instIsScalarTower' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] :
                  IsScalarTower R' R S
                  Equations
                  • =
                  instance NonUnitalSubalgebra.instSMulCommClass' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SMulCommClass R' R A] :
                  SMulCommClass R' R S
                  Equations
                  • =
                  Equations
                  • =
                  theorem NonUnitalSubalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} (x : S) (y : S) :
                  (x + y) = x + y
                  theorem NonUnitalSubalgebra.coe_mul {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} (x : S) (y : S) :
                  (x * y) = x * y
                  theorem NonUnitalSubalgebra.coe_neg {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} (x : S) :
                  (-x) = -x
                  theorem NonUnitalSubalgebra.coe_sub {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} (x : S) (y : S) :
                  (x - y) = x - y
                  @[simp]
                  theorem NonUnitalSubalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : S) :
                  (r x) = r x
                  theorem NonUnitalSubalgebra.coe_eq_zero {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {x : S} :
                  x = 0 x = 0

                  Linear equivalence between S : Submodule R A and S. Though these types are equal, we define it as a LinearEquiv to avoid type equalities.

                  Equations
                  Instances For

                    Transport a non-unital subalgebra via an algebra homomorphism.

                    Equations
                    Instances For
                      theorem NonUnitalSubalgebra.map_mono {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalSubalgebra R A} {f : F} :
                      @[simp]
                      theorem NonUnitalSubalgebra.mem_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {y : B} :
                      y NonUnitalSubalgebra.map f S xS, f x = y
                      theorem NonUnitalSubalgebra.map_toNonUnitalSubsemiring {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} :
                      (NonUnitalSubalgebra.map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (f) S.toNonUnitalSubsemiring
                      @[simp]
                      theorem NonUnitalSubalgebra.coe_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R A) (f : F) :
                      (NonUnitalSubalgebra.map f S) = f '' S

                      Preimage of a non-unital subalgebra under an algebra homomorphism.

                      Equations
                      Instances For
                        @[simp]
                        theorem NonUnitalSubalgebra.mem_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) (x : A) :
                        @[simp]
                        theorem NonUnitalSubalgebra.coe_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) :
                        Equations
                        • =
                        def Submodule.toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x py px * y p) :

                        A submodule closed under multiplication is a non-unital subalgebra.

                        Equations
                        • p.toNonUnitalSubalgebra h_mul = { toAddSubmonoid := p.toAddSubmonoid, mul_mem' := , smul_mem' := }
                        Instances For
                          @[simp]
                          theorem Submodule.mem_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {p : Submodule R A} {h_mul : ∀ (x y : A), x py px * y p} {x : A} :
                          x p.toNonUnitalSubalgebra h_mul x p
                          @[simp]
                          theorem Submodule.coe_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x py px * y p) :
                          (p.toNonUnitalSubalgebra h_mul) = p
                          theorem Submodule.toNonUnitalSubalgebra_mk {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (hmul : ∀ (x y : A), x py px * y p) :
                          p.toNonUnitalSubalgebra hmul = { carrier := p, add_mem' := , zero_mem' := , mul_mem' := , smul_mem' := }
                          @[simp]
                          theorem Submodule.toNonUnitalSubalgebra_toSubmodule {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x py px * y p) :
                          (p.toNonUnitalSubalgebra h_mul).toSubmodule = p
                          @[simp]
                          theorem NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) :
                          S.toSubmodule.toNonUnitalSubalgebra = S
                          def NonUnitalAlgHom.range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) :

                          Range of an NonUnitalAlgHom as a non-unital subalgebra.

                          Equations
                          Instances For
                            @[simp]
                            theorem NonUnitalAlgHom.mem_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) {y : B} :
                            y NonUnitalAlgHom.range φ ∃ (x : A), φ x = y
                            theorem NonUnitalAlgHom.mem_range_self {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (x : A) :
                            @[simp]
                            theorem NonUnitalAlgHom.coe_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) :
                            def NonUnitalAlgHom.codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x S) :
                            A →ₙₐ[R] S

                            Restrict the codomain of a non-unital algebra homomorphism.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem NonUnitalAlgHom.coe_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x S) (x : A) :
                              ((NonUnitalAlgHom.codRestrict f S hf) x) = f x
                              @[reducible, inline]

                              Restrict the codomain of an NonUnitalAlgHom f to f.range.

                              This is the bundled version of Set.rangeFactorization.

                              Equations
                              Instances For
                                def NonUnitalAlgHom.equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (ϕ : F) (ψ : F) :

                                The equalizer of two non-unital R-algebra homomorphisms

                                Equations
                                • NonUnitalAlgHom.equalizer ϕ ψ = { carrier := {a : A | ϕ a = ψ a}, add_mem' := , zero_mem' := , mul_mem' := , smul_mem' := }
                                Instances For
                                  @[simp]
                                  theorem NonUnitalAlgHom.mem_equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (ψ : F) (x : A) :

                                  The range of a morphism of algebras is a fintype, if the domain is a fintype.

                                  Note that this instance can cause a diamond with Subtype.fintype if B is also a fintype.

                                  Equations

                                  The minimal non-unital subalgebra that includes s.

                                  Equations
                                  Instances For
                                    theorem NonUnitalAlgebra.adjoin_induction {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : AProp} {a : A} (h : a NonUnitalAlgebra.adjoin R s) (mem : xs, p x) (add : ∀ (x y : A), p xp yp (x + y)) (zero : p 0) (mul : ∀ (x y : A), p xp yp (x * y)) (smul : ∀ (r : R) (x : A), p xp (r x)) :
                                    p a

                                    If some predicate holds for all x ∈ (s : Set A) and this predicate is closed under the algebraMap, addition, multiplication and star operations, then it holds for a ∈ adjoin R s.

                                    theorem NonUnitalAlgebra.adjoin_induction₂ {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : AAProp} {a : A} {b : A} (ha : a NonUnitalAlgebra.adjoin R s) (hb : b NonUnitalAlgebra.adjoin R s) (Hs : xs, ys, p x y) (H0_left : ∀ (y : A), p 0 y) (H0_right : ∀ (x : A), p x 0) (Hadd_left : ∀ (x₁ x₂ y : A), p x₁ yp x₂ yp (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : A), p x y₁p x y₂p x (y₁ + y₂)) (Hmul_left : ∀ (x₁ x₂ y : A), p x₁ yp x₂ yp (x₁ * x₂) y) (Hmul_right : ∀ (x y₁ y₂ : A), p x y₁p x y₂p x (y₁ * y₂)) (Hsmul_left : ∀ (r : R) (x y : A), p x yp (r x) y) (Hsmul_right : ∀ (r : R) (x y : A), p x yp x (r y)) :
                                    p a b
                                    theorem NonUnitalAlgebra.adjoin_induction_subtype {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : (NonUnitalAlgebra.adjoin R s)Prop} (a : (NonUnitalAlgebra.adjoin R s)) (mem : ∀ (x : A) (h : x s), p x, ) (add : ∀ (x y : (NonUnitalAlgebra.adjoin R s)), p xp yp (x + y)) (zero : p 0) (mul : ∀ (x y : (NonUnitalAlgebra.adjoin R s)), p xp yp (x * y)) (smul : ∀ (r : R) (x : (NonUnitalAlgebra.adjoin R s)), p xp (r x)) :
                                    p a

                                    The difference with NonUnitalAlgebra.adjoin_induction is that this acts on the subtype.

                                    theorem NonUnitalAlgebra.adjoin_induction' {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : (x : A) → x NonUnitalAlgebra.adjoin R sProp} (mem : ∀ (x : A) (h : x s), p x ) (add : ∀ (x : A) (hx : x NonUnitalAlgebra.adjoin R s) (y : A) (hy : y NonUnitalAlgebra.adjoin R s), p x hxp y hyp (x + y) ) (zero : p 0 ) (mul : ∀ (x : A) (hx : x NonUnitalAlgebra.adjoin R s) (y : A) (hy : y NonUnitalAlgebra.adjoin R s), p x hxp y hyp (x * y) ) (smul : ∀ (r : R) (x : A) (hx : x NonUnitalAlgebra.adjoin R s), p x hxp (r x) ) {a : A} (ha : a NonUnitalAlgebra.adjoin R s) :
                                    p a ha

                                    A dependent version of NonUnitalAlgebra.adjoin_induction.

                                    Galois insertion between adjoin and Subtype.val.

                                    Equations
                                    Instances For
                                      Equations
                                      • NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra = NonUnitalAlgebra.gi.liftCompleteLattice
                                      @[simp]
                                      @[simp]
                                      theorem NonUnitalAlgebra.coe_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :
                                      = Set.univ
                                      @[simp]
                                      theorem NonUnitalAlgebra.mem_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} :
                                      @[simp]
                                      @[simp]
                                      theorem NonUnitalAlgebra.top_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :
                                      .toNonUnitalSubsemiring =
                                      @[simp]
                                      theorem NonUnitalAlgebra.top_toSubring {R : Type u_2} {A : Type u_3} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :
                                      .toNonUnitalSubring =
                                      @[simp]
                                      @[simp]
                                      theorem NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} :
                                      S.toNonUnitalSubsemiring = S =
                                      @[simp]
                                      theorem NonUnitalAlgebra.to_subring_eq_top {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} :
                                      S.toNonUnitalSubring = S =
                                      theorem NonUnitalAlgebra.mem_sup_left {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} :
                                      x Sx S T
                                      theorem NonUnitalAlgebra.mem_sup_right {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} :
                                      x Tx S T
                                      theorem NonUnitalAlgebra.mul_mem_sup {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} {y : A} (hx : x S) (hy : y T) :
                                      x * y S T
                                      @[simp]
                                      theorem NonUnitalAlgebra.coe_inf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) (T : NonUnitalSubalgebra R A) :
                                      (S T) = S T
                                      @[simp]
                                      theorem NonUnitalAlgebra.mem_inf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} :
                                      x S T x S x T
                                      @[simp]
                                      theorem NonUnitalAlgebra.inf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) (T : NonUnitalSubalgebra R A) :
                                      (S T).toSubmodule = S.toSubmodule T.toSubmodule
                                      @[simp]
                                      theorem NonUnitalAlgebra.inf_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) (T : NonUnitalSubalgebra R A) :
                                      (S T).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring T.toNonUnitalSubsemiring
                                      @[simp]
                                      theorem NonUnitalAlgebra.coe_sInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) :
                                      (sInf S) = sS, s
                                      theorem NonUnitalAlgebra.mem_sInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : Set (NonUnitalSubalgebra R A)} {x : A} :
                                      x sInf S pS, x p
                                      @[simp]
                                      theorem NonUnitalAlgebra.sInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) :
                                      (sInf S).toSubmodule = sInf (NonUnitalSubalgebra.toSubmodule '' S)
                                      @[simp]
                                      theorem NonUnitalAlgebra.sInf_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) :
                                      (sInf S).toNonUnitalSubsemiring = sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S)
                                      @[simp]
                                      theorem NonUnitalAlgebra.coe_iInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} {S : ιNonUnitalSubalgebra R A} :
                                      (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                                      theorem NonUnitalAlgebra.mem_iInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} {S : ιNonUnitalSubalgebra R A} {x : A} :
                                      x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                      @[simp]
                                      theorem NonUnitalAlgebra.iInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} (S : ιNonUnitalSubalgebra R A) :
                                      (⨅ (i : ι), S i).toSubmodule = ⨅ (i : ι), (S i).toSubmodule
                                      Equations
                                      • NonUnitalAlgebra.instInhabitedNonUnitalSubalgebra = { default := }
                                      theorem NonUnitalAlgebra.mem_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} :
                                      x x = 0
                                      @[simp]
                                      theorem NonUnitalAlgebra.coe_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :
                                      = {0}
                                      theorem NonUnitalAlgebra.eq_top_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} :
                                      S = ∀ (x : A), x S

                                      NonUnitalAlgHom to ⊤ : NonUnitalSubalgebra R A.

                                      Equations
                                      Instances For

                                        The map S → T when S is a non-unital subalgebra contained in the non-unital subalgebra T.

                                        This is the non-unital subalgebra version of Submodule.inclusion, or Subring.inclusion

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem NonUnitalSubalgebra.inclusion_mk {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S T) (x : A) (hx : x S) :
                                          (NonUnitalSubalgebra.inclusion h) x, hx = x,
                                          theorem NonUnitalSubalgebra.inclusion_right {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S T) (x : T) (m : x S) :
                                          (NonUnitalSubalgebra.inclusion h) x, m = x
                                          @[simp]
                                          theorem NonUnitalSubalgebra.coe_inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S T) (s : S) :

                                          The product of two non-unital subalgebras is a non-unital subalgebra.

                                          Equations
                                          • S.prod S₁ = let __src := S.prod S₁.toNonUnitalSubsemiring; { carrier := S ×ˢ S₁, add_mem' := , zero_mem' := , mul_mem' := , smul_mem' := }
                                          Instances For
                                            @[simp]
                                            theorem NonUnitalSubalgebra.coe_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] (S : NonUnitalSubalgebra R A) (S₁ : NonUnitalSubalgebra R B) :
                                            (S.prod S₁) = S ×ˢ S₁
                                            theorem NonUnitalSubalgebra.prod_toSubmodule {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] (S : NonUnitalSubalgebra R A) (S₁ : NonUnitalSubalgebra R B) :
                                            (S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule
                                            @[simp]
                                            theorem NonUnitalSubalgebra.mem_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] {S : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {x : A × B} :
                                            x S.prod S₁ x.1 S x.2 S₁
                                            theorem NonUnitalSubalgebra.prod_mono {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {T₁ : NonUnitalSubalgebra R B} :
                                            S TS₁ T₁S.prod S₁ T.prod T₁
                                            @[simp]
                                            theorem NonUnitalSubalgebra.prod_inf_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {T₁ : NonUnitalSubalgebra R B} :
                                            S.prod S₁ T.prod T₁ = (S T).prod (S₁ T₁)
                                            theorem NonUnitalSubalgebra.coe_iSup_of_directed {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Type u_1} [Nonempty ι] {S : ιNonUnitalSubalgebra R A} (dir : Directed (fun (x x_1 : NonUnitalSubalgebra R A) => x x_1) S) :
                                            (iSup S) = ⋃ (i : ι), (S i)
                                            noncomputable def NonUnitalSubalgebra.iSupLift {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] (K : ιNonUnitalSubalgebra R A) (dir : Directed (fun (x x_1 : NonUnitalSubalgebra R A) => x x_1) K) (f : (i : ι) → (K i) →ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)) (T : NonUnitalSubalgebra R A) (hT : T = iSup K) :
                                            T →ₙₐ[R] B

                                            Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining it on each non-unital subalgebra, and proving that it agrees on the intersection of non-unital subalgebras.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem NonUnitalSubalgebra.iSupLift_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ιNonUnitalSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalSubalgebra R A) => x x_1) K} {f : (i : ι) → (K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : (K i)) (h : K i T) :
                                              @[simp]
                                              theorem NonUnitalSubalgebra.iSupLift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ιNonUnitalSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalSubalgebra R A) => x x_1) K} {f : (i : ι) → (K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i T) :
                                              @[simp]
                                              theorem NonUnitalSubalgebra.iSupLift_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ιNonUnitalSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalSubalgebra R A) => x x_1) K} {f : (i : ι) → (K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : (K i)) (hx : x T) :
                                              (NonUnitalSubalgebra.iSupLift K dir f hf T hT) x, hx = (f i) x
                                              theorem NonUnitalSubalgebra.iSupLift_of_mem {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ιNonUnitalSubalgebra R A} {dir : Directed (fun (x x_1 : NonUnitalSubalgebra R A) => x x_1) K} {f : (i : ι) → (K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : T) (hx : x K i) :
                                              (NonUnitalSubalgebra.iSupLift K dir f hf T hT) x = (f i) x, hx
                                              theorem Set.smul_mem_center {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (r : R) {a : A} (ha : a Set.center A) :

                                              The center of a non-unital algebra is the set of elements which commute with every element. They form a non-unital subalgebra.

                                              Equations
                                              Instances For

                                                The center of a non-unital algebra is commutative and associative

                                                Equations
                                                theorem NonUnitalSubalgebra.mem_center_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} :
                                                a NonUnitalSubalgebra.center R A ∀ (b : A), b * a = a * b
                                                @[simp]
                                                theorem Set.smul_mem_centralizer {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (r : R) {a : A} (ha : a s.centralizer) :
                                                r a s.centralizer

                                                The centralizer of a set as a non-unital subalgebra.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem NonUnitalSubalgebra.coe_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) :
                                                  (NonUnitalSubalgebra.centralizer R s) = s.centralizer
                                                  theorem NonUnitalSubalgebra.mem_centralizer_iff (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {z : A} :
                                                  z NonUnitalSubalgebra.centralizer R s gs, g * z = z * g

                                                  A non-unital subsemiring is a non-unital -subalgebra.

                                                  Equations
                                                  Instances For

                                                    A non-unital subring is a non-unital -subalgebra.

                                                    Equations
                                                    Instances For