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

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

• carrier : Set A
• mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• algebraMap_mem' : ∀ (r : R), (algebraMap R A) r ∈ self.carrier

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

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

Equations

• Subalgebra.instSetLikeSubalgebra = { coe := fun (s : Subalgebra R A) => s.carrier, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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.natCast_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (n : ℕ) : ↑n ∈ S

theorem Subalgebra.list_prod_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {L : List A} (h : ∀ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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

Equations

• ⋯ = ⋯

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.intCast_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) (n : ℤ) : ↑n ∈ S

@[deprecated natCast_mem]

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

Alias of Subalgebra.natCast_mem.

@[deprecated intCast_mem]

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

Alias of Subalgebra.intCast_mem.

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.

Equations

• Subalgebra.toAddSubmonoid S = Subsemiring.toAddSubmonoid S.toSubsemiring

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.

Equations

• Subalgebra.toSubring S = let __src := S.toSubsemiring; { toSubsemiring := __src, neg_mem' := ⋯ }

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

Equations

• Subalgebra.instInhabitedSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra S = { default := 0 }

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 ↥S

Equations

• Subalgebra.toSemiring S = Subsemiring.toSemiring S.toSubsemiring

instance Subalgebra.toCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) : CommSemiring ↥S

Equations

• Subalgebra.toCommSemiring S = Subsemiring.toCommSemiring S.toSubsemiring

instance Subalgebra.toRing {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : Ring ↥S

Equations

• Subalgebra.toRing S = Subring.toRing (Subalgebra.toSubring S)

instance Subalgebra.toCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) : CommRing ↥S

Equations

• Subalgebra.toCommRing S = Subring.toCommRing (Subalgebra.toSubring 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

Equations

• One or more equations did not get rendered due to their size.

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

theorem Subalgebra.toSubmodule_injective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Function.Injective ⇑Subalgebra.toSubmodule

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' ↥S

Equations

• Subalgebra.module' S = Submodule.module' (Subalgebra.toSubmodule S)

instance Subalgebra.instModuleSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToNonAssocSemiringToSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Module R ↥S

Equations

• One or more equations did not get rendered due to their size.

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 ↥S

Equations

• ⋯ = ⋯

instance Subalgebra.algebra' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] : Algebra R' ↥S

Equations

• Subalgebra.algebra' S = let __src := RingHom.codRestrict (algebraMap R' A) S ⋯; Algebra.mk __src ⋯ ⋯

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

Equations

• Subalgebra.algebra S = Subalgebra.algebra' 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 ↥S

Equations

• ⋯ = ⋯

theorem Subalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (y : ↥S) : ↑(x + y) = ↑x + ↑y

theorem Subalgebra.coe_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (y : ↥S) : ↑(x * y) = ↑x * ↑y

theorem Subalgebra.coe_zero {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↑0 = 0

theorem Subalgebra.coe_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↑1 = 1

theorem Subalgebra.coe_neg {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (x : ↥S) : ↑(-x) = -↑x

theorem Subalgebra.coe_sub {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (x : ↥S) (y : ↥S) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem Subalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : ↥S) : ↑(r • x) = r • ↑x

@[simp]

theorem Subalgebra.coe_algebraMap {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] (r : R') : ↑((algebraMap R' ↥S) r) = (algebraMap R' A) r

theorem Subalgebra.coe_pow {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

theorem Subalgebra.coe_eq_zero {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : ↥S} : ↑x = 0 ↔ x = 0

theorem Subalgebra.coe_eq_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : ↥S} : ↑x = 1 ↔ x = 1

def Subalgebra.val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↥S →ₐ[R] A

Embedding of a subalgebra into the algebra.

Equations

• Subalgebra.val S = { toRingHom := { toMonoidHom := { toOneHom := { toFun := Subtype.val, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, commutes' := ⋯ }

@[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 : ↥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) : ↥(Subalgebra.toSubmodule S) ≃ₗ[R] ↥S

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

Equations

• Subalgebra.toSubmoduleEquiv S = LinearEquiv.ofEq (Subalgebra.toSubmodule S) (Subalgebra.toSubmodule S) ⋯

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.

Equations

• Subalgebra.map f S = let __src := Subsemiring.map (↑f) S.toSubsemiring; { toSubsemiring := __src, algebraMap_mem' := ⋯ }

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 ∈ 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.toRingHom 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.

Equations

• Subalgebra.comap f S = let __src := Subsemiring.comap (↑f) S.toSubsemiring; { toSubsemiring := __src, algebraMap_mem' := ⋯ }

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 ↥S

Equations

• ⋯ = ⋯

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 ↥S

Equations

• ⋯ = ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

@[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' := ⋯, zero_mem' := ⋯ }, algebraMap_mem' := ⋯ }

@[simp]

theorem Submodule.toSubalgebra_toSubmodule {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ 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) ⋯ ⋯ = 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.

Equations

• AlgHom.range φ = let __src := RingHom.rangeS φ.toRingHom; { toSubsemiring := __src, algebraMap_mem' := ⋯ }

@[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 : A), φ x = y

theorem AlgHom.mem_range_self {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) (x : A) : φ x ∈ 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] ↥S

Restrict the codomain of an algebra homomorphism.

Equations

• AlgHom.codRestrict f S hf = let __src := RingHom.codRestrict (↑f) S hf; { toRingHom := __src, commutes' := ⋯ }

@[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] ↥(AlgHom.range f)

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

This is the bundled version of Set.rangeFactorization.

Equations

• AlgHom.rangeRestrict f = AlgHom.codRestrict f (AlgHom.range f) ⋯

theorem AlgHom.rangeRestrict_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) : Function.Surjective ⇑(AlgHom.rangeRestrict f)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• AlgHom.fintypeRange φ = Set.fintypeRange ⇑φ

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] ↥(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.

Equations

• One or more equations did not get rendered due to their size.

@[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 : ↥(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] ↥(AlgHom.range f)

Restrict an injective algebra homomorphism to an algebra isomorphism

Equations

• AlgEquiv.ofInjective f hf = AlgEquiv.ofLeftInverse ⋯

@[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] ↥(AlgHom.range f)

Restrict an algebra homomorphism between fields to an algebra isomorphism

Equations

• AlgEquiv.ofInjectiveField f = AlgEquiv.ofInjective f ⋯

@[simp]

theorem AlgEquiv.subalgebraMap_symm_apply_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (y : ↑(⇑↑(RingEquiv.toAddEquiv (AlgEquiv.toRingEquiv e)) '' ↑(Subsemiring.toAddSubmonoid S.toSubsemiring))) : ↑((AlgEquiv.symm (AlgEquiv.subalgebraMap e S)) y) = (AddEquiv.symm ↑↑e) ↑y

@[simp]

theorem AlgEquiv.subalgebraMap_apply_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (x : ↑↑(Subsemiring.toAddSubmonoid S.toSubsemiring)) : ↑((AlgEquiv.subalgebraMap e S) x) = e ↑x

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

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

Equations

• AlgEquiv.subalgebraMap e S = let __src := RingEquiv.subsemiringMap (AlgEquiv.toRingEquiv e) S.toSubsemiring; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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.

Equations

• Algebra.adjoin R s = let __src := Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s); { toSubsemiring := __src, algebraMap_mem' := ⋯ }

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.

Equations

• Algebra.gi = { choice := fun (s : Set A) (hs : ↑(Algebra.adjoin R s) ≤ s) => Subalgebra.copy (Algebra.adjoin R s) s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

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

Equations

• Algebra.instCompleteLatticeSubalgebra = let __spread.0 := GaloisInsertion.liftCompleteLattice Algebra.gi; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• Algebra.instInhabitedSubalgebra = { default := ⊥ }

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 ⊥ = 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] ↥⊤

AlgHom to ⊤ : Subalgebra R A.

Equations

• Algebra.toTop = AlgHom.codRestrict (AlgHom.id 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)) : ↥⊥ ≃ₐ[R] R

The bottom subalgebra is isomorphic to the base ring.

Equations

• Algebra.botEquivOfInjective h = AlgEquiv.symm (AlgEquiv.ofBijective (Algebra.ofId R ↥⊥) ⋯)

@[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 ↥⊥) a

noncomputable def Algebra.botEquiv (F : Type u_1) (R : Type u_2) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] : ↥⊥ ≃ₐ[F] F

The bottom subalgebra is isomorphic to the field.

Equations

• Algebra.botEquiv F R = Algebra.botEquivOfInjective ⋯

@[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 : ↥⊤) : Subalgebra.topEquiv a = ↑a

def Subalgebra.topEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : ↥⊤ ≃ₐ[R] A

The top subalgebra is isomorphic to the algebra.

This is the algebra version of Submodule.topEquiv.

Equations

• Subalgebra.topEquiv = AlgEquiv.ofAlgHom (Subalgebra.val ⊤) Algebra.toTop ⋯ ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• Subalgebra.instUniqueSubalgebraToSemiringId = let __src := inferInstanceAs (Inhabited (Subalgebra R R)); { toInhabited := __src, uniq := ⋯ }

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) : ↥S →ₐ[R] ↥T

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

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

Equations

• One or more equations did not get rendered due to their size.

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 ⋯ = AlgHom.id R ↥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 := ⋯ }

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 : ↥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 : ↥S) : (Subalgebra.inclusion htu) ((Subalgebra.inclusion hst) x) = (Subalgebra.inclusion ⋯) 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 : ↥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 : ↥S) : (Subalgebra.equivOfEq S T h) x = { val := ↑x, property := ⋯ }

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) : ↥S ≃ₐ[R] ↥T

Two subalgebras that are equal are also equivalent as algebras.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

theorem Subalgebra.range_comp_val {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) : AlgHom.range (AlgHom.comp f (Subalgebra.val S)) = Subalgebra.map f S

noncomputable def Subalgebra.equivMapOfInjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) : ↥S ≃ₐ[R] ↥(Subalgebra.map f S)

A subalgebra is isomorphic to its image under an injective AlgHom

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subalgebra.coe_equivMapOfInjective_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) (x : ↥S) : ↑((Subalgebra.equivMapOfInjective S f hf) x) = f ↑x

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 (↥S) α

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

Equations

• Subalgebra.instSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra S = inferInstanceAs (SMul (↥S.toSubsemiring) α)

theorem Subalgebra.smul_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [SMul A α] {S : Subalgebra R A} (g : ↥S) (m : α) : g • m = ↑g • m

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

instance Subalgebra.isScalarTower_mid {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [Semiring S] [AddCommMonoid T] [Algebra R S] [Module R T] [Module S T] [IsScalarTower R S T] (S' : Subalgebra R S) : IsScalarTower R (↥S') T

Equations

• ⋯ = ⋯

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 (↥S) α

Equations

• ⋯ = ⋯

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 (↥S) α

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

Equations

• One or more equations did not get rendered due to their size.

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 (↥S) α

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

Equations

• One or more equations did not get rendered due to their size.

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 (↥S) α

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

Equations

• One or more equations did not get rendered due to their size.

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 (↥S) α

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

Equations

• Subalgebra.instMulActionWithZeroSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToMonoidWithZeroToSemiring S = inferInstanceAs (MulActionWithZero (↥S.toSubsemiring) α)

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

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

Equations

• Subalgebra.moduleLeft S = inferInstanceAs (Module (↥S.toSubsemiring) α)

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

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

Equations

• Subalgebra.toAlgebra S = Algebra.ofSubsemiring S.toSubsemiring

theorem Subalgebra.algebraMap_eq {α : Type u_1} {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α] (S : Subalgebra R A) : algebraMap (↥S) α = 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 (↥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 (↥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 (↥S) A

Equations

• ⋯ = ⋯

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.

Equations

• Subalgebra.center R A = let __src := Subsemiring.center A; { toSubsemiring := __src, algebraMap_mem' := ⋯ }

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 ↥(Subalgebra.center R A)

Equations

• Subalgebra.instCommSemiringSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraCenter = inferInstanceAs (CommSemiring ↥(Subsemiring.center A))

instance Subalgebra.instCommRingSubtypeMemSubalgebraToSemiringInstMembershipInstSetLikeSubalgebraCenter {R : Type u} [CommSemiring R] {A : Type u_1} [Ring A] [Algebra R A] : CommRing ↥(Subalgebra.center R A)

Equations

• Subalgebra.instCommRingSubtypeMemSubalgebraToSemiringInstMembershipInstSetLikeSubalgebraCenter = inferInstanceAs (CommRing ↥(Subring.center 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.

Equations

• Subalgebra.centralizer R s = let __src := Subsemiring.centralizer s; { toSubsemiring := __src, algebraMap_mem' := ⋯ }

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

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

A subsemiring is an ℕ-subalgebra.

Equations

• subalgebraOfSubsemiring S = { toSubsemiring := S, algebraMap_mem' := ⋯ }

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

Equations

• subalgebraOfSubring S = { toSubsemiring := S.toSubsemiring, algebraMap_mem' := ⋯ }

@[simp]

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