Documentation

Mathlib.Algebra.Algebra.Subalgebra.Basic

Subalgebras over Commutative Semiring #

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

The Algebra.adjoin operation and complete lattice structure can be found in Mathlib.Algebra.Algebra.Subalgebra.Lattice.

structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] extends Subsemiring A :

A subalgebra is a sub(semi)ring that includes the range of algebraMap.

Instances For
    instance Subalgebra.instSetLike {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
    Equations
    def Subalgebra.ofClass {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [SMulMemClass S R A] (s : S) :

    The actual Subalgebra obtained from an element of a type satisfying SubsemiringClass and SMulMemClass.

    Equations
    • Subalgebra.ofClass s = { carrier := s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
    Instances For
      @[simp]
      theorem Subalgebra.coe_ofClass {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [SMulMemClass S R A] (s : S) :
      (ofClass s) = s
      @[instance 100]
      instance Subalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMap {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
      CanLift (Set A) (Subalgebra R A) SetLike.coe fun (s : Set A) => (∀ {x y : A}, x sy sx + y s) (∀ {x y : A}, x sy sx * y s) ∀ (r : R), (algebraMap R A) r s
      @[simp]
      theorem Subalgebra.mem_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {x : A} :
      theorem Subalgebra.mem_carrier {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Subalgebra R A} {x : A} :
      x s.carrier x s
      theorem Subalgebra.ext {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : ∀ (x : A), x S x T) :
      S = T
      theorem Subalgebra.ext_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} :
      S = T ∀ (x : A), x S x T
      @[simp]
      theorem Subalgebra.coe_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
      S.toSubsemiring = S
      def Subalgebra.copy {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (s : Set A) (hs : s = S) :

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

      Equations
      • S.copy s hs = { carrier := s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
      Instances For
        @[simp]
        theorem Subalgebra.coe_copy {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (s : Set A) (hs : s = S) :
        (S.copy s hs) = s
        @[simp]
        theorem Subalgebra.copy_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (s : Set A) (hs : s = S) :
        (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := }
        theorem Subalgebra.copy_eq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (s : Set A) (hs : s = S) :
        S.copy s hs = S
        theorem algebraMap_mem {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [OneMemClass S A] [SMulMemClass S R A] (s : S) (r : R) :
        (algebraMap R A) r s
        theorem Subalgebra.algebraMap_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (r : R) :
        (algebraMap R A) r S
        theorem Subalgebra.range_subset {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
        Set.range (algebraMap R A) S
        theorem Subalgebra.range_le {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
        Set.range (algebraMap R A) S
        theorem Subalgebra.smul_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x S) (r : R) :
        r x S
        theorem Subalgebra.one_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
        1 S
        theorem Subalgebra.mul_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x y : A} (hx : x S) (hy : y S) :
        x * y S
        theorem Subalgebra.pow_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x S) (n : ) :
        x ^ n S
        theorem Subalgebra.zero_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
        0 S
        theorem Subalgebra.add_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x y : A} (hx : x S) (hy : y S) :
        x + y S
        theorem Subalgebra.nsmul_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x S) (n : ) :
        n x S
        theorem Subalgebra.natCast_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (n : ) :
        n S
        theorem Subalgebra.list_prod_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {L : List A} (h : xL, x S) :
        L.prod S
        theorem Subalgebra.list_sum_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {L : List A} (h : xL, x S) :
        L.sum S
        theorem Subalgebra.multiset_sum_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {m : Multiset A} (h : xm, x S) :
        m.sum S
        theorem Subalgebra.sum_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ιA} (h : xt, f x S) :
        xt, f x S
        theorem Subalgebra.multiset_prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) {m : Multiset A} (h : xm, x S) :
        m.prod S
        theorem Subalgebra.prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ιA} (h : xt, f x S) :
        xt, f x S

        Turn a Subalgebra into a NonUnitalSubalgebra by forgetting that it contains 1.

        Equations
        Instances For
          instance Subalgebra.instSubringClass {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] :
          theorem Subalgebra.neg_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x S) :
          -x S
          theorem Subalgebra.sub_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) {x y : A} (hx : x S) (hy : y S) :
          x - y S
          theorem Subalgebra.zsmul_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x S) (n : ) :
          n x S
          theorem Subalgebra.intCast_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) (n : ) :
          n S

          The projection from a subalgebra of A to an additive submonoid of A.

          Equations
          Instances For
            @[simp]
            theorem Subalgebra.coe_toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
            def Subalgebra.toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :

            A subalgebra over a ring is also a Subring.

            Equations
            Instances For
              @[simp]
              theorem Subalgebra.mem_toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} {x : A} :
              @[simp]
              theorem Subalgebra.coe_toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
              S.toSubring = S
              theorem Subalgebra.toSubring_inj {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S U : Subalgebra R A} :
              instance Subalgebra.instInhabitedSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
              Equations

              Subalgebras inherit structure from their Subsemiring / Semiring coercions.

              instance Subalgebra.toSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
              Equations
              instance Subalgebra.toCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
              Equations
              instance Subalgebra.toRing {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
              Ring S
              Equations
              instance Subalgebra.toCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) :
              Equations

              The forgetful map from Subalgebra to Submodule as an OrderEmbedding

              Equations
              Instances For
                @[simp]
                theorem Subalgebra.mem_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} :
                @[simp]
                theorem Subalgebra.coe_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                (toSubmodule S) = S

                Subalgebras inherit structure from their Submodule coercions.

                @[instance 100]
                instance Subalgebra.module' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] :
                Module R' S
                Equations
                instance Subalgebra.instModuleSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                Module R S
                Equations
                instance Subalgebra.instIsScalarTowerSubtypeMem {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] :
                IsScalarTower R' R S
                @[instance 500]
                instance Subalgebra.algebra' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] :
                Algebra R' S
                Equations
                instance Subalgebra.algebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                Algebra R S
                Equations
                theorem Subalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x y : S) :
                ↑(x + y) = x + y
                theorem Subalgebra.coe_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x y : S) :
                ↑(x * y) = x * y
                theorem Subalgebra.coe_zero {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                0 = 0
                theorem Subalgebra.coe_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                1 = 1
                theorem Subalgebra.coe_neg {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (x : S) :
                ↑(-x) = -x
                theorem Subalgebra.coe_sub {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (x y : S) :
                ↑(x - y) = x - y
                @[simp]
                theorem Subalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [SMul R' R] [SMul R' A] [IsScalarTower R' R A] (r : R') (x : S) :
                ↑(r x) = r x
                @[simp]
                theorem Subalgebra.coe_algebraMap {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] (r : R') :
                ((algebraMap R' S) r) = (algebraMap R' A) r
                theorem Subalgebra.coe_pow {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : S) (n : ) :
                ↑(x ^ n) = x ^ n
                theorem Subalgebra.coe_eq_zero {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : S} :
                x = 0 x = 0
                theorem Subalgebra.coe_eq_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : S} :
                x = 1 x = 1
                def Subalgebra.val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                S →ₐ[R] A

                Embedding of a subalgebra into the algebra.

                Equations
                • S.val = { toFun := Subtype.val, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                Instances For
                  @[simp]
                  theorem Subalgebra.coe_val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                  theorem Subalgebra.val_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : S) :
                  S.val x = x
                  @[simp]
                  theorem Subalgebra.toSubsemiring_subtype {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                  S.subtype = S.val
                  @[simp]
                  theorem Subalgebra.toSubring_subtype {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
                  def Subalgebra.toSubmoduleEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                  (toSubmodule S) ≃ₗ[R] S

                  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
                    def Subalgebra.map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R A) :

                    Transport a subalgebra via an algebra homomorphism.

                    Equations
                    Instances For
                      @[simp]
                      theorem Subalgebra.coe_map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R A) :
                      (map f S) = f '' S
                      @[simp]
                      theorem Subalgebra.map_toSubsemiring {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R A) :
                      theorem Subalgebra.map_mono {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S₁ S₂ : Subalgebra R A} {f : A →ₐ[R] B} :
                      S₁ S₂map f S₁ map f S₂
                      theorem Subalgebra.map_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₐ[R] B} (hf : Function.Injective f) :
                      @[simp]
                      theorem Subalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                      map (AlgHom.id R A) S = S
                      theorem Subalgebra.map_map {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (S : Subalgebra R A) (g : B →ₐ[R] C) (f : A →ₐ[R] B) :
                      map g (map f S) = map (g.comp f) S
                      @[simp]
                      theorem Subalgebra.mem_map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} {y : B} :
                      y map f S xS, f x = y
                      theorem Subalgebra.map_toSubmodule {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} :
                      def Subalgebra.comap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) :

                      Preimage of a subalgebra under an algebra homomorphism.

                      Equations
                      Instances For
                        @[simp]
                        theorem Subalgebra.coe_comap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) :
                        (comap f S) = f ⁻¹' S
                        @[simp]
                        theorem Subalgebra.comap_toSubsemiring {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) :
                        theorem Subalgebra.map_le {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} {U : Subalgebra R B} :
                        map f S U S comap f U
                        theorem Subalgebra.gc_map_comap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :
                        @[simp]
                        theorem Subalgebra.mem_comap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R B) (f : A →ₐ[R] B) (x : A) :
                        x comap f S f x S
                        instance Subalgebra.noZeroDivisors {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [NoZeroDivisors A] [Algebra R A] (S : Subalgebra R A) :
                        instance Subalgebra.isDomain {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [IsDomain A] [Algebra R A] (S : Subalgebra R A) :
                        @[instance 75]
                        instance SubalgebraClass.toAlgebra {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) :
                        Algebra R s
                        Equations
                        • One or more equations did not get rendered due to their size.
                        @[simp]
                        theorem SubalgebraClass.coe_algebraMap {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) (r : R) :
                        ((algebraMap R s) r) = (algebraMap R A) r
                        def SubalgebraClass.val {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) :
                        s →ₐ[R] A

                        Embedding of a subalgebra into the algebra, as an algebra homomorphism.

                        Equations
                        Instances For
                          @[simp]
                          theorem SubalgebraClass.coe_val {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) :
                          def Submodule.toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 p) (h_mul : ∀ (x y : A), x py px * y p) :

                          A submodule containing 1 and closed under multiplication is a subalgebra.

                          Equations
                          • p.toSubalgebra h_one h_mul = { carrier := p.carrier, mul_mem' := , one_mem' := h_one, add_mem' := , zero_mem' := , algebraMap_mem' := }
                          Instances For
                            @[simp]
                            theorem Submodule.coe_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 p) (h_mul : ∀ (x y : A), x py px * y p) :
                            (p.toSubalgebra h_one h_mul) = p.carrier
                            @[simp]
                            theorem Submodule.toSubalgebra_toSubsemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 p) (h_mul : ∀ (x y : A), x py px * y p) :
                            (p.toSubalgebra h_one h_mul).toSubsemiring = { carrier := p.carrier, mul_mem' := , one_mem' := h_one, add_mem' := , zero_mem' := }
                            @[simp]
                            theorem Submodule.mem_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {p : Submodule R A} {h_one : 1 p} {h_mul : ∀ (x y : A), x py px * y p} {x : A} :
                            x p.toSubalgebra h_one h_mul x p
                            theorem Submodule.toSubalgebra_mk {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (s : Submodule R A) (h1 : 1 s) (hmul : ∀ (x y : A), x sy sx * y s) :
                            s.toSubalgebra h1 hmul = { carrier := s, mul_mem' := hmul, one_mem' := h1, add_mem' := , zero_mem' := , algebraMap_mem' := }
                            @[simp]
                            theorem Submodule.toSubalgebra_toSubmodule {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 p) (h_mul : ∀ (x y : A), x py px * y p) :
                            @[simp]
                            theorem Subalgebra.toSubmodule_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                            (toSubmodule S).toSubalgebra = S
                            def AlgHom.range {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) :

                            Range of an AlgHom as a subalgebra.

                            Equations
                            Instances For
                              @[simp]
                              theorem AlgHom.range_toSubsemiring {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) :
                              @[simp]
                              theorem AlgHom.coe_range {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) :
                              φ.range = Set.range φ
                              @[simp]
                              theorem AlgHom.mem_range {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) {y : B} :
                              y φ.range ∃ (x : A), φ x = y
                              theorem AlgHom.mem_range_self {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) (x : A) :
                              φ x φ.range
                              theorem AlgHom.range_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
                              theorem AlgHom.range_comp_le_range {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
                              def AlgHom.codRestrict {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ (x : A), f x S) :
                              A →ₐ[R] S

                              Restrict the codomain of an algebra homomorphism.

                              Equations
                              Instances For
                                @[simp]
                                theorem AlgHom.val_comp_codRestrict {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ (x : A), f x S) :
                                S.val.comp (f.codRestrict S hf) = f
                                @[simp]
                                theorem AlgHom.coe_codRestrict {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ (x : A), f x S) (x : A) :
                                ((f.codRestrict S hf) x) = f x
                                theorem AlgHom.injective_codRestrict {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ (x : A), f x S) :
                                @[reducible, inline]
                                abbrev AlgHom.rangeRestrict {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :
                                A →ₐ[R] f.range

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

                                This is the bundled version of Set.rangeFactorization.

                                Equations
                                Instances For
                                  instance AlgHom.fintypeRange {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Fintype A] [DecidableEq B] (φ : A →ₐ[R] B) :

                                  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
                                  def AlgEquiv.ofLeftInverse {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {g : BA} {f : A →ₐ[R] B} (h : Function.LeftInverse g f) :
                                  A ≃ₐ[R] f.range

                                  Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.

                                  This is a computable alternative to AlgEquiv.ofInjective.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem AlgEquiv.ofLeftInverse_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {g : BA} {f : A →ₐ[R] B} (h : Function.LeftInverse g f) (x : A) :
                                    ((ofLeftInverse h) x) = f x
                                    @[simp]
                                    theorem AlgEquiv.ofLeftInverse_symm_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {g : BA} {f : A →ₐ[R] B} (h : Function.LeftInverse g f) (x : f.range) :
                                    (ofLeftInverse h).symm x = g x
                                    noncomputable def AlgEquiv.ofInjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective f) :
                                    A ≃ₐ[R] f.range

                                    Restrict an injective algebra homomorphism to an algebra isomorphism

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem AlgEquiv.ofInjective_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective f) (x : A) :
                                      ((ofInjective f hf) x) = f x
                                      noncomputable def AlgEquiv.ofInjectiveField {R : Type u} [CommSemiring R] {E : Type u_1} {F : Type u_2} [DivisionRing E] [Semiring F] [Nontrivial F] [Algebra R E] [Algebra R F] (f : E →ₐ[R] F) :
                                      E ≃ₐ[R] f.range

                                      Restrict an algebra homomorphism between fields to an algebra isomorphism

                                      Equations
                                      Instances For
                                        def AlgEquiv.subalgebraMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) :
                                        S ≃ₐ[R] (Subalgebra.map (↑e) S)

                                        Given an equivalence e : A ≃ₐ[R] B of R-algebras and a subalgebra S of A, subalgebraMap is the induced equivalence between S and S.map e

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem AlgEquiv.subalgebraMap_apply_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (x : S.toAddSubmonoid) :
                                          ((e.subalgebraMap S) x) = e x
                                          @[simp]
                                          theorem AlgEquiv.subalgebraMap_symm_apply_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (y : ↑(e.toRingEquiv.toAddEquiv '' S.toAddSubmonoid)) :
                                          ((e.subalgebraMap S).symm y) = (↑e).symm y
                                          theorem Subalgebra.range_val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                                          S.val.range = S
                                          def Subalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) :
                                          S →ₐ[R] T

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

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

                                          Equations
                                          Instances For
                                            theorem Subalgebra.inclusion_injective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) :
                                            @[simp]
                                            theorem Subalgebra.inclusion_self {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :
                                            inclusion = AlgHom.id R S
                                            @[simp]
                                            theorem Subalgebra.inclusion_mk {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) (x : A) (hx : x S) :
                                            (inclusion h) x, hx = x,
                                            theorem Subalgebra.inclusion_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) (x : T) (m : x S) :
                                            (inclusion h) x, m = x
                                            @[simp]
                                            theorem Subalgebra.inclusion_inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T U : Subalgebra R A} (hst : S T) (htu : T U) (x : S) :
                                            (inclusion htu) ((inclusion hst) x) = (inclusion ) x
                                            @[simp]
                                            theorem Subalgebra.coe_inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) (s : S) :
                                            ((inclusion h) s) = s
                                            theorem Subalgebra.inclusion.isScalarTower_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) (X : Type u_1) [SMul X R] [SMul X A] [IsScalarTower X R A] :
                                            IsScalarTower X S T
                                            theorem Subalgebra.inclusion.isScalarTower_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) (X : Type u_1) [MulAction A X] :
                                            IsScalarTower (↥S) (↥T) X
                                            theorem Subalgebra.inclusion.faithfulSMul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S T) :
                                            FaithfulSMul S T
                                            def Subalgebra.equivOfEq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) (h : S = T) :
                                            S ≃ₐ[R] T

                                            Two subalgebras that are equal are also equivalent as algebras.

                                            This is the Subalgebra version of LinearEquiv.ofEq and Equiv.setCongr.

                                            Equations
                                            • S.equivOfEq T h = { toFun := fun (x : S) => x, , invFun := fun (x : T) => x, , left_inv := , right_inv := , map_mul' := , map_add' := , commutes' := }
                                            Instances For
                                              @[simp]
                                              theorem Subalgebra.equivOfEq_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) (h : S = T) (x : S) :
                                              (S.equivOfEq T h) x = x,
                                              @[simp]
                                              theorem Subalgebra.equivOfEq_symm {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) (h : S = T) :
                                              (S.equivOfEq T h).symm = T.equivOfEq S
                                              @[simp]
                                              theorem Subalgebra.equivOfEq_rfl {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                                              @[simp]
                                              theorem Subalgebra.equivOfEq_trans {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T U : Subalgebra R A) (hST : S = T) (hTU : T = U) :
                                              (S.equivOfEq T hST).trans (T.equivOfEq U hTU) = S.equivOfEq U
                                              theorem Subalgebra.range_comp_val {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) :
                                              (f.comp S.val).range = map f S
                                              def AlgHom.subalgebraMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) :
                                              S →ₐ[R] (Subalgebra.map f S)

                                              An AlgHom between two rings restricts to an AlgHom from any subalgebra of the domain onto the image of that subalgebra.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem AlgHom.subalgebraMap_coe_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} (f : A →ₐ[R] B) (x : S) :
                                                ((subalgebraMap S f) x) = f x
                                                theorem AlgHom.subalgebraMap_surjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) :
                                                noncomputable def Subalgebra.equivMapOfInjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective f) :
                                                S ≃ₐ[R] (map f S)

                                                A subalgebra is isomorphic to its image under an injective AlgHom

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Subalgebra.coe_equivMapOfInjective_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective f) (x : S) :
                                                  ((S.equivMapOfInjective f hf) x) = f x

                                                  Actions by Subalgebras #

                                                  These are just copies of the definitions about Subsemiring starting from Subring.mulAction.

                                                  instance Subalgebra.instSMulSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [SMul A α] (S : Subalgebra R A) :
                                                  SMul (↥S) α

                                                  The action by a subalgebra is the action by the underlying algebra.

                                                  Equations
                                                  theorem Subalgebra.smul_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [SMul A α] {S : Subalgebra R A} (g : S) (m : α) :
                                                  g m = g m
                                                  instance Subalgebra.smulCommClass_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} {β : Type u_2} [SMul A β] [SMul α β] [SMulCommClass A α β] (S : Subalgebra R A) :
                                                  SMulCommClass (↥S) α β
                                                  instance Subalgebra.smulCommClass_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} {β : Type u_2} [SMul α β] [SMul A β] [SMulCommClass α A β] (S : Subalgebra R A) :
                                                  SMulCommClass α (↥S) β
                                                  instance Subalgebra.isScalarTower_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} {β : Type u_2} [SMul α β] [SMul A α] [SMul A β] [IsScalarTower A α β] (S : Subalgebra R A) :
                                                  IsScalarTower (↥S) α β

                                                  Note that this provides IsScalarTower S R R which is needed by smul_mul_assoc.

                                                  instance Subalgebra.isScalarTower_mid {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [Semiring S] [AddCommMonoid T] [Algebra R S] [Module R T] [Module S T] [IsScalarTower R S T] (S' : Subalgebra R S) :
                                                  IsScalarTower R (↥S') T
                                                  instance Subalgebra.instFaithfulSMulSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [SMul A α] [FaithfulSMul A α] (S : Subalgebra R A) :
                                                  FaithfulSMul (↥S) α
                                                  instance Subalgebra.instMulActionSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [MulAction A α] (S : Subalgebra R A) :
                                                  MulAction (↥S) α

                                                  The action by a subalgebra is the action by the underlying algebra.

                                                  Equations
                                                  instance Subalgebra.instDistribMulActionSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [AddMonoid α] [DistribMulAction A α] (S : Subalgebra R A) :

                                                  The action by a subalgebra is the action by the underlying algebra.

                                                  Equations
                                                  instance Subalgebra.instSMulWithZeroSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [Zero α] [SMulWithZero A α] (S : Subalgebra R A) :
                                                  SMulWithZero (↥S) α

                                                  The action by a subalgebra is the action by the underlying algebra.

                                                  Equations
                                                  instance Subalgebra.instMulActionWithZeroSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [Zero α] [MulActionWithZero A α] (S : Subalgebra R A) :

                                                  The action by a subalgebra is the action by the underlying algebra.

                                                  Equations
                                                  instance Subalgebra.moduleLeft {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [AddCommMonoid α] [Module A α] (S : Subalgebra R A) :
                                                  Module (↥S) α

                                                  The action by a subalgebra is the action by the underlying algebra.

                                                  Equations
                                                  instance Subalgebra.toAlgebra {α : Type u_1} {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α] (S : Subalgebra R A) :
                                                  Algebra (↥S) α

                                                  The action by a subalgebra is the action by the underlying algebra.

                                                  Equations
                                                  theorem Subalgebra.algebraMap_eq {α : Type u_1} {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α] (S : Subalgebra R A) :
                                                  algebraMap (↥S) α = (algebraMap A α).comp S.val
                                                  @[simp]
                                                  theorem Subalgebra.rangeS_algebraMap {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
                                                  @[simp]
                                                  theorem Subalgebra.range_algebraMap {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) :
                                                  theorem Set.algebraMap_mem_center {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
                                                  def Subalgebra.center (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

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

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    @[simp]
                                                    theorem Subalgebra.center_toSubring (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Algebra R A] :
                                                    theorem Subalgebra.mem_center_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} :
                                                    a center R A ∀ (b : A), b * a = a * b
                                                    @[simp]
                                                    theorem Set.algebraMap_mem_centralizer {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} (r : R) :
                                                    def Subalgebra.centralizer (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

                                                    The centralizer of a set as a subalgebra.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Subalgebra.coe_centralizer (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :
                                                      theorem Subalgebra.mem_centralizer_iff (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {z : A} :
                                                      z centralizer R s gs, g * z = z * g
                                                      theorem Subalgebra.center_le_centralizer (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :
                                                      theorem Subalgebra.centralizer_le (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s t : Set A) (h : s t) :

                                                      A subsemiring is an -subalgebra.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        def subalgebraOfSubring {R : Type u_1} [Ring R] (S : Subring R) :

                                                        A subring is a -subalgebra.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem mem_subalgebraOfSubring {R : Type u_1} [Ring R] {x : R} {S : Subring R} :
                                                          def AlgHom.equalizer {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} (ϕ ψ : F) [FunLike F A B] [AlgHomClass F R A B] :

                                                          The equalizer of two R-algebra homomorphisms

                                                          Equations
                                                          • AlgHom.equalizer ϕ ψ = { carrier := {a : A | ϕ a = ψ a}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
                                                          Instances For
                                                            @[simp]
                                                            theorem AlgHom.coe_equalizer {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} (ϕ ψ : F) [FunLike F A B] [AlgHomClass F R A B] :
                                                            (equalizer ϕ ψ) = {a : A | ϕ a = ψ a}
                                                            @[simp]
                                                            theorem AlgHom.equalizer_toSubsemiring {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} (ϕ ψ : F) [FunLike F A B] [AlgHomClass F R A B] :
                                                            (equalizer ϕ ψ).toSubsemiring = { carrier := {a : A | ϕ a = ψ a}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := }
                                                            @[simp]
                                                            theorem AlgHom.mem_equalizer {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] (φ ψ : F) (x : A) :
                                                            x equalizer φ ψ φ x = ψ x
                                                            theorem AlgHom.equalizer_toSubmodule {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] {φ ψ : F} :
                                                            theorem AlgHom.le_equalizer {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] {φ ψ : F} {S : Subalgebra R A} :
                                                            S equalizer φ ψ Set.EqOn φ ψ S
                                                            theorem Subalgebra.comap_map_eq_self_of_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₐ[R] B} (hf : Function.Injective f) (S : Subalgebra R A) :
                                                            comap f (map f S) = S
                                                            def NonUnitalSubalgebra.toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : NonUnitalSubalgebra R A) (h1 : 1 S) :

                                                            Turn a non-unital subalgebra containing 1 into a subalgebra.

                                                            Equations
                                                            • S.toSubalgebra h1 = { carrier := S.carrier, mul_mem' := , one_mem' := h1, add_mem' := , zero_mem' := , algebraMap_mem' := }
                                                            Instances For