Mathlib.Algebra.Algebra.Basic

PUnit.algebra instance

: Algebra R PUnit.{v + 1}

Full source

instance _root_.PUnit.algebra : Algebra R PUnitPUnit.{v + 1} where
  algebraMap :=
  { toFun _ := PUnit.unit
    map_one' := rfl
    map_mul' _ _ := rfl
    map_zero' := rfl
    map_add' _ _ := rfl }
  commutes' _ _ := rfl
  smul_def' _ _ := rfl

Algebra Structure on the One-Element Type

Informal description

For any commutative semiring $R$, the one-element type $\mathrm{PUnit}$ has a canonical algebra structure over $R$.

Algebra.algebraMap_pUnit theorem

(r : R) : algebraMap R PUnit r = PUnit.unit

Full source

@[simp]
theorem algebraMap_pUnit (r : R) : algebraMap R PUnit r = PUnit.unit :=
  rfl

Algebra Map to PUnit is Constant

Informal description

For any commutative semiring $R$ and any element $r \in R$, the algebra map from $R$ to the one-element type $\mathrm{PUnit}$ sends $r$ to the unique element $\mathrm{PUnit.unit}$ of $\mathrm{PUnit}$.

ULift.algebra instance

: Algebra R (ULift A)

Full source

instance _root_.ULift.algebra : Algebra R (ULift A) :=
  { ULift.module' with
    algebraMap :=
    { (ULift.ringEquiv : ULiftULift A ≃+* A).symm.toRingHom.comp (algebraMap R A) with
      toFun := fun r => ULift.up (algebraMap R A r) }
    commutes' := fun r x => ULift.down_injective <| Algebra.commutes r x.down
    smul_def' := fun r x => ULift.down_injective <| Algebra.smul_def' r x.down }

Algebra Structure on Lifted Types

Informal description

For any commutative semiring $R$ and any $R$-algebra $A$, the lifted type $\mathrm{ULift}\,A$ is also an $R$-algebra, with the algebra structure inherited from $A$.

ULift.algebraMap_eq theorem

(r : R) : algebraMap R (ULift A) r = ULift.up (algebraMap R A r)

Full source

theorem _root_.ULift.algebraMap_eq (r : R) :
    algebraMap R (ULift A) r = ULift.up (algebraMap R A r) :=
  rfl

Algebra Map Equality for Lifted Types

Informal description

For any commutative semiring $R$, any $R$-algebra $A$, and any element $r \in R$, the algebra map from $R$ to the lifted algebra $\mathrm{ULift}\,A$ satisfies $$\mathrm{algebraMap}\,R\,(\mathrm{ULift}\,A)\,r = \mathrm{ULift.up}\,(\mathrm{algebraMap}\,R\,A\,r).$$

ULift.down_algebraMap theorem

(r : R) : (algebraMap R (ULift A) r).down = algebraMap R A r

Full source

@[simp]
theorem _root_.ULift.down_algebraMap (r : R) : (algebraMap R (ULift A) r).down = algebraMap R A r :=
  rfl

Down Projection of Algebra Map on Lifted Types

Informal description

For any commutative semiring $R$ and $R$-algebra $A$, the down projection of the algebra map from $R$ to $\mathrm{ULift}\,A$ evaluated at $r \in R$ equals the algebra map from $R$ to $A$ evaluated at $r$. In symbols: $$(\mathrm{algebraMap}\,R\,(\mathrm{ULift}\,A)\,r).\mathrm{down} = \mathrm{algebraMap}\,R\,A\,r.$$

Algebra.ofSubsemiring instance

(S : Subsemiring R) : Algebra S A

Full source

/-- Algebra over a subsemiring. This builds upon `Subsemiring.module`. -/
instance ofSubsemiring (S : Subsemiring R) : Algebra S A where
  algebraMap := (algebraMap R A).comp S.subtype
  smul := (· • ·)
  commutes' r x := Algebra.commutes (r : R) x
  smul_def' r x := Algebra.smul_def (r : R) x

Subsemiring as Algebra over Parent Semiring

Informal description

For any commutative semiring $R$ and any subsemiring $S$ of $R$, there is a canonical algebra structure on $S$ over $R$. This means that $S$ inherits the structure of an $R$-algebra from the inclusion map $S \hookrightarrow R$.

Algebra.algebraMap_ofSubsemiring theorem

(S : Subsemiring R) : (algebraMap S R : S →+* R) = Subsemiring.subtype S

Full source

theorem algebraMap_ofSubsemiring (S : Subsemiring R) :
    (algebraMap S R : S →+* R) = Subsemiring.subtype S :=
  rfl

Algebra Map from Subsemiring Equals Inclusion Homomorphism

Informal description

For any commutative semiring $R$ and any subsemiring $S$ of $R$, the algebra map from $S$ to $R$ (as a semiring homomorphism) is equal to the inclusion homomorphism of $S$ into $R$.

Algebra.coe_algebraMap_ofSubsemiring theorem

(S : Subsemiring R) : (algebraMap S R : S → R) = Subtype.val

Full source

theorem coe_algebraMap_ofSubsemiring (S : Subsemiring R) : (algebraMap S R : S → R) = Subtype.val :=
  rfl

Algebra map coincides with inclusion for subsemirings

Informal description

For any subsemiring $S$ of a commutative semiring $R$, the algebra map from $S$ to $R$ (when viewed as a function) coincides with the canonical inclusion map $\text{Subtype.val} : S \to R$ that sends an element of $S$ to its underlying element in $R$.

Algebra.algebraMap_ofSubsemiring_apply theorem

(S : Subsemiring R) (x : S) : algebraMap S R x = x

Full source

theorem algebraMap_ofSubsemiring_apply (S : Subsemiring R) (x : S) : algebraMap S R x = x :=
  rfl

Algebra Map from Subsemiring Acts as Inclusion

Informal description

For any subsemiring $S$ of a commutative semiring $R$, the algebra map $\text{algebraMap}\, S\, R$ sends an element $x \in S$ to itself when viewed as an element of $R$, i.e., $\text{algebraMap}\, S\, R\, x = x$.

Algebra.ofSubring instance

{R A : Type*} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) : Algebra S A

Full source

/-- Algebra over a subring. This builds upon `Subring.module`. -/
instance ofSubring {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) :
    Algebra S A where
  algebraMap := (algebraMap R A).comp S.subtype
  smul := (· • ·)
  commutes' r x := Algebra.commutes (r : R) x
  smul_def' r x := Algebra.smul_def (r : R) x

Algebra Structure Induced by Subring Inclusion

Informal description

For any commutative ring $R$, ring $A$ with an algebra structure over $R$, and subring $S$ of $R$, there is a canonical algebra structure of $S$ on $A$ induced by the inclusion $S \hookrightarrow R$.

Algebra.algebraMap_ofSubring theorem

{R : Type*} [CommRing R] (S : Subring R) : (algebraMap S R : S →+* R) = Subring.subtype S

