RingHomSurjective.comp
theorem RingHomSurjective.comp :
∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
{σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[inst_4 : RingHomSurjective σ₁₂] [inst_5 : RingHomSurjective σ₂₃], RingHomSurjective σ₁₃
This theorem states that if we have three semirings `R₁`, `R₂`, and `R₃`, and we are given ring homomorphisms `σ₁₂ : R₁ →+* R₂` and `σ₂₃ : R₂ →+* R₃` such that they compose to `σ₁₃ : R₁ →+* R₃` (i.e., we have a `RingHomCompTriple σ₁₂ σ₂₃ σ₁₃`), and we know that `σ₁₂` and `σ₂₃` are surjective (i.e., for any element in the target ring, there is an element in the source ring that maps to it), then `σ₁₃` is also surjective. In other words, the composition of two surjective ring homomorphisms is always surjective.
More concisely: If `σ₁₂ : R₁ → R₂` and `σ₂₃ : R₂ → R₃` are surjective ring homomorphisms with `σ₁₃ := σ₁₂ ∘ σ₂₃` being their composition, then `σ₁₃` is also a surjective ring homomorphism.
|
RingHomCompTriple.comp_apply
theorem RingHomCompTriple.comp_apply :
∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
{σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {x : R₁},
σ₂₃ (σ₁₂ x) = σ₁₃ x
This theorem, "RingHomCompTriple.comp_apply", establishes that for any three semirings, R₁, R₂, and R₃, along with three ring homomorphisms σ₁₂ from R₁ to R₂, σ₂₃ from R₂ to R₃, and σ₁₃ from R₁ to R₃, if the three homomorphisms form a ring homomorphism composition triple, then for any element x in R₁, applying σ₂₃ to the result of applying σ₁₂ to x is equivalent to directly applying σ₁₃ to x. Essentially, this is showing a fundamental property of function composition in the context of ring homomorphisms.
More concisely: Given semirings R₁, R₂, R₃ and ring homomorphisms σ₁₂ : R₁ → R₂, σ₂₃ : R₂ → R₃, and σ₁₃ : R₁ → R₃, if σ₁₃ = σ₂₃ ∘ σ₁₂, then for all x in R₁, σ₂₃ (σ₁₂ x) = σ₁₃ x.
|
RingHomSurjective.is_surjective
theorem RingHomSurjective.is_surjective :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ : R₁ →+* R₂}
[self : RingHomSurjective σ], Function.Surjective ⇑σ
This theorem states that for any two types `R₁` and `R₂`, which have `Semiring` structures, any ring homomorphism `σ` from `R₁` to `R₂` that satisfies the `RingHomSurjective` property is a surjective function. In other words, for every element in the range `R₂`, there is an element in the domain `R₁` such that the ring homomorphism `σ` maps the domain element to the range element.
More concisely: Given any ring homomorphisms σ : R₁ → R₂ between semirings R₁ and R₂, if σ is surjective as a function then it is a surjective ring homomorphism.
|
RingHomCompTriple.comp_eq
theorem RingHomCompTriple.comp_eq :
∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
{σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : outParam (R₁ →+* R₃)} [self : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃],
σ₂₃.comp σ₁₂ = σ₁₃
This theorem states that in the context of semirings R₁, R₂, and R₃, and given ring homomorphisms σ₁₂ from R₁ to R₂, σ₂₃ from R₂ to R₃, and σ₁₃ from R₁ to R₃, if these morphisms form a commutative triangle (i.e., they satisfy the property of a `RingHomCompTriple`), then the composition of σ₂₃ and σ₁₂ equals to σ₁₃. In simpler terms, "going" from R₁ to R₃ directly via σ₁₃ is the same as first going from R₁ to R₂ via σ₁₂ and then from R₂ to R₃ via σ₂₃.
More concisely: Given semirings R₁, R₂, and R₃ and ring homomorphisms σ₁₂ : R₁ → R₂, σ₂₃ : R₂ → R₃, and σ₁₃ : R₁ → R₃ such that (σ₁₂ ∘ σ₂₃) = (σ₁₃), then σ₁₂ and σ₁₃ form a commutative triangle, that is, σ₂₃ ∘ σ₁₂ = σ₁₃.
|
RingHomInvPair.comp_eq₂
theorem RingHomInvPair.comp_eq₂ :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ : R₁ →+* R₂}
{σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'], σ.comp σ' = RingHom.id R₂
This theorem states that for any two types `R₁` and `R₂` that have the structure of a semiring, if we have a ring homomorphism `σ` from `R₁` to `R₂` and another ring homomorphism `σ'` from `R₂` to `R₁` such that `σ'` is a left inverse of `σ` (as indicated by the `RingHomInvPair` typeclass instance), then the composition of `σ` and `σ'` (that is, first applying `σ'` and then `σ`) is the identity on `R₂`. This is a formal way of expressing the concept that `σ'` "undoes" the action of `σ` on elements of the semiring `R₂`.
More concisely: If `σ:` `R₁` → `R₂` and `σ':` `R₂` → `R₁` are ring homomorphisms with `σ'` being a left inverse of `σ`, then `σ' ∘ σ = id R₂`, where `id R₂` is the identity function on `R₂`.
|
RingHomInvPair.comp_eq
theorem RingHomInvPair.comp_eq :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ : R₁ →+* R₂}
{σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'], RingHom.comp σ' σ = RingHom.id R₁
The theorem `RingHomInvPair.comp_eq` states that for any two types `R₁` and `R₂` with `Semiring` structures and any ring homomorphism `σ` from `R₁` to `R₂`, if `σ'` is a left inverse of `σ` (i.e., if `σ'` and `σ` form a `RingHomInvPair`), then the composition of `σ'` and `σ` (in that order) is the identity ring homomorphism on `R₁`. In other words, for all elements in `R₁`, applying `σ` followed by `σ'` brings us back to the original element.
More concisely: For any ring homomorphisms σ : R₁ → R₂ and σ' : R₂ → R₁ such that σ ∘ σ' = id\_{R₁}, the composition σ' ∘ σ = id\_{R₁}.
|
RingHomInvPair.of_ringEquiv
theorem RingHomInvPair.of_ringEquiv :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (e : R₁ ≃+* R₂),
RingHomInvPair ↑e ↑e.symm
The theorem `RingHomInvPair.of_ringEquiv` states that for any two types `R₁` and `R₂`, which are semirings, and given a ring isomorphism `e` from `R₁` to `R₂`, we can construct a `RingHomInvPair` from the ring isomorphism `e` and its inverse. Here, a `RingHomInvPair` is a pair of ring homomorphisms that are inverses of each other. This theorem is not an instance, meaning it does not provide a canonical way to construct a `RingHomInvPair` in all contexts. This is because, for ring isomorphisms that are also involutions (self-inverses), a better instance would be a pair consisting of the isomorphism and itself.
More concisely: Given a ring isomorphism between semirings with a inverse, there exists a pair of ring homomorphisms that are inverses of each other.
|
RingHomInvPair.symm
theorem RingHomInvPair.symm :
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁)
[inst_2 : RingHomInvPair σ₁₂ σ₂₁], RingHomInvPair σ₂₁ σ₁₂
This theorem, `RingHomInvPair.symm`, states that for any two types `R₁` and `R₂` (which are semirings), and given a pair of ring homomorphisms (`σ₁₂` and `σ₂₁`) that form a `RingHomInvPair` (meaning that applying `σ₁₂` followed by `σ₂₁` brings us back to the original element of `R₁` and the same for `R₂` with the order of operations reversed), we can swap the direction of this `RingHomInvPair`. In other words, if `σ₁₂` and `σ₂₁` form an inverse pair where `σ₁₂` is the forward direction and `σ₂₁` is the backward direction, then `σ₂₁` and `σ₁₂` also form an inverse pair, but with `σ₂₁` as the forward direction and `σ₁₂` as the backward direction.
More concisely: Given two semirings R₁ and R₂ and a pair of ring homomorphisms σ₁₂ : R₁ → R₂ and σ₂₁ : R₂ → R₁ forming a ring homeomorphism, the pair (σ₂₁, σ₁₂) is also a ring homeomorphism.
|