EllipticCurve.coe_Δ'
theorem EllipticCurve.coe_Δ' : ∀ {R : Type u} [inst : CommRing R] (self : EllipticCurve R), ↑self.Δ' = self.Δ := by
sorry
This theorem states that for any given elliptic curve `E` over a commutative ring `R`, the discriminant of `E` when casted (or converted) is equal to the discriminant of `E` as a Weierstrass curve. In mathematical terms, this theorem is ensuring that the discriminant of the elliptic curve remains the same even when it is expressed in different forms or representations, such as the Weierstrass form.
More concisely: The discriminant of an elliptic curve over a commutative ring is equal to its discriminant as a Weierstrass curve.
|
WeierstrassCurve.map_b₂
theorem WeierstrassCurve.map_b₂ :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (φ : R →+* A),
(W.map φ).b₂ = φ W.b₂
This theorem, `WeierstrassCurve.map_b₂`, states that for any type `R` that has a commutative ring structure, any Weierstrass curve `W` defined over `R`, any other type `A` also with a commutative ring structure, and any ring homomorphism `φ` from `R` to `A`, the `b₂` coefficient of the Weierstrass curve obtained by mapping `W` using `φ` is equal to the image under `φ` of the `b₂` coefficient of `W`. In mathematical terms, if `W` is a Weierstrass curve defined over a commutative ring `R` and `φ` is a ring homomorphism from `R` to another commutative ring `A`, then the `b₂` coefficient of the Weierstrass curve in `A` obtained by mapping `W` under `φ` is `φ(W.b₂)`.
More concisely: For any commutative rings R and A, any Weierstrass curve W over R, and any ring homomorphism φ from R to A, the `b₂` coefficient of the Weierstrass curve over A obtained by mapping W under φ is equal to φ(W.b₂).
|
WeierstrassCurve.map_baseChange
theorem WeierstrassCurve.map_baseChange :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {S : Type s} [inst_1 : CommRing S]
[inst_2 : Algebra R S] {A : Type v} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
[inst_6 : IsScalarTower R S A] {B : Type w} [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B]
[inst_10 : IsScalarTower R S B] (ψ : A →ₐ[S] B), (W.baseChange A).map ↑ψ = W.baseChange B
This theorem, known as `WeierstrassCurve.map_baseChange`, states that for any commutative rings `R`, `S`, `A`, and `B` such that `R` is an algebra over `S`, `A` is an algebra over `R`, and `B` is an algebra over `R` and `S` with `A` and `B` forming scalar towers with `R` and `S`, and for any Weierstrass curve `W` defined over `R`, and any algebra homomorphism `ψ` from `A` to `B` preserving the scalar multiplication by `S`, the base change of `W` to `A` followed by mapping via `ψ` is equal to the base change of `W` to `B`. In simpler terms, changing the base ring of the Weierstrass curve and then applying a map is the same as applying the map after changing the base ring.
More concisely: For any commutative rings R, S, A, B with R an algebra over S, A an algebra over R, B an algebra over R and S with A and B being scalar towers, and for any Weierstrass curve W over R and algebra homomorphism ψ from A to B preserving scalar multiplication by S, the base change of W from R to A then mapped via ψ equals the base change of W from R to B.
|
WeierstrassCurve.map_b₄
theorem WeierstrassCurve.map_b₄ :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (φ : R →+* A),
(W.map φ).b₄ = φ W.b₄
This theorem, named `WeierstrassCurve.map_b₄`, states that for any commutative ring `R`, any Weierstrass curve `W` defined over `R`, any type `A` with a commutative ring structure, and any morphism `φ` from `R` to `A`, the fourth coefficient `b₄` of the Weierstrass curve obtained by mapping `W` via `φ` is equal to the image under `φ` of the fourth coefficient `b₄` of `W`. In essence, this theorem shows how the fourth coefficient of a Weierstrass curve behaves under a ring homomorphism.
More concisely: For any Weierstrass curve `W` over a commutative ring `R`, and any ring homomorphism `φ` from `R` to a commutative ring `A`, the fourth coefficient of the Weierstrass curve `W` mapped via `φ` equals the image under `φ` of the fourth coefficient of `W`.
|