Full source

theorem algebraMap_ofSubring {R : Type*} [CommRing R] (S : Subring R) :
    (algebraMap S R : S →+* R) = Subring.subtype S :=
  rfl

Algebra Map from Subring Equals Inclusion Homomorphism

Informal description

For any commutative ring $R$ and subring $S$ of $R$, the algebra map from $S$ to $R$ (as a ring homomorphism) is equal to the inclusion homomorphism of $S$ into $R$.

Algebra.coe_algebraMap_ofSubring theorem

{R : Type*} [CommRing R] (S : Subring R) : (algebraMap S R : S → R) = Subtype.val

Full source

theorem coe_algebraMap_ofSubring {R : Type*} [CommRing R] (S : Subring R) :
    (algebraMap S R : S → R) = Subtype.val :=
  rfl

Algebra Map from Subring Equals Inclusion

Informal description

For any commutative ring $R$ and subring $S$ of $R$, the algebra map from $S$ to $R$ (when viewed as a function) coincides with the canonical inclusion map $\text{Subtype.val} : S \to R$.

Algebra.algebraMap_ofSubring_apply theorem

{R : Type*} [CommRing R] (S : Subring R) (x : S) : algebraMap S R x = x

Full source

theorem algebraMap_ofSubring_apply {R : Type*} [CommRing R] (S : Subring R) (x : S) :
    algebraMap S R x = x :=
  rfl

Algebra Map from Subring Acts as Inclusion

Informal description

For any commutative ring $R$ and subring $S$ of $R$, the algebra map $\text{algebraMap}_S^R$ from $S$ to $R$ satisfies $\text{algebraMap}_S^R(x) = x$ for all $x \in S$.

Algebra.algebraMapSubmonoid definition

(S : Type*) [Semiring S] [Algebra R S] (M : Submonoid R) : Submonoid S

Full source

/-- Explicit characterization of the submonoid map in the case of an algebra.
`S` is made explicit to help with type inference -/
def algebraMapSubmonoid (S : Type*) [Semiring S] [Algebra R S] (M : Submonoid R) : Submonoid S :=
  M.map (algebraMap R S)

Image of a submonoid under the algebra map

Informal description

Given a semiring $S$ with an algebra structure over $R$, and a submonoid $M$ of $R$, the submonoid of $S$ obtained by applying the algebra map $\text{algebraMap} \colon R \to S$ to each element of $M$.

Algebra.mem_algebraMapSubmonoid_of_mem theorem

{S : Type*} [Semiring S] [Algebra R S] {M : Submonoid R} (x : M) : algebraMap R S x ∈ algebraMapSubmonoid S M

Full source

theorem mem_algebraMapSubmonoid_of_mem {S : Type*} [Semiring S] [Algebra R S] {M : Submonoid R}
    (x : M) : algebraMapalgebraMap R S x ∈ algebraMapSubmonoid S M :=
  Set.mem_image_of_mem (algebraMap R S) x.2

Image of Submonoid Element under Algebra Map Belongs to Image Submonoid

Informal description

Let $R$ and $S$ be semirings with an algebra structure from $R$ to $S$, and let $M$ be a submonoid of $R$. For any element $x \in M$, the image of $x$ under the algebra map $\text{algebraMap}_R^S$ belongs to the submonoid of $S$ generated by the image of $M$ under $\text{algebraMap}_R^S$.

Algebra.mul_sub_algebraMap_commutes theorem

[Ring A] [Algebra R A] (x : A) (r : R) : x * (x - algebraMap R A r) = (x - algebraMap R A r) * x

Full source

theorem mul_sub_algebraMap_commutes [Ring A] [Algebra R A] (x : A) (r : R) :
    x * (x - algebraMap R A r) = (x - algebraMap R A r) * x := by rw [mul_sub, ← commutes, sub_mul]

Commutation Relation for Multiplication with Shifted Algebra Map

Informal description

Let $A$ be a ring with an algebra structure over a commutative ring $R$. For any element $x \in A$ and any scalar $r \in R$, the following commutation relation holds: \[ x \cdot (x - \text{algebraMap}_R^A(r)) = (x - \text{algebraMap}_R^A(r)) \cdot x \] where $\text{algebraMap}_R^A : R \to A$ is the canonical algebra homomorphism from $R$ to $A$.

Algebra.mul_sub_algebraMap_pow_commutes theorem

[Ring A] [Algebra R A] (x : A) (r : R) (n : ℕ) : x * (x - algebraMap R A r) ^ n = (x - algebraMap R A r) ^ n * x

Full source

theorem mul_sub_algebraMap_pow_commutes [Ring A] [Algebra R A] (x : A) (r : R) (n : ℕ) :
    x * (x - algebraMap R A r) ^ n = (x - algebraMap R A r) ^ n * x := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

Generalized Commutation Relation for Powers of Shifted Algebra Map

Informal description

Let $A$ be a ring with an algebra structure over a commutative ring $R$. For any element $x \in A$, any scalar $r \in R$, and any natural number $n$, the following commutation relation holds: \[ x \cdot (x - \varphi(r))^n = (x - \varphi(r))^n \cdot x \] where $\varphi : R \to A$ is the canonical algebra homomorphism from $R$ to $A$.

Algebra.semiringToRing abbrev

(R : Type*) [CommRing R] [Semiring A] [Algebra R A] : Ring A

Full source

/-- A `Semiring` that is an `Algebra` over a commutative ring carries a natural `Ring` structure.
See note [reducible non-instances]. -/
abbrev semiringToRing (R : Type*) [CommRing R] [Semiring A] [Algebra R A] : Ring A :=
  { __ := (inferInstance : Semiring A)
    __ := Module.addCommMonoidToAddCommGroup R
    intCast := fun z => algebraMap R A z
    intCast_ofNat := fun z => by simp only [Int.cast_natCast, map_natCast]
    intCast_negSucc := fun z => by simp }

Ring Structure Induced by Algebra over a Commutative Ring

Informal description

Given a commutative ring $R$ and a semiring $A$ equipped with an $R$-algebra structure, the semiring $A$ naturally carries the structure of a ring.

Algebra.instSubtypeMemSubringCenter instance

{R : Type*} [Ring R] : Algebra (Subring.center R) R

Full source

