Documentation

Mathlib.Algebra.Algebra.Subalgebra.Basic

Subalgebras over Commutative Semiring #

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

More lemmas about adjoin can be found in RingTheory.Adjoin.

structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] extends Subsemiring :
  • carrier : Set A
  • mul_mem' : ∀ {a b : A}, a s.carrierb s.carriera * b s.carrier
  • one_mem' : 1 s.carrier
  • add_mem' : ∀ {a b : A}, a s.carrierb s.carriera + b s.carrier
  • zero_mem' : 0 s.carrier
  • algebraMap_mem' : ∀ (r : R), ↑(algebraMap R A) r s.carrier

    The image of algebraMap is contained in the underlying set of the subalgebra

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

Instances For
    @[simp]
    theorem Subalgebra.mem_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {x : A} :
    x S.toSubsemiring x S
    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 : Subalgebra R A} {T : Subalgebra R A} (h : ∀ (x : A), x S x T) :
    S = 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
    theorem Subalgebra.toSubsemiring_injective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
    Function.Injective Subalgebra.toSubsemiring
    theorem Subalgebra.toSubsemiring_inj {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {U : Subalgebra R A} :
    S.toSubsemiring = U.toSubsemiring S = U
    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.

    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) :
      ↑(Subalgebra.copy S s hs) = s
      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) :
      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.rangeS_le {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
      RingHom.rangeS (algebraMap R A) S.toSubsemiring
      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 : A} {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 : A} {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.coe_nat_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 : ∀ (x : A), x Lx 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 : ∀ (x : A), x Lx 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 : ∀ (x : A), x mx 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 : ∀ (x : ι), x tf x S) :
      (Finset.sum t fun x => 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 : ∀ (x : A), x mx 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 : ∀ (x : ι), x tf x S) :
      (Finset.prod t fun x => f x) S
      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 : A} {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.coe_int_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.

      Instances For
        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.

        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) :
          theorem Subalgebra.toSubring_injective {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] :
          Function.Injective Subalgebra.toSubring

          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) :
          Semiring { x // x S }
          instance Subalgebra.toCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
          CommSemiring { x // x S }
          instance Subalgebra.toRing {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
          Ring { x // x S }
          instance Subalgebra.toCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) :
          CommRing { x // x S }
          instance Subalgebra.toOrderedSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [OrderedSemiring A] [Algebra R A] (S : Subalgebra R A) :
          OrderedSemiring { x // x S }
          instance Subalgebra.toOrderedRing {R : Type u_1} {A : Type u_2} [CommRing R] [OrderedRing A] [Algebra R A] (S : Subalgebra R A) :
          OrderedRing { x // x S }
          instance Subalgebra.toOrderedCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [OrderedCommRing A] [Algebra R A] (S : Subalgebra R A) :
          OrderedCommRing { x // x S }
          instance Subalgebra.toLinearOrderedRing {R : Type u_1} {A : Type u_2} [CommRing R] [LinearOrderedRing A] [Algebra R A] (S : Subalgebra R A) :
          LinearOrderedRing { x // x S }

          The forgetful map from Subalgebra to Submodule as an OrderEmbedding

          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} :
            x Subalgebra.toSubmodule S x S
            @[simp]
            theorem Subalgebra.coe_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
            ↑(Subalgebra.toSubmodule S) = S

            Subalgebras inherit structure from their Submodule coercions.

            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' { x // x S }
            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' { x // x S }
            instance Subalgebra.algebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
            Algebra R { x // x S }
            theorem Subalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : { x // x S }) (y : { x // x 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 : { x // x S }) (y : { x // x 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 : { x // 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 : { x // x S }) (y : { x // x 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) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : { x // 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' { x // x 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 : { x // 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 : { x // 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 : { x // 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) :
            { x // x S } →ₐ[R] A

            Embedding of a subalgebra into the algebra.

            Instances For
              @[simp]
              theorem Subalgebra.coe_val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
              ↑(Subalgebra.val S) = Subtype.val
              theorem Subalgebra.val_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : { x // x S }) :
              ↑(Subalgebra.val S) x = x
              @[simp]
              theorem Subalgebra.toSubsemiring_subtype {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
              Subsemiring.subtype S.toSubsemiring = ↑(Subalgebra.val S)
              @[simp]
              def Subalgebra.toSubmoduleEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
              { x // x Subalgebra.toSubmodule S } ≃ₗ[R] { x // x 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.

              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.

                Instances For
                  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₁ : Subalgebra R A} {S₂ : Subalgebra R A} {f : A →ₐ[R] B} :
                  S₁ S₂Subalgebra.map f S₁ Subalgebra.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) :
                  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) :
                  @[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 Subalgebra.map f S x, x S 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} :
                  Subalgebra.toSubmodule (Subalgebra.map f S) = Submodule.map (AlgHom.toLinearMap f) (Subalgebra.toSubmodule S)
                  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] {S : Subalgebra R A} {f : A →ₐ[R] B} :
                  (Subalgebra.map f S).toSubsemiring = Subsemiring.map (f) S.toSubsemiring
                  @[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] (S : Subalgebra R A) (f : A →ₐ[R] B) :
                  ↑(Subalgebra.map f S) = f '' S
                  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.

                  Instances For
                    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} :
                    @[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 Subalgebra.comap f S f x S
                    @[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] (S : Subalgebra R B) (f : A →ₐ[R] B) :
                    ↑(Subalgebra.comap f S) = f ⁻¹' 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) :
                    NoZeroDivisors { x // x S }
                    instance Subalgebra.isDomain {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [IsDomain A] [Algebra R A] (S : Subalgebra R A) :
                    IsDomain { x // x 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.

                    Instances For
                      @[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 Submodule.toSubalgebra p h_one h_mul x p
                      @[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) :
                      ↑(Submodule.toSubalgebra p h_one h_mul) = 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) :
                      Submodule.toSubalgebra s h1 hmul = { toSubsemiring := { toSubmonoid := { toSubsemigroup := { carrier := s, mul_mem' := hmul }, one_mem' := h1 }, add_mem' := (_ : ∀ {a b : A}, a sb sa + b s), zero_mem' := (_ : 0 s) }, algebraMap_mem' := (_ : ∀ (r : R), ↑(algebraMap R A) r { toSubmonoid := { toSubsemigroup := { carrier := s, mul_mem' := hmul }, one_mem' := h1 }, add_mem' := (_ : ∀ {a b : A}, a sb sa + b s), zero_mem' := (_ : 0 s) }.toSubmonoid.toSubsemigroup.carrier) }
                      @[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) :
                      Subalgebra.toSubmodule (Submodule.toSubalgebra p h_one h_mul) = 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) :
                      Submodule.toSubalgebra (Subalgebra.toSubmodule S) (_ : 1 S) (_ : ∀ (x x_1 : A), x Sx_1 Sx * x_1 S) = 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.

                      Instances For
                        @[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 AlgHom.range φ x, φ 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 AlgHom.range φ
                        @[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) :
                        ↑(AlgHom.range φ) = Set.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] { x // x S }

                        Restrict the codomain of an algebra homomorphism.

                        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) :
                          @[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) :
                          ↑(↑(AlgHom.codRestrict f 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]
                          def 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] { x // x AlgHom.range f }

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

                          This is the bundled version of Set.rangeFactorization.

                          Instances For
                            def AlgHom.equalizer {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (ϕ : A →ₐ[R] B) (ψ : A →ₐ[R] B) :

                            The equalizer of two R-algebra homomorphisms

                            Instances For
                              @[simp]
                              theorem AlgHom.mem_equalizer {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (ϕ : A →ₐ[R] B) (ψ : A →ₐ[R] B) (x : A) :
                              x AlgHom.equalizer ϕ ψ ϕ x = ψ x
                              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) :
                              Fintype { x // x AlgHom.range φ }

                              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.

                              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] { x // x AlgHom.range f }

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

                              This is a computable alternative to AlgEquiv.ofInjective.

                              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) :
                                ↑(↑(AlgEquiv.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 : { x // x AlgHom.range f }) :
                                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] { x // x AlgHom.range f }

                                Restrict an injective algebra homomorphism to an algebra isomorphism

                                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) :
                                  ↑(↑(AlgEquiv.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] { x // x AlgHom.range f }

                                  Restrict an algebra homomorphism between fields to an algebra isomorphism

                                  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) :
                                    ∀ (a : ↑(Subsemiring.toAddSubmonoid S.toSubsemiring)), ↑(↑(AlgEquiv.subalgebraMap e S) a) = e a
                                    @[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) :
                                    ∀ (a : ↑(↑(RingEquiv.toAddEquiv (AlgEquiv.toRingEquiv e)) '' ↑(Subsemiring.toAddSubmonoid S.toSubsemiring))), ↑(↑(AlgEquiv.symm (AlgEquiv.subalgebraMap e S)) a) = ↑(AddEquiv.symm e) a
                                    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) :
                                    { x // x S } ≃ₐ[R] { x // x Subalgebra.map (e) S }

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

                                    Instances For
                                      def Algebra.adjoin (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

                                      The minimal subalgebra that includes s.

                                      Instances For
                                        theorem Algebra.gc {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                        def Algebra.gi {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

                                        Galois insertion between adjoin and coe.

                                        Instances For
                                          @[simp]
                                          theorem Algebra.coe_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                          = Set.univ
                                          @[simp]
                                          theorem Algebra.mem_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} :
                                          @[simp]
                                          theorem Algebra.top_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                          Subalgebra.toSubmodule =
                                          @[simp]
                                          theorem Algebra.top_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                          .toSubsemiring =
                                          @[simp]
                                          theorem Algebra.top_toSubring {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] :
                                          @[simp]
                                          theorem Algebra.toSubmodule_eq_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :
                                          Subalgebra.toSubmodule S = S =
                                          @[simp]
                                          theorem Algebra.toSubsemiring_eq_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :
                                          S.toSubsemiring = S =
                                          @[simp]
                                          theorem Algebra.toSubring_eq_top {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} :
                                          theorem Algebra.mem_sup_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} {x : A} :
                                          x Sx S T
                                          theorem Algebra.mem_sup_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} {x : A} :
                                          x Tx S T
                                          theorem Algebra.mul_mem_sup {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} {x : A} {y : A} (hx : x S) (hy : y T) :
                                          x * y S T
                                          theorem Algebra.map_sup {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) (T : Subalgebra R A) :
                                          @[simp]
                                          theorem Algebra.coe_inf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) :
                                          ↑(S T) = S T
                                          @[simp]
                                          theorem Algebra.mem_inf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} {x : A} :
                                          x S T x S x T
                                          @[simp]
                                          theorem Algebra.inf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) :
                                          Subalgebra.toSubmodule (S T) = Subalgebra.toSubmodule S Subalgebra.toSubmodule T
                                          @[simp]
                                          theorem Algebra.inf_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) :
                                          (S T).toSubsemiring = S.toSubsemiring T.toSubsemiring
                                          @[simp]
                                          theorem Algebra.coe_sInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :
                                          ↑(sInf S) = ⋂ (s : Subalgebra R A) (_ : s S), s
                                          theorem Algebra.mem_sInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Set (Subalgebra R A)} {x : A} :
                                          x sInf S ∀ (p : Subalgebra R A), p Sx p
                                          @[simp]
                                          theorem Algebra.sInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :
                                          Subalgebra.toSubmodule (sInf S) = sInf (Subalgebra.toSubmodule '' S)
                                          @[simp]
                                          theorem Algebra.sInf_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :
                                          (sInf S).toSubsemiring = sInf (Subalgebra.toSubsemiring '' S)
                                          @[simp]
                                          theorem Algebra.coe_iInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} {S : ιSubalgebra R A} :
                                          ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
                                          theorem Algebra.mem_iInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} {S : ιSubalgebra R A} {x : A} :
                                          x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                          @[simp]
                                          theorem Algebra.iInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} (S : ιSubalgebra R A) :
                                          Subalgebra.toSubmodule (⨅ (i : ι), S i) = ⨅ (i : ι), Subalgebra.toSubmodule (S i)
                                          theorem Algebra.mem_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} :
                                          theorem Algebra.toSubmodule_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                          Subalgebra.toSubmodule = Submodule.span R {1}
                                          @[simp]
                                          theorem Algebra.coe_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                          theorem Algebra.eq_top_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :
                                          S = ∀ (x : A), x S
                                          @[simp]
                                          theorem Algebra.range_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                          @[simp]
                                          theorem Algebra.map_top {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 Algebra.map_bot {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 Algebra.comap_top {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) :
                                          def Algebra.toTop {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                          A →ₐ[R] { x // x }

                                          AlgHom to ⊤ : Subalgebra R A.

                                          Instances For
                                            noncomputable def Algebra.botEquivOfInjective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective ↑(algebraMap R A)) :
                                            { x // x } ≃ₐ[R] R

                                            The bottom subalgebra is isomorphic to the base ring.

                                            Instances For
                                              @[simp]
                                              theorem Algebra.botEquiv_symm_apply (F : Type u_1) (R : Type u_2) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :
                                              ∀ (a : F), ↑(AlgEquiv.symm (Algebra.botEquiv F R)) a = ↑(Algebra.ofId F { x // x }) a
                                              noncomputable def Algebra.botEquiv (F : Type u_1) (R : Type u_2) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :
                                              { x // x } ≃ₐ[F] F

                                              The bottom subalgebra is isomorphic to the field.

                                              Instances For
                                                @[simp]
                                                theorem Subalgebra.topEquiv_symm_apply_coe {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :
                                                ↑(↑(AlgEquiv.symm Subalgebra.topEquiv) a) = a
                                                @[simp]
                                                theorem Subalgebra.topEquiv_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : { x // x }) :
                                                Subalgebra.topEquiv a = a
                                                def Subalgebra.topEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                                { x // x } ≃ₐ[R] A

                                                The top subalgebra is isomorphic to the algebra.

                                                This is the algebra version of Submodule.topEquiv.

                                                Instances For
                                                  instance AlgHom.subsingleton {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Subsingleton (Subalgebra R A)] :
                                                  def Subalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S T) :
                                                  { x // x S } →ₐ[R] { x // x T }

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

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

                                                  Instances For
                                                    @[simp]
                                                    theorem Subalgebra.inclusion_self {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :
                                                    Subalgebra.inclusion (_ : S S) = AlgHom.id R { x // x S }
                                                    @[simp]
                                                    theorem Subalgebra.inclusion_mk {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S T) (x : A) (hx : x S) :
                                                    ↑(Subalgebra.inclusion h) { val := x, property := hx } = { val := x, property := h x hx }
                                                    theorem Subalgebra.inclusion_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S T) (x : { x // x T }) (m : x S) :
                                                    ↑(Subalgebra.inclusion h) { val := x, property := m } = x
                                                    @[simp]
                                                    theorem Subalgebra.inclusion_inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} {U : Subalgebra R A} (hst : S T) (htu : T U) (x : { x // x S }) :
                                                    ↑(Subalgebra.inclusion htu) (↑(Subalgebra.inclusion hst) x) = ↑(Subalgebra.inclusion (_ : S U)) x
                                                    @[simp]
                                                    theorem Subalgebra.coe_inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S T) (s : { x // x S }) :
                                                    ↑(↑(Subalgebra.inclusion h) s) = s
                                                    @[simp]
                                                    theorem Subalgebra.equivOfEq_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (h : S = T) (x : { x // x S }) :
                                                    ↑(Subalgebra.equivOfEq S T h) x = { val := x, property := (_ : x T) }
                                                    def Subalgebra.equivOfEq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (h : S = T) :
                                                    { x // x S } ≃ₐ[R] { x // x T }

                                                    Two subalgebras that are equal are also equivalent as algebras.

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

                                                    Instances For
                                                      @[simp]
                                                      theorem Subalgebra.equivOfEq_symm {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (h : S = T) :
                                                      @[simp]
                                                      theorem Subalgebra.equivOfEq_rfl {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
                                                      Subalgebra.equivOfEq S S (_ : S = S) = AlgEquiv.refl
                                                      @[simp]
                                                      theorem Subalgebra.equivOfEq_trans {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (U : Subalgebra R A) (hST : S = T) (hTU : T = U) :
                                                      def Subalgebra.prod {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) (S₁ : Subalgebra R B) :
                                                      Subalgebra R (A × B)

                                                      The product of two subalgebras is a subalgebra.

                                                      Instances For
                                                        @[simp]
                                                        theorem Subalgebra.coe_prod {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) (S₁ : Subalgebra R B) :
                                                        ↑(Subalgebra.prod S S₁) = S ×ˢ S₁
                                                        theorem Subalgebra.prod_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) (S₁ : Subalgebra R B) :
                                                        Subalgebra.toSubmodule (Subalgebra.prod S S₁) = Submodule.prod (Subalgebra.toSubmodule S) (Subalgebra.toSubmodule S₁)
                                                        @[simp]
                                                        theorem Subalgebra.mem_prod {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} {S₁ : Subalgebra R B} {x : A × B} :
                                                        x Subalgebra.prod S S₁ x.fst S x.snd S₁
                                                        @[simp]
                                                        theorem Subalgebra.prod_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] :
                                                        theorem Subalgebra.prod_mono {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} {T : Subalgebra R A} {S₁ : Subalgebra R B} {T₁ : Subalgebra R B} :
                                                        S TS₁ T₁Subalgebra.prod S S₁ Subalgebra.prod T T₁
                                                        @[simp]
                                                        theorem Subalgebra.prod_inf_prod {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} {T : Subalgebra R A} {S₁ : Subalgebra R B} {T₁ : Subalgebra R B} :
                                                        Subalgebra.prod S S₁ Subalgebra.prod T T₁ = Subalgebra.prod (S T) (S₁ T₁)
                                                        theorem Subalgebra.coe_iSup_of_directed {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Type u_1} [Nonempty ι] {S : ιSubalgebra R A} (dir : Directed (fun x x_1 => x x_1) S) :
                                                        ↑(iSup S) = ⋃ (i : ι), ↑(S i)
                                                        noncomputable def Subalgebra.iSupLift {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_1} [Nonempty ι] (K : ιSubalgebra R A) (dir : Directed (fun x x_1 => x x_1) K) (f : (i : ι) → { x // x K i } →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i K j), f i = AlgHom.comp (f j) (Subalgebra.inclusion h)) (T : Subalgebra R A) (hT : T = iSup K) :
                                                        { x // x T } →ₐ[R] B

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

                                                        Instances For
                                                          @[simp]
                                                          theorem Subalgebra.iSupLift_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_1} [Nonempty ι] {K : ιSubalgebra R A} {dir : Directed (fun x x_1 => x x_1) K} {f : (i : ι) → { x // x K i } →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = AlgHom.comp (f j) (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : { x // x K i }) (h : K i T) :
                                                          ↑(Subalgebra.iSupLift K dir f hf T hT) (↑(Subalgebra.inclusion h) x) = ↑(f i) x
                                                          @[simp]
                                                          theorem Subalgebra.iSupLift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_1} [Nonempty ι] {K : ιSubalgebra R A} {dir : Directed (fun x x_1 => x x_1) K} {f : (i : ι) → { x // x K i } →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = AlgHom.comp (f j) (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (h : K i T) :
                                                          @[simp]
                                                          theorem Subalgebra.iSupLift_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_1} [Nonempty ι] {K : ιSubalgebra R A} {dir : Directed (fun x x_1 => x x_1) K} {f : (i : ι) → { x // x K i } →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = AlgHom.comp (f j) (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : { x // x K i }) (hx : x T) :
                                                          ↑(Subalgebra.iSupLift K dir f hf T hT) { val := x, property := hx } = ↑(f i) x
                                                          theorem Subalgebra.iSupLift_of_mem {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_1} [Nonempty ι] {K : ιSubalgebra R A} {dir : Directed (fun x x_1 => x x_1) K} {f : (i : ι) → { x // x K i } →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i K j), f i = AlgHom.comp (f j) (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : { x // x T }) (hx : x K i) :
                                                          ↑(Subalgebra.iSupLift K dir f hf T hT) x = ↑(f i) { val := x, property := hx }

                                                          Actions by Subalgebras #

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

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

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

                                                          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 : { x // x 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 { x // x 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 α { x // x 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 { x // x 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 { x // x S' } T

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

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

                                                          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 { x // x S } α

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

                                                          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 { x // x S } α

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

                                                          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 { x // x S } α = RingHom.comp (algebraMap A α) ↑(Subalgebra.val S)
                                                          @[simp]
                                                          theorem Subalgebra.rangeS_algebraMap {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
                                                          RingHom.rangeS (algebraMap { x // x S } A) = S.toSubsemiring
                                                          @[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.

                                                          Instances For
                                                            @[simp]
                                                            theorem Subalgebra.center_toSubsemiring (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :
                                                            (Subalgebra.center R A).toSubsemiring = Subsemiring.center A
                                                            @[simp]
                                                            theorem Subalgebra.mem_center_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} :
                                                            a Subalgebra.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.

                                                            Instances For
                                                              @[simp]
                                                              theorem Subalgebra.mem_centralizer_iff (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {z : A} :
                                                              z Subalgebra.centralizer R s ∀ (g : A), g sg * z = z * g
                                                              theorem Subalgebra.centralizer_le (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) (t : Set A) (h : s t) :
                                                              theorem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem {R : Type u} [CommSemiring R] {S : Type u_1} [CommRing S] [Algebra R S] (S' : Subalgebra R S) {ι : Type u_2} (ι' : Finset ι) (s : ιS) (l : ιS) (e : (Finset.sum ι' fun i => l i * s i) = 1) (hs : ∀ (i : ι), s i S') (hl : ∀ (i : ι), l i S') (x : S) (H : ∀ (i : ι), n, s i ^ n x S') :
                                                              x S'

                                                              Suppose we are given ∑ i, lᵢ * sᵢ = 1 in S, and S' a subalgebra of S that contains lᵢ and sᵢ. To check that an x : S falls in S', we only need to show that sᵢ ^ n • x ∈ S' for some n for each sᵢ.

                                                              theorem Subalgebra.mem_of_span_eq_top_of_smul_pow_mem {R : Type u} [CommSemiring R] {S : Type u_1} [CommRing S] [Algebra R S] (S' : Subalgebra R S) (s : Set S) (l : s →₀ S) (hs : ↑(Finsupp.total (s) S S Subtype.val) l = 1) (hs' : s S') (hl : ∀ (i : s), l i S') (x : S) (H : ∀ (r : s), n, r ^ n x S') :
                                                              x S'

                                                              A subsemiring is an -subalgebra.

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

                                                                A subring is a -subalgebra.

                                                                Instances For
                                                                  @[simp]
                                                                  theorem mem_subalgebraOfSubring {R : Type u_1} [Ring R] {x : R} {S : Subring R} :