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 : Type v

• carrier : Set A
• mul_mem' : ∀ {a b : A}, a ∈ s.carrier → b ∈ s.carrier → a * b ∈ s.carrier
• one_mem' : 1 ∈ s.carrier
• add_mem' : ∀ {a b : A}, a ∈ s.carrier → b ∈ s.carrier → a + 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.

instance Subalgebra.instSetLikeSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : SetLike (Subalgebra R A) A

instance Subalgebra.SubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : SubsemiringClass (Subalgebra R A) A

@[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) : Subalgebra R A

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

@[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) : Subalgebra.copy S s hs = S

instance Subalgebra.instSMulMemClass {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : SMulMemClass (Subalgebra R A) R A

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 ∈ L → x ∈ S) : List.prod L ∈ 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 ∈ L → x ∈ S) : List.sum L ∈ 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 ∈ m → x ∈ S) : Multiset.sum m ∈ 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 ∈ t → f 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 ∈ m → x ∈ S) : Multiset.prod m ∈ 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 ∈ t → f x ∈ S) : (Finset.prod t fun x => f x) ∈ S

instance Subalgebra.instSubringClassSubalgebraToCommSemiringToSemiringInstSetLikeSubalgebra {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) 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 : 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

def Subalgebra.toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : AddSubmonoid A

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

def Subalgebra.toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : Subring A

A subalgebra over a ring is also a Subring.

@[simp]

theorem Subalgebra.mem_toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} {x : A} : x ∈ Subalgebra.toSubring S ↔ x ∈ S

@[simp]

theorem Subalgebra.coe_toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : ↑(Subalgebra.toSubring S) = ↑S

theorem Subalgebra.toSubring_injective {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] : Function.Injective Subalgebra.toSubring

theorem Subalgebra.toSubring_inj {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} {U : Subalgebra R A} : Subalgebra.toSubring S = Subalgebra.toSubring U ↔ S = U