instance {R : Type*} [Ring R] : Algebra (Subring.center R) R where
  algebraMap :=
  { toFun := Subtype.val
    map_one' := rfl
    map_mul' _ _ := rfl
    map_zero' := rfl
    map_add' _ _ := rfl }
  commutes' r x := (Subring.mem_center_iff.1 r.2 x).symm
  smul_def' _ _ := rfl

Algebra Structure on the Center of a Ring

Informal description

For any ring $R$, the center of $R$ (the subring of elements that commute with all elements of $R$) has a canonical algebra structure over itself.

Module.End.instAlgebra instance

: Algebra R (Module.End S M)

Full source

instance End.instAlgebra : Algebra R (Module.End S M) :=
  Algebra.ofModule smul_mul_assoc fun r f g => (smul_comm r f g).symm

Algebra Structure on Module Endomorphisms

Informal description

For any semiring $R$ and $S$-module $M$, the ring of $S$-linear endomorphisms $\text{End}_S(M)$ has a canonical $R$-algebra structure when $S$ is an $R$-algebra. The algebra map sends each element $r \in R$ to the scalar multiplication by $r$ composed with the identity endomorphism.

Module.algebraMap_end_eq_smul_id theorem

(a : R) : algebraMap R (End S M) a = a • LinearMap.id

Full source

theorem algebraMap_end_eq_smul_id (a : R) : algebraMap R (End S M) a = a • LinearMap.id :=
  rfl

Algebra Map to Endomorphism Ring as Scalar Multiplication of Identity

Informal description

For any element $a$ in a semiring $R$, the algebra map from $R$ to the ring of $S$-linear endomorphisms of an $S$-module $M$ evaluated at $a$ equals the scalar multiplication of $a$ with the identity linear map on $M$. That is, the algebra map satisfies $\text{algebraMap}_R(\text{End}_S(M))(a) = a \cdot \text{id}_M$.

Module.algebraMap_end_apply theorem

(a : R) (m : M) : algebraMap R (End S M) a m = a • m

Full source

@[simp]
theorem algebraMap_end_apply (a : R) (m : M) : algebraMap R (End S M) a m = a • m :=
  rfl

Algebra Map Action Equals Scalar Multiplication in Module Endomorphisms

Informal description

For any element $a$ in a semiring $R$ and any element $m$ in an $S$-module $M$, the action of the algebra map $\text{algebraMap}_R(\text{End}_S(M))(a)$ on $m$ is equal to the scalar multiplication $a \bullet m$.

Module.ker_algebraMap_end theorem

 (K : Type u) (V : Type v) [Semifield K] [AddCommMonoid V] [Module K V] (a : K) (ha : a ≠ 0) :
  LinearMap.ker ((algebraMap K (End K V)) a) = ⊥

Full source

@[simp]
theorem ker_algebraMap_end (K : Type u) (V : Type v) [Semifield K] [AddCommMonoid V] [Module K V]
    (a : K) (ha : a ≠ 0) : LinearMap.ker ((algebraMap K (End K V)) a) = ⊥ :=
  LinearMap.ker_smul _ _ ha

Trivial Kernel of Scalar Multiplication Endomorphism: $\ker(a \cdot \text{id}_V) = \{0\}$ for $a \neq 0$

Informal description

Let $K$ be a semifield and $V$ a $K$-module. For any nonzero scalar $a \in K$, the kernel of the $K$-linear endomorphism $a \cdot \text{id}_V$ is the trivial submodule $\{0\}$, i.e., \[ \ker(a \cdot \text{id}_V) = \{0\}. \]

Module.End.algebraMap_isUnit_inv_apply_eq_iff theorem

 {x : R} (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) : (↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m'

Full source

theorem End.algebraMap_isUnit_inv_apply_eq_iff {x : R}
    (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
    (↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m' where
  mp H := H ▸ (isUnit_apply_inv_apply_of_isUnit h m).symm
  mpr H :=
    H.symm ▸ by
      apply_fun ⇑h.unit.val using ((isUnit_iff _).mp h).injective
      simpa using Module.End.isUnit_apply_inv_apply_of_isUnit h (x • m')

Inverse of Scalar Multiplication Endomorphism Characterization: $f^{-1}(m) = m' \leftrightarrow m = x \cdot m'$

Informal description

Let $R$ and $S$ be semirings, and let $M$ be an $S$-module. For any $x \in R$ such that the algebra map $\text{algebraMap}_R(x) \in \text{End}_S(M)$ is invertible, and for any $m, m' \in M$, we have: \[ f^{-1}(m) = m' \quad \text{if and only if} \quad m = x \cdot m' \] where $f = \text{algebraMap}_R(x)$ is the scalar multiplication by $x$ viewed as an endomorphism of $M$, and $f^{-1}$ denotes its inverse.

Module.End.algebraMap_isUnit_inv_apply_eq_iff' theorem

 {x : R} (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) : m' = (↑h.unit⁻¹ : Module.End S M) m ↔ m = x • m'

Full source

theorem End.algebraMap_isUnit_inv_apply_eq_iff' {x : R}
    (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
    m' = (↑h.unit⁻¹ : Module.End S M) m ↔ m = x • m' where
  mp H := H ▸ (isUnit_apply_inv_apply_of_isUnit h m).symm
  mpr H :=
    H.symm ▸ by
      apply_fun (↑h.unit : M → M) using ((isUnit_iff _).mp h).injective
      simpa using isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm

Invertible Algebra Map Characterization: $m' = f^{-1}(m) \iff m = x \bullet m'$

Informal description

Let $R$ and $S$ be semirings, $M$ an $S$-module, and $x \in R$ such that the algebra map $\text{algebraMap} \colon R \to \text{End}_S(M)$ sends $x$ to an invertible endomorphism (i.e., $\text{algebraMap}(x)$ is a unit in $\text{End}_S(M)$). Then for any $m, m' \in M$, we have the equivalence: \[ m' = f^{-1}(m) \iff m = x \bullet m' \] where $f = \text{algebraMap}(x)$ and $f^{-1}$ denotes its inverse endomorphism.

LinearMap.map_algebraMap_mul theorem

(f : A →ₗ[R] B) (a : A) (r : R) : f (algebraMap R A r * a) = algebraMap R B r * f a

Full source

/-- An alternate statement of `LinearMap.map_smul` for when `algebraMap` is more convenient to
work with than `•`. -/
theorem map_algebraMap_mul (f : A →ₗ[R] B) (a : A) (r : R) :
    f (algebraMap R A r * a) = algebraMap R B r * f a := by
  rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]

Linearity of Scalar Multiplication under Algebra Maps

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any $R$-linear map $f \colon A \to B$, element $a \in A$, and scalar $r \in R$, we have: \[ f(r \cdot a) = r \cdot f(a) \] where $r \cdot a$ denotes the action of $R$ on $A$ via the algebra map $\text{algebraMap} \colon R \to A$, and similarly for $B$.

LinearMap.map_mul_algebraMap theorem

(f : A →ₗ[R] B) (a : A) (r : R) : f (a * algebraMap R A r) = f a * algebraMap R B r

Full source

theorem map_mul_algebraMap (f : A →ₗ[R] B) (a : A) (r : R) :
    f (a * algebraMap R A r) = f a * algebraMap R B r := by
  rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]

Linearity of Right Scalar Multiplication under Algebra Maps

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any $R$-linear map $f \colon A \to B$, element $a \in A$, and scalar $r \in R$, we have: \[ f(a \cdot r) = f(a) \cdot r \] where $a \cdot r$ denotes the right multiplication of $a$ by $r$ via the algebra map $\text{algebraMap} \colon R \to A$, and similarly for $B$.

Semiring.toNatAlgebra instance

: Algebra ℕ R

Full source

/-- Semiring ⥤ ℕ-Alg -/
instance (priority := 99) Semiring.toNatAlgebra : Algebra ℕ R where
  commutes' := Nat.cast_commute
  smul_def' _ _ := nsmul_eq_mul _ _
  algebraMap := Nat.castRingHom R

Natural Number Algebra Structure on Semirings

Informal description

Every semiring $R$ has a canonical $\mathbb{N}$-algebra structure, where the scalar multiplication is given by repeated addition.

nat_algebra_subsingleton instance

: Subsingleton (Algebra ℕ R)

Full source

instance nat_algebra_subsingleton : Subsingleton (Algebra ℕ R) :=
  ⟨fun P Q => by ext; simp⟩

Uniqueness of Natural Number Algebra Structure on Semirings

Informal description

For any semiring $R$, there is at most one $\mathbb{N}$-algebra structure on $R$.

algebraMap_comp_natCast theorem

(R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] : algebraMap R A ∘ Nat.cast = Nat.cast

Full source

@[simp]
lemma algebraMap_comp_natCast (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
    algebraMapalgebraMap R A ∘ Nat.cast = Nat.cast := by
  ext; simp

Compatibility of Algebra Map with Natural Number Embedding

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with an $R$-algebra structure. The composition of the algebra map $\text{algebraMap} \colon R \to A$ with the natural number embedding $\text{Nat.cast} \colon \mathbb{N} \to R$ equals the natural number embedding $\text{Nat.cast} \colon \mathbb{N} \to A$. In other words, for any natural number $n$, we have $\text{algebraMap}(n) = n$ in $A$.

Ring.toIntAlgebra instance

: Algebra ℤ R

Full source

/-- Ring ⥤ ℤ-Alg -/
instance (priority := 99) Ring.toIntAlgebra : Algebra ℤ R where
  commutes' := Int.cast_commute
  smul_def' _ _ := zsmul_eq_mul _ _
  algebraMap := Int.castRingHom R

Canonical $\mathbb{Z}$-Algebra Structure on a Ring

Informal description

For any ring $R$, there is a canonical $\mathbb{Z}$-algebra structure on $R$ where the scalar multiplication is given by the ring multiplication.

algebraMap_int_eq theorem

: algebraMap ℤ R = Int.castRingHom R

Full source

/-- A special case of `eq_intCast'` that happens to be true definitionally -/
@[simp]
theorem algebraMap_int_eq : algebraMap ℤ R = Int.castRingHom R :=
  rfl

Equality of Integer Algebra Map and Canonical Ring Homomorphism

Informal description

The algebra map from the integers $\mathbb{Z}$ to a ring $R$ is equal to the canonical ring homomorphism from $\mathbb{Z}$ to $R$.

int_algebra_subsingleton instance

: Subsingleton (Algebra ℤ R)

Full source

instance int_algebra_subsingleton : Subsingleton (Algebra ℤ R) :=
  ⟨fun P Q => Algebra.algebra_ext P Q <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

Uniqueness of $\mathbb{Z}$-Algebra Structure on a Ring

Informal description

For any ring $R$, there is at most one $\mathbb{Z}$-algebra structure on $R$.

algebraMap_comp_intCast theorem

(R A : Type*) [CommRing R] [Ring A] [Algebra R A] : algebraMap R A ∘ Int.cast = Int.cast

Full source

@[simp]
lemma algebraMap_comp_intCast (R A : Type*) [CommRing R] [Ring A] [Algebra R A] :
    algebraMapalgebraMap R A ∘ Int.cast = Int.cast := by
  ext; simp

Compatibility of Algebra Map with Integer Casting

Informal description

Let $R$ be a commutative ring and $A$ be a ring with an algebra structure over $R$. Then the composition of the algebra map from $R$ to $A$ with the canonical integer casting function equals the integer casting function on $A$, i.e., $\text{algebraMap}_R^A \circ \text{Int.cast} = \text{Int.cast}$.

instFaithfulSMul instance

(R : Type*) [NonAssocSemiring R] : FaithfulSMul R R

Full source

instance (R : Type*) [NonAssocSemiring R] : FaithfulSMul R R := ⟨fun {r₁ r₂} h ↦ by simpa using h 1⟩

Faithful Scalar Multiplication on Non-Associative Semirings

Informal description

For any non-associative semiring $R$, the scalar multiplication action of $R$ on itself is faithful. This means that if two elements $r_1, r_2 \in R$ satisfy $r_1 \cdot x = r_2 \cdot x$ for all $x \in R$, then $r_1 = r_2$.

faithfulSMul_iff_injective_smul_one theorem

[Module R A] [IsScalarTower R A A] : FaithfulSMul R A ↔ Injective (fun r : R ↦ r • (1 : A))

Full source

lemma faithfulSMul_iff_injective_smul_one [Module R A] [IsScalarTower R A A] :
    FaithfulSMulFaithfulSMul R A ↔ Injective (fun r : R ↦ r • (1 : A)) := by
  refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
  · simp only at hr
    rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
  · simpa using hr 1

Faithfulness of scalar multiplication via injectivity of $r \mapsto r \bullet 1$

Informal description

Let $R$ be a semiring and $A$ be a module over $R$ such that the scalar multiplication satisfies the tower property `IsScalarTower R A A`. Then the scalar multiplication action of $R$ on $A$ is faithful if and only if the map $r \mapsto r \bullet 1_A$ from $R$ to $A$ is injective, where $1_A$ is the multiplicative identity in $A$.

faithfulSMul_iff_algebraMap_injective theorem

: FaithfulSMul R A ↔ Injective (algebraMap R A)

Full source

lemma faithfulSMul_iff_algebraMap_injective : FaithfulSMulFaithfulSMul R A ↔ Injective (algebraMap R A) := by
  rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']

Faithfulness of Scalar Multiplication via Injectivity of Algebra Map

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with a faithful scalar multiplication action of $R$ on $A$. Then the scalar multiplication is faithful if and only if the algebra map $\text{algebraMap} : R \to A$ is injective.

FaithfulSMul.algebraMap_injective theorem

: Injective (algebraMap R A)

Full source

lemma algebraMap_injective : Injective (algebraMap R A) :=
  (faithfulSMul_iff_algebraMap_injective R A).mp inferInstance

Injectivity of the Algebra Map under Faithful Scalar Multiplication

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with a faithful scalar multiplication action of $R$ on $A$. Then the algebra map $\text{algebraMap} : R \to A$ is injective.

FaithfulSMul.algebraMap_eq_zero_iff theorem

{r : R} : algebraMap R A r = 0 ↔ r = 0

Full source

@[simp]
lemma algebraMap_eq_zero_iff {r : R} : algebraMapalgebraMap R A r = 0 ↔ r = 0 :=
  map_eq_zero_iff (algebraMap R A) <| algebraMap_injective R A

Algebra Map Zero Criterion under Faithful Scalar Multiplication

Informal description

For any element $r$ in a commutative semiring $R$ and a semiring $A$ with faithful scalar multiplication, the algebra map $\text{algebraMap} : R \to A$ satisfies $\text{algebraMap}(r) = 0$ if and only if $r = 0$.

FaithfulSMul.algebraMap_eq_one_iff theorem

{r : R} : algebraMap R A r = 1 ↔ r = 1

Full source

@[simp]
lemma algebraMap_eq_one_iff {r : R} : algebraMapalgebraMap R A r = 1 ↔ r = 1 :=
  map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R A

Faithful Algebra Map Preserves Identity: $\text{algebraMap}(r) = 1 \leftrightarrow r = 1$

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with a faithful scalar multiplication action of $R$ on $A$. For any element $r \in R$, the algebra map $\text{algebraMap} : R \to A$ satisfies $\text{algebraMap}(r) = 1$ if and only if $r = 1$.

NeZero.of_faithfulSMul theorem

(n : ℕ) [NeZero (n : R)] : NeZero (n : A)

Full source

theorem _root_.NeZero.of_faithfulSMul (n : ℕ) [NeZero (n : R)] :
    NeZero (n : A) :=
  NeZero.nat_of_injective <| FaithfulSMul.algebraMap_injective R A

Non-zero natural numbers remain non-zero under faithful scalar multiplication

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with a faithful scalar multiplication action of $R$ on $A$. For any natural number $n$, if $n$ is non-zero in $R$ (i.e., $n \neq 0$ in $R$), then $n$ is also non-zero in $A$ (i.e., $n \neq 0$ in $A$).

Algebra.charZero_of_charZero theorem

[CharZero R] : CharZero A

Full source

lemma Algebra.charZero_of_charZero [CharZero R] : CharZero A :=
  have := algebraMap_comp_natCast R A
  ⟨this ▸ (FaithfulSMul.algebraMap_injective R A).comp CharZero.cast_injective⟩

Characteristic Zero Preservation in Algebra Extensions

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with an $R$-algebra structure. If $R$ has characteristic zero, then $A$ also has characteristic zero. In other words, the natural number embedding $\mathbb{N} \to A$ is injective whenever the natural number embedding $\mathbb{N} \to R$ is injective.

instFaithfulSMulNatOfCharZero instance

[CharZero R] : FaithfulSMul ℕ R

Full source

instance (priority := 100) [CharZero R] : FaithfulSMul ℕ R := by
  simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℕ R).injective_nat

Faithful Natural Number Scalar Multiplication in Characteristic Zero Semirings

Informal description

For any semiring $R$ of characteristic zero, the scalar multiplication action of the natural numbers $\mathbb{N}$ on $R$ is faithful. That is, the map $\mathbb{N} \times R \to R$ given by $(n, x) \mapsto n \cdot x$ is injective in the first argument.

instFaithfulSMulIntOfCharZero instance

(R : Type*) [Ring R] [CharZero R] : FaithfulSMul ℤ R

Full source

instance (priority := 100) (R : Type*) [Ring R] [CharZero R] : FaithfulSMul ℤ R := by
  simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℤ R).injective_int

Faithful Integer Scalar Multiplication in Characteristic Zero Rings

Informal description

For any ring $R$ of characteristic zero, the scalar multiplication action of the integers $\mathbb{Z}$ on $R$ is faithful. That is, the map $\mathbb{Z} \times R \to R$ given by $(n, x) \mapsto n \cdot x$ is injective in the first argument.

NoZeroSMulDivisors.instOfFaithfulSMul instance

 {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A] [FaithfulSMul R A] :
  NoZeroSMulDivisors R A

Full source

instance (priority := 100) instOfFaithfulSMul {R A : Type*}
    [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A] [FaithfulSMul R A] :
    NoZeroSMulDivisors R A :=
  ⟨fun hcx => (mul_eq_zero.mp ((Algebra.smul_def _ _).symm.trans hcx)).imp_left
    (map_eq_zero_iff (algebraMap R A) <| FaithfulSMul.algebraMap_injective R A).mp⟩

Faithful Scalar Multiplication Implies No Zero Divisors in Algebras

Informal description

Let $R$ be a commutative semiring and $A$ be a semiring with an algebra structure over $R$. If $A$ has no zero divisors and the scalar multiplication action of $R$ on $A$ is faithful, then $A$ satisfies the no zero scalar divisors condition with respect to $R$. That is, for any $r \in R$ and $a \in A$, if $r \cdot a = 0$, then either $r = 0$ or $a = 0$.

NoZeroSMulDivisors.instFaithfulSMulOfNontrivial instance

[Nontrivial A] [NoZeroSMulDivisors R A] : FaithfulSMul R A

Full source

instance [Nontrivial A] [NoZeroSMulDivisors R A] : FaithfulSMul R A where
  eq_of_smul_eq_smul {r₁ r₂} h := by
    specialize h 1
    rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero] at h
    exact h.resolve_right one_ne_zero

Faithful Scalar Multiplication in Nontrivial Modules with No Zero Divisors

Informal description

For any nontrivial type $A$ with a scalar multiplication operation by $R$ that satisfies the no zero scalar divisors condition, the scalar multiplication action of $R$ on $A$ is faithful.

NoZeroSMulDivisors.iff_faithfulSMul theorem

[IsDomain A] : NoZeroSMulDivisors R A ↔ FaithfulSMul R A

Full source

theorem iff_faithfulSMul [IsDomain A] : NoZeroSMulDivisorsNoZeroSMulDivisors R A ↔ FaithfulSMul R A :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

Equivalence of No Zero Scalar Divisors and Faithful Scalar Multiplication in Domains

Informal description

For a domain $A$, the following are equivalent: 1. The scalar multiplication operation of $R$ on $A$ has no zero divisors (i.e., $r \cdot a = 0$ implies $r = 0$ or $a = 0$ for all $r \in R$ and $a \in A$). 2. The scalar multiplication action of $R$ on $A$ is faithful (i.e., distinct elements of $R$ act differently on $A$).

NoZeroSMulDivisors.iff_algebraMap_injective theorem

[IsDomain A] : NoZeroSMulDivisors R A ↔ Injective (algebraMap R A)

Full source

theorem iff_algebraMap_injective [IsDomain A] :
    NoZeroSMulDivisorsNoZeroSMulDivisors R A ↔ Injective (algebraMap R A) := by
  rw [iff_faithfulSMul]
  exact faithfulSMul_iff_algebraMap_injective R A

Equivalence of No Zero Scalar Divisors and Injectivity of Algebra Map in Domains

Informal description

For a domain $A$, the scalar multiplication operation of $R$ on $A$ has no zero divisors if and only if the algebra map $\text{algebraMap} : R \to A$ is injective. In other words, the following are equivalent: 1. For all $r \in R$ and $a \in A$, $r \cdot a = 0$ implies $r = 0$ or $a = 0$. 2. The map $\text{algebraMap} : R \to A$ is injective.

algebra_compatible_smul theorem

(r : R) (m : M) : r • m = (algebraMap R A) r • m

Full source

theorem algebra_compatible_smul (r : R) (m : M) : r • m = (algebraMap R A) r • m := by
  rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]

Compatibility of Scalar Multiplication with Algebra Map: $r \cdot m = \text{algebraMap}(r) \cdot m$

Informal description

For any element $r$ in a commutative semiring $R$ and any element $m$ in a module $M$ over $R$, the scalar multiplication $r \cdot m$ is equal to the scalar multiplication of the image of $r$ under the algebra map $\text{algebraMap} : R \to A$ with $m$, i.e., $r \cdot m = (\text{algebraMap}(r)) \cdot m$.

algebraMap_smul theorem

(r : R) (m : M) : (algebraMap R A) r • m = r • m

Full source

@[simp]
theorem algebraMap_smul (r : R) (m : M) : (algebraMap R A) r • m = r • m :=
  (algebra_compatible_smul A r m).symm

Equality of Scalar Multiplications via Algebra Map: $(\text{algebraMap}(r)) \cdot m = r \cdot m$

Informal description

For any element $r$ in a commutative semiring $R$ and any element $m$ in a module $M$ over $R$, the scalar multiplication of the image of $r$ under the algebra map $\text{algebraMap} : R \to A$ with $m$ is equal to the scalar multiplication of $r$ with $m$, i.e., $(\text{algebraMap}(r)) \cdot m = r \cdot m$.

NoZeroSMulDivisors.trans_faithfulSMul theorem

 (R A M : Type*) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [AddCommMonoid M] [Module R M]
  [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M

Full source

/-- If `M` is `A`-torsion free and `algebraMap R A` is injective, `M` is also `R`-torsion free. -/
theorem NoZeroSMulDivisors.trans_faithfulSMul (R A M : Type*) [CommSemiring R] [Semiring A]
    [Algebra R A] [FaithfulSMul R A] [AddCommMonoid M] [Module R M] [Module A M]
    [IsScalarTower R A M] [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M where
  eq_zero_or_eq_zero_of_smul_eq_zero hx := by
    rw [← algebraMap_smul (A := A)] at hx
    simpa only [map_eq_zero_iff _ <| FaithfulSMul.algebraMap_injective R A] using
      eq_zero_or_eq_zero_of_smul_eq_zero hx

Torsion-Free Property Transfer via Faithful Scalar Multiplication and Algebra Map

Informal description

Let $R$ be a commutative semiring, $A$ a semiring with an $R$-algebra structure, and $M$ an $A$-module that is also an $R$-module. Suppose that: 1. The scalar multiplication action of $R$ on $A$ is faithful (i.e., the algebra map $\text{algebraMap} : R \to A$ is injective). 2. The scalar multiplications satisfy the tower property: $(r \cdot a) \cdot m = r \cdot (a \cdot m)$ for all $r \in R$, $a \in A$, and $m \in M$. 3. $M$ is $A$-torsion free (i.e., $a \cdot m = 0$ implies $a = 0$ or $m = 0$ for $a \in A$ and $m \in M$). Then $M$ is also $R$-torsion free (i.e., $r \cdot m = 0$ implies $r = 0$ or $m = 0$ for $r \in R$ and $m \in M$).

IsScalarTower.to_smulCommClass instance

: SMulCommClass R A M

Full source

instance (priority := 120) IsScalarTower.to_smulCommClass : SMulCommClass R A M :=
  ⟨fun r a m => by
    rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]⟩

Commutativity of Scalar Multiplications in a Tower Structure

Informal description

For a commutative semiring $R$, a semiring $A$ with an $R$-algebra structure, and an $A$-module $M$ that is also an $R$-module, if the scalar multiplications satisfy the tower property $(r \cdot a) \cdot m = r \cdot (a \cdot m)$ for all $r \in R$, $a \in A$, and $m \in M$, then the scalar multiplications by $R$ and $A$ on $M$ commute. That is, $r \cdot (a \cdot m) = a \cdot (r \cdot m)$ for all $r \in R$, $a \in A$, and $m \in M$.

IsScalarTower.to_smulCommClass' instance

: SMulCommClass A R M

Full source

instance (priority := 110) IsScalarTower.to_smulCommClass' : SMulCommClass A R M :=
  SMulCommClass.symm _ _ _

Commutativity of Scalar Multiplications in a Tower Structure (Reversed)

Informal description

For a commutative semiring $R$, a semiring $A$ with an $R$-algebra structure, and an $A$-module $M$ that is also an $R$-module, if the scalar multiplications satisfy the tower property $(r \cdot a) \cdot m = r \cdot (a \cdot m)$ for all $r \in R$, $a \in A$, and $m \in M$, then the scalar multiplications by $A$ and $R$ on $M$ commute. That is, $a \cdot (r \cdot m) = r \cdot (a \cdot m)$ for all $r \in R$, $a \in A$, and $m \in M$.

Algebra.to_smulCommClass instance

{R A} [CommSemiring R] [Semiring A] [Algebra R A] : SMulCommClass R A A

Full source

instance (priority := 200) Algebra.to_smulCommClass {R A} [CommSemiring R] [Semiring A]
    [Algebra R A] : SMulCommClass R A A :=
  IsScalarTower.to_smulCommClass

Commutativity of Scalar Multiplications in an Algebra

Informal description

For any commutative semiring $R$ and semiring $A$ with an $R$-algebra structure, the scalar multiplications by $R$ and $A$ on $A$ commute. That is, for all $r \in R$, $a \in A$, and $x \in A$, we have $r \cdot (a \cdot x) = a \cdot (r \cdot x)$.

smul_algebra_smul_comm theorem

(r : R) (a : A) (m : M) : a • r • m = r • a • m

Full source

theorem smul_algebra_smul_comm (r : R) (a : A) (m : M) : a • r • m = r • a • m :=
  smul_comm _ _ _

Commutativity of Algebra Scalar Multiplication

Informal description

For any elements $r \in R$, $a \in A$, and $m \in M$, the scalar multiplications commute as follows: \[ a \cdot (r \cdot m) = r \cdot (a \cdot m) \]

LinearMap.ltoFun definition

 (R : Type u) (M : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] :
  (M →ₗ[R] A) →ₗ[A] M → A

Full source

/-- `A`-linearly coerce an `R`-linear map from `M` to `A` to a function, given an algebra `A` over
a commutative semiring `R` and `M` a module over `R`. -/
def ltoFun (R : Type u) (M : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M]
    [CommSemiring A] [Algebra R A] : (M →ₗ[R] A) →ₗ[A] M → A where
  toFun f := f.toFun
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Linear map to function conversion

Informal description

Given a commutative semiring $R$, an $R$-module $M$, and a commutative semiring $A$ that is an $R$-algebra, the function `LinearMap.ltoFun` constructs an $A$-linear map from the space of $R$-linear maps $M \to A$ to the space of functions $M \to A$. This map simply extracts the underlying function from an $R$-linear map, preserving both addition and scalar multiplication.

LinearMap.ker_restrictScalars theorem

(f : M →ₗ[S] N) : LinearMap.ker (f.restrictScalars R) = (LinearMap.ker f).restrictScalars R

Full source

@[simp]
theorem LinearMap.ker_restrictScalars (f : M →ₗ[S] N) :
    LinearMap.ker (f.restrictScalars R) = (LinearMap.ker f).restrictScalars R :=
  rfl

Kernel Preservation Under Scalar Restriction for Linear Maps

Informal description

For any $S$-linear map $f \colon M \to N$ between modules over semirings $R$ and $S$ (with $R$ acting on $S$), the kernel of the scalar-restricted map $f \colon M \to N$ (viewed as an $R$-linear map) is equal to the scalar-restricted kernel of $f$ (viewed as an $S$-submodule). In symbols: \[ \ker(f_{\text{restrictScalars } R}) = (\ker f)_{\text{restrictScalars } R} \]

Invertible.algebraMapOfInvertibleAlgebraMap abbrev

(f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : Invertible (algebraMap R A r)) : Invertible (algebraMap R B r)

Full source

/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
invertible when `algebraMap R A r` is. -/
abbrev Invertible.algebraMapOfInvertibleAlgebraMap (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R}
    (h : Invertible (algebraMap R A r)) : Invertible (algebraMap R B r) where
  invOf := f ⅟(algebraMap R A r)
  invOf_mul_self := by rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def,
    mul_invOf_self, hf]
  mul_invOf_self := by rw [← Algebra.smul_def, ← map_smul, Algebra.smul_def, mul_invOf_self, hf]

Invertibility Preservation Under Linear Maps Preserving 1

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. Given a linear map $f \colon A \to B$ that preserves the multiplicative identity (i.e., $f(1) = 1$), if the algebra map $\text{algebraMap}_R A(r)$ is invertible for some $r \in R$, then $\text{algebraMap}_R B(r)$ is also invertible.

IsUnit.algebraMap_of_algebraMap theorem

(f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : IsUnit (algebraMap R A r)) : IsUnit (algebraMap R B r)

Full source

/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
a unit when `algebraMap R A r` is. -/
lemma IsUnit.algebraMap_of_algebraMap (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R}
    (h : IsUnit (algebraMap R A r)) : IsUnit (algebraMap R B r) :=
  let ⟨i⟩ := nonempty_invertible h
  letI := Invertible.algebraMapOfInvertibleAlgebraMap f hf i
  isUnit_of_invertible _

Unit Preservation Under Linear Maps Preserving 1

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. Given a linear map $f \colon A \to B$ such that $f(1) = 1$, if the algebra map $\text{algebraMap}_R A(r)$ is a unit for some $r \in R$, then $\text{algebraMap}_R B(r)$ is also a unit.

injective_algebraMap_of_linearMap theorem

(hb : Injective b) : Injective (algebraMap F E)

Full source

/-- If `E` is an `F`-algebra, and there exists an injective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also injective. -/
theorem injective_algebraMap_of_linearMap (hb : Injective b) :
    Injective (algebraMap F E) := fun x y e ↦ hb <| by
  rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]

Injectivity of algebra homomorphism induced by injective linear map

Informal description

Let $E$ be an $F$-algebra and $b \colon F \to E$ be an injective $F$-linear map. Then the algebra homomorphism $\text{algebraMap} \colon F \to E$ is also injective.

surjective_algebraMap_of_linearMap theorem

(hb : Surjective b) : Surjective (algebraMap F E)

Full source

/-- If `E` is an `F`-algebra, and there exists a surjective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also surjective. -/
theorem surjective_algebraMap_of_linearMap (hb : Surjective b) :
    Surjective (algebraMap F E) := fun x ↦ by
  obtain ⟨x, rfl⟩ := hb x
  obtain ⟨y, hy⟩ := hb (b 1 * b 1)
  refine ⟨x * y, ?_⟩
  obtain ⟨z, hz⟩ := hb 1
  apply_fun (x • z • ·) at hy
  rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy

Surjectivity of algebra map induced by a surjective linear map

Informal description

Let $E$ be an $F$-algebra, and let $b \colon F \to E$ be a surjective $F$-linear map. Then the algebra homomorphism $\text{algebraMap} \colon F \to E$ is also surjective.

bijective_algebraMap_of_linearMap theorem

(hb : Bijective b) : Bijective (algebraMap F E)

Full source

/-- If `E` is an `F`-algebra, and there exists a bijective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also bijective.