instance Subalgebra.instInhabitedSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Inhabited { x // x ∈ S }

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.toStrictOrderedSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [StrictOrderedSemiring A] [Algebra R A] (S : Subalgebra R A) : StrictOrderedSemiring { x // x ∈ S }

instance Subalgebra.toOrderedCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [OrderedCommSemiring A] [Algebra R A] (S : Subalgebra R A) : OrderedCommSemiring { x // x ∈ S }

instance Subalgebra.toStrictOrderedCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [StrictOrderedCommSemiring A] [Algebra R A] (S : Subalgebra R A) : StrictOrderedCommSemiring { 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.toLinearOrderedSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [LinearOrderedSemiring A] [Algebra R A] (S : Subalgebra R A) : LinearOrderedSemiring { x // x ∈ S }

instance Subalgebra.toLinearOrderedCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [LinearOrderedCommSemiring A] [Algebra R A] (S : Subalgebra R A) : LinearOrderedCommSemiring { 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 }

instance Subalgebra.toLinearOrderedCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [LinearOrderedCommRing A] [Algebra R A] (S : Subalgebra R A) : LinearOrderedCommRing { x // x ∈ S }

def Subalgebra.toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Subalgebra R A ↪o Submodule R A

The forgetful map from Subalgebra to Submodule as an OrderEmbedding

@[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.instModuleSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToNonAssocSemiringToSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Module R { x // x ∈ S }

instance Subalgebra.instIsScalarTowerSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSMulZeroToZeroToMonoidWithZeroToZeroMemClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToAddSubmonoidClassSubsemiringClassToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZeroToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSubsemiringInstModuleSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToNonAssocSemiringToSubsemiringToSMulToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroModule' {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 { 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 }

instance Subalgebra.noZeroSMulDivisors_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [NoZeroSMulDivisors R A] : NoZeroSMulDivisors 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.

@[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]

theorem Subalgebra.toSubring_subtype {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : Subring.subtype (Subalgebra.toSubring S) = ↑(Subalgebra.val S)

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.

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) : Subalgebra R B

Transport a subalgebra via an algebra homomorphism.

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) : Function.Injective (Subalgebra.map f)

@[simp]

theorem Subalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Subalgebra.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) : Subalgebra.map g (Subalgebra.map f S) = Subalgebra.map (AlgHom.comp g 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 ∈ 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) : Subalgebra R A

Preimage of a subalgebra under an algebra homomorphism.

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} : Subalgebra.map f S ≤ U ↔ S ≤ Subalgebra.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) : GaloisConnection (Subalgebra.map f) (Subalgebra.comap f)

@[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 ∈ p → y ∈ p → x * y ∈ p) : Subalgebra R A

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

@[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 ∈ p → y ∈ p → x * 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 ∈ p → y ∈ p → x * 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 ∈ s → y ∈ s → x * y ∈ s) : Submodule.toSubalgebra s h1 hmul = { toSubsemiring := { toSubmonoid := { toSubsemigroup := { carrier := ↑s, mul_mem' := hmul }, one_mem' := h1 }, add_mem' := (_ : ∀ {a b : A}, a ∈ s → b ∈ s → a + 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 ∈ s → b ∈ s → a + 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 ∈ p → y ∈ p → x * 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 ∈ S → x_1 ∈ S → x * 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) : Subalgebra R B

Range of an AlgHom as a subalgebra.

@[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) : AlgHom.range (AlgHom.comp g f) = Subalgebra.map g (AlgHom.range f)

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) : AlgHom.range (AlgHom.comp g f) ≤ AlgHom.range g

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.

@[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) : AlgHom.comp (Subalgebra.val S) (AlgHom.codRestrict f 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) : ↑(↑(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) : Function.Injective ↑(AlgHom.codRestrict f S hf) ↔ Function.Injective ↑f

@[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.

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) : Subalgebra R A

The equalizer of two R-algebra homomorphisms

@[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 : B → A} {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.

@[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 : B → A} {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 : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g ↑f) (x : { x // x ∈ AlgHom.range f }) : ↑(AlgEquiv.symm (AlgEquiv.ofLeftInverse h)) 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] { x // x ∈ AlgHom.range f }

Restrict an injective algebra homomorphism to an algebra isomorphism

@[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

@[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

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

The minimal subalgebra that includes s.

theorem Algebra.gc {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : GaloisConnection (Algebra.adjoin R) SetLike.coe

def Algebra.gi {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : GaloisInsertion (Algebra.adjoin R) SetLike.coe

Galois insertion between adjoin and coe.

instance Algebra.instCompleteLatticeSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : CompleteLattice (Subalgebra R A)

@[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} : x ∈ ⊤

@[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] : Subalgebra.toSubring ⊤ = ⊤

@[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} : Subalgebra.toSubring S = ⊤ ↔ S = ⊤

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 ∈ S → x ∈ 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 ∈ T → x ∈ 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) : Subalgebra.map f (S ⊔ T) = Subalgebra.map f S ⊔ Subalgebra.map f T

@[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 ∈ S → x ∈ 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)

instance Algebra.instInhabitedSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Inhabited (Subalgebra R A)

theorem Algebra.mem_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} : x ∈ ⊥ ↔ x ∈ Set.range ↑(algebraMap R 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] : ↑⊥ = Set.range ↑(algebraMap 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

theorem Algebra.range_top_iff_surjective {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) : AlgHom.range f = ⊤ ↔ Function.Surjective ↑f

@[simp]

theorem Algebra.range_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : AlgHom.range (AlgHom.id 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) : Subalgebra.map f ⊤ = AlgHom.range f

@[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) : Subalgebra.map f ⊥ = ⊥

@[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) : Subalgebra.comap f ⊤ = ⊤

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.

theorem Algebra.surjective_algebraMap_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Function.Surjective ↑(algebraMap R A) ↔ ⊤ = ⊥

theorem Algebra.bijective_algebraMap_iff {R : Type u_1} {A : Type u_2} [Field R] [Semiring A] [Nontrivial A] [Algebra R A] : Function.Bijective ↑(algebraMap R A) ↔ ⊤ = ⊥

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.

@[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.

@[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.

instance Subalgebra.subsingleton_of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [Subsingleton A] : Subsingleton (Subalgebra R A)

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)] : Subsingleton (A →ₐ[R] B)

instance AlgEquiv.subsingleton_left {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)] : Subsingleton (A ≃ₐ[R] B)

instance AlgEquiv.subsingleton_right {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Subsingleton (Subalgebra R B)] : Subsingleton (A ≃ₐ[R] B)

theorem Subalgebra.range_val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : AlgHom.range (Subalgebra.val S) = S

instance Subalgebra.instUniqueSubalgebraToSemiringId {R : Type u} [CommSemiring R] : Unique (Subalgebra R R)

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

theorem Subalgebra.inclusion_injective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S ≤ T) : Function.Injective ↑(Subalgebra.inclusion h)

@[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.

@[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) : AlgEquiv.symm (Subalgebra.equivOfEq S T h) = Subalgebra.equivOfEq T S (_ : T = S)

@[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) : AlgEquiv.trans (Subalgebra.equivOfEq S T hST) (Subalgebra.equivOfEq T U hTU) = Subalgebra.equivOfEq S U (_ : S = 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.

@[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] : Subalgebra.prod ⊤ ⊤ = ⊤

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 ≤ T → S₁ ≤ 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.

@[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) : AlgHom.comp (Subalgebra.iSupLift K dir f hf T hT) (Subalgebra.inclusion h) = f i

@[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

instance Subalgebra.instFaithfulSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraInstSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra {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 { x // x ∈ S } α

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

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

instance Subalgebra.instDistribMulActionSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToMonoidToMonoidToMonoidWithZeroToSubmonoidToNonAssocSemiringToSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [AddMonoid α] [DistribMulAction A α] (S : Subalgebra R A) : DistribMulAction { x // x ∈ S } α

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

instance Subalgebra.instSMulWithZeroSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraZeroToZeroToMonoidWithZeroToZeroMemClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToAddSubmonoidClassSubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [Zero α] [SMulWithZero A α] (S : Subalgebra R A) : SMulWithZero { x // x ∈ S } α

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

instance Subalgebra.instMulActionWithZeroSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToMonoidWithZeroToSemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [Zero α] [MulActionWithZero A α] (S : Subalgebra R A) : MulActionWithZero { x // x ∈ S } α

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) : RingHom.range (algebraMap { x // x ∈ S } A) = Subalgebra.toSubring S

instance Subalgebra.noZeroSMulDivisors_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A] (S : Subalgebra R A) : NoZeroSMulDivisors { x // x ∈ S } A

theorem Set.algebraMap_mem_center {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : ↑(algebraMap R A) r ∈ Set.center A

def Subalgebra.center (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : Subalgebra R A

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

theorem Subalgebra.coe_center (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : ↑(Subalgebra.center R A) = Set.center A

@[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.center_toSubring (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Algebra R A] : Subalgebra.toSubring (Subalgebra.center R A) = Subring.center A

@[simp]

theorem Subalgebra.center_eq_top (R : Type u) [CommSemiring R] (A : Type u_1) [CommSemiring A] [Algebra R A] : Subalgebra.center R A = ⊤

instance Subalgebra.instCommSemiringSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraCenter {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : CommSemiring { x // x ∈ Subalgebra.center R A }

instance Subalgebra.instCommRingSubtypeMemSubalgebraToSemiringInstMembershipInstSetLikeSubalgebraCenter {R : Type u} [CommSemiring R] {A : Type u_1} [Ring A] [Algebra R A] : CommRing { x // x ∈ Subalgebra.center R A }

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) : ↑(algebraMap R A) r ∈ Set.centralizer s

def Subalgebra.centralizer (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : Subalgebra R A

The centralizer of a set as a subalgebra.

@[simp]

theorem Subalgebra.coe_centralizer (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : ↑(Subalgebra.centralizer R s) = Set.centralizer s

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 ∈ s → 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) : Subalgebra.center R A ≤ Subalgebra.centralizer R s

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) : Subalgebra.centralizer R t ≤ Subalgebra.centralizer R s

@[simp]

theorem Subalgebra.centralizer_eq_top_iff_subset (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} : Subalgebra.centralizer R s = ⊤ ↔ s ⊆ ↑(Subalgebra.center R A)

@[simp]

theorem Subalgebra.centralizer_univ (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Subalgebra.centralizer R Set.univ = Subalgebra.center R A

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'

def subalgebraOfSubsemiring {R : Type u_1} [Semiring R] (S : Subsemiring R) : Subalgebra ℕ R

A subsemiring is an ℕ-subalgebra.

@[simp]

theorem mem_subalgebraOfSubsemiring {R : Type u_1} [Semiring R] {x : R} {S : Subsemiring R} : x ∈ subalgebraOfSubsemiring S ↔ x ∈ S

def subalgebraOfSubring {R : Type u_1} [Ring R] (S : Subring R) : Subalgebra ℤ R

A subring is a ℤ-subalgebra.

@[simp]

theorem mem_subalgebraOfSubring {R : Type u_1} [Ring R] {x : R} {S : Subring R} : x ∈ subalgebraOfSubring S ↔ x ∈ S