NOTE: The same result can also be obtained if there are two `F`-linear maps from `F` to `E`,
one is injective, the other one is surjective. In this case, use
`injective_algebraMap_of_linearMap` and `surjective_algebraMap_of_linearMap` separately. -/
theorem bijective_algebraMap_of_linearMap (hb : Bijective b) :
    Bijective (algebraMap F E) :=
  ⟨injective_algebraMap_of_linearMap b hb.1, surjective_algebraMap_of_linearMap b hb.2⟩

Bijectivity of algebra homomorphism induced by bijective linear map

Informal description

Let $E$ be an $F$-algebra and $b \colon F \to E$ be a bijective $F$-linear map. Then the algebra homomorphism $\text{algebraMap} \colon F \to E$ is also bijective.

bijective_algebraMap_of_linearEquiv theorem

(b : F ≃ₗ[F] E) : Bijective (algebraMap F E)

Full source

/-- If `E` is an `F`-algebra, there exists an `F`-linear isomorphism from `F` to `E` (namely,
`E` is a free `F`-module of rank one), then the algebra map from `F` to `E` is bijective. -/
theorem bijective_algebraMap_of_linearEquiv (b : F ≃ₗ[F] E) :
    Bijective (algebraMap F E) :=
  bijective_algebraMap_of_linearMap _ b.bijective

Bijectivity of Algebra Map via Linear Isomorphism

Informal description

Let $E$ be an $F$-algebra and suppose there exists an $F$-linear isomorphism $b \colon F \to E$. Then the algebra homomorphism $\text{algebraMap} \colon F \to E$ is bijective.

LinearMap.extendScalarsOfSurjectiveEquiv definition

(h : Surjective (algebraMap R S)) : (M →ₗ[R] N) ≃ₗ[R] (M →ₗ[S] N)

Full source

/-- If `R →+* S` is surjective, then `S`-linear maps between modules are exactly `R`-linear maps. -/
def LinearMap.extendScalarsOfSurjectiveEquiv (h : Surjective (algebraMap R S)) :
    (M →ₗ[R] N) ≃ₗ[R] (M →ₗ[S] N) where
  toFun f := { __ := f, map_smul' := fun r x ↦ by obtain ⟨r, rfl⟩ := h r; simp }
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun f := f.restrictScalars S
  left_inv _ := rfl
  right_inv _ := rfl

Linear equivalence between $R$-linear and $S$-linear maps via a surjective algebra map

Informal description

Given a surjective ring homomorphism $\text{algebraMap} \colon R \to S$, there is a linear equivalence between the space of $R$-linear maps $M \to N$ and the space of $S$-linear maps $M \to N$. More precisely, the equivalence is constructed as follows: - The forward map takes an $R$-linear map $f \colon M \to N$ and extends it to an $S$-linear map by defining its action on scalars via the surjection $R \to S$. - The inverse map restricts an $S$-linear map back to an $R$-linear map by composing with the algebra map $R \to S$. This equivalence preserves addition and scalar multiplication (with respect to $R$).

LinearMap.extendScalarsOfSurjective abbrev

(h : Surjective (algebraMap R S)) (l : M →ₗ[R] N) : M →ₗ[S] N

Full source

/-- If `R →+* S` is surjective, then `R`-linear maps are also `S`-linear. -/
abbrev LinearMap.extendScalarsOfSurjective (h : Surjective (algebraMap R S))
    (l : M →ₗ[R] N) : M →ₗ[S] N :=
  extendScalarsOfSurjectiveEquiv h l

Extension of scalars for linear maps via a surjective ring homomorphism

Informal description

Given a surjective ring homomorphism $\sigma \colon R \to S$ and an $R$-linear map $l \colon M \to N$ between $R$-modules $M$ and $N$, there exists an induced $S$-linear map $M \to N$ obtained by extending the scalars via $\sigma$.

LinearEquiv.extendScalarsOfSurjective definition

(h : Surjective (algebraMap R S)) (f : M ≃ₗ[R] N) : M ≃ₗ[S] N

Full source

/-- If `R →+* S` is surjective, then `R`-linear isomorphisms are also `S`-linear. -/
def LinearEquiv.extendScalarsOfSurjective (h : Surjective (algebraMap R S))
    (f : M ≃ₗ[R] N) : M ≃ₗ[S] N where
  __ := f
  map_smul' r x := by obtain ⟨r, rfl⟩ := h r; simp

Extension of scalars for linear equivalences via a surjective algebra map

Informal description

Given a surjective ring homomorphism $\text{algebraMap} \colon R \to S$ and an $R$-linear equivalence $f \colon M \simeq_R N$ between $R$-modules $M$ and $N$, there exists an induced $S$-linear equivalence $M \simeq_S N$.

LinearMap.extendScalarsOfSurjective_apply theorem

(l : M →ₗ[R] N) (x) : l.extendScalarsOfSurjective h x = l x

Full source

@[simp]
lemma LinearMap.extendScalarsOfSurjective_apply (l : M →ₗ[R] N) (x) :
    l.extendScalarsOfSurjective h x = l x := rfl

Extension of Scalars Preserves Action on Elements for Linear Maps

Informal description

Let $R$ and $S$ be semirings with a surjective ring homomorphism $\text{algebraMap} \colon R \to S$, and let $M$ and $N$ be $R$-modules. For any $R$-linear map $l \colon M \to N$, the extension of scalars $l \colon M \to_S N$ satisfies $l(x) = l(x)$ for all $x \in M$.

LinearEquiv.extendScalarsOfSurjective_apply theorem

(f : M ≃ₗ[R] N) (x) : f.extendScalarsOfSurjective h x = f x

Full source

@[simp]
lemma LinearEquiv.extendScalarsOfSurjective_apply (f : M ≃ₗ[R] N) (x) :
    f.extendScalarsOfSurjective h x = f x := rfl

Extension of Scalars Preserves Action on Elements

Informal description

Given a surjective ring homomorphism $\text{algebraMap} \colon R \to S$ and an $R$-linear equivalence $f \colon M \simeq_R N$ between $R$-modules $M$ and $N$, the extension of scalars $f \colon M \simeq_S N$ satisfies $f(x) = f(x)$ for all $x \in M$.

LinearEquiv.extendScalarsOfSurjective_symm theorem

(f : M ≃ₗ[R] N) : (f.extendScalarsOfSurjective h).symm = f.symm.extendScalarsOfSurjective h

Full source

@[simp]
lemma LinearEquiv.extendScalarsOfSurjective_symm (f : M ≃ₗ[R] N) :
    (f.extendScalarsOfSurjective h).symm = f.symm.extendScalarsOfSurjective h := rfl

Inverse of Extended Scalar Equivalence via Surjective Algebra Map

Informal description

Let $R$ and $S$ be semirings with a surjective ring homomorphism $\text{algebraMap} \colon R \to S$, and let $M$ and $N$ be $R$-modules. For any $R$-linear equivalence $f \colon M \simeq_R N$, the inverse of the extended $S$-linear equivalence $f.\text{extendScalarsOfSurjective}\, h$ is equal to the extension of the inverse equivalence $f^{-1}$ via $h$. That is, $$(f.\text{extendScalarsOfSurjective}\, h)^{-1} = f^{-1}.\text{extendScalarsOfSurjective}\, h.$$

algebraMap.coe_prod theorem

(a : ι → R) : (↑(∏ i ∈ s, a i : R) : A) = ∏ i ∈ s, (↑(a i) : A)

Full source

@[norm_cast]
theorem coe_prod (a : ι → R) : (↑(∏ i ∈ s, a i : R) : A) = ∏ i ∈ s, (↑(a i) : A) :=
  map_prod (algebraMap R A) a s

Algebra Map Preserves Finite Products: $\uparrow(\prod a_i) = \prod \uparrow(a_i)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any finite set $s$ and any function $a : \iota \to R$, the algebra map $\uparrow$ from $R$ to $A$ satisfies \[ \uparrow\left(\prod_{i \in s} a_i\right) = \prod_{i \in s} \uparrow(a_i). \]

algebraMap.coe_sum theorem

(a : ι → R) : ↑(∑ i ∈ s, a i) = ∑ i ∈ s, (↑(a i) : A)

Full source

@[norm_cast]
theorem coe_sum (a : ι → R) : ↑(∑ i ∈ s, a i) = ∑ i ∈ s, (↑(a i) : A) :=
  map_sum (algebraMap R A) a s

Algebra Map Preserves Finite Sums

Informal description

For any commutative semiring $R$ and any $R$-algebra $A$, the algebra map $R \to A$ preserves finite sums. Specifically, for any finite set $s$ and any function $a : \iota \to R$, the image of the sum $\sum_{i \in s} a_i$ under the algebra map equals the sum $\sum_{i \in s} (a_i : A)$ of the images in $A$.