structure RingAntiHom (R : Type u_1) (S : Type u_2) [Ring R] [Ring S] : Type (max u_1 u_2)

A ring anti-homomorphism R → S: a map that preserves addition and the multiplicative identity, but reverses the order of multiplication, i.e. f (a * b) = f b * f a. Corresponds to Definition 12.1 of Sutherland's Elliptic Curves.

• toFun : R → S
• map_add (a b : R) : self.toFun (a + b) = self.toFun a + self.toFun b
• map_one : self.toFun 1 = 1
• map_mul_rev (a b : R) : self.toFun (a * b) = self.toFun b * self.toFun a

@[implicit_reducible]

instance RingAntiHom.instFunLike {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] : FunLike (RingAntiHom R S) R S

RingAntiHom R S is a FunLike type: it coerces to its underlying function and the coercion is injective.

@[simp]

theorem RingAntiHom.coe_mk {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R → S) (hadd : ∀ (a b : R), f (a + b) = f a + f b) (hone : f 1 = 1) (hmul : ∀ (a b : R), f (a * b) = f b * f a) : ⇑{ toFun := f, map_add := hadd, map_one := hone, map_mul_rev := hmul } = f

The coercion of an anti-homomorphism built via RingAntiHom.mk is its underlying function.

def RingAntiHom.ofRingHomToOp {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* Sᵐᵒᵖ) : RingAntiHom R S

Convert a ring homomorphism into the opposite ring R →+* Sᵐᵒᵖ to a ring anti-homomorphism R → S by post-composing with unop.

structure RingInvolution (R : Type u_1) [Ring R] extends RingAntiHom R R : Type u_1

A ring involution on R: a ring anti-homomorphism R → R that is its own inverse. This is the second half of Definition 12.1 in Sutherland's Elliptic Curves.

• toFun : R → R
• map_add (a b : R) : self.toFun (a + b) = self.toFun a + self.toFun b
• map_one : self.toFun 1 = 1
• map_mul_rev (a b : R) : self.toFun (a * b) = self.toFun b * self.toFun a
• involution (x : R) : self.toFun (self.toFun x) = x

@[implicit_reducible]

instance RingInvolution.instFunLike {R : Type u_1} [Ring R] : FunLike (RingInvolution R) R R

RingInvolution R is a FunLike type: it coerces to its underlying function and the coercion is injective.

theorem RingInvolution.map_mul_rev' {R : Type u_1} [Ring R] (φ : RingInvolution R) (a b : R) : φ (a * b) = φ b * φ a

A ring involution φ reverses multiplication: φ (a * b) = φ b * φ a.

theorem RingInvolution.map_one' {R : Type u_1} [Ring R] (φ : RingInvolution R) : φ 1 = 1

A ring involution sends 1 to 1.

theorem RingInvolution.map_add' {R : Type u_1} [Ring R] (φ : RingInvolution R) (a b : R) : φ (a + b) = φ a + φ b

A ring involution preserves addition.

theorem RingInvolution.bijective {R : Type u_1} [Ring R] (φ : RingInvolution R) : Function.Bijective φ.toFun

A ring involution is bijective; its inverse is itself.

def RingInvolution.ofRingInvo {R : Type u_1} [Ring R] (f : RingInvo R) : RingInvolution R

Convert Mathlib's RingInvo R (a ring involution as a R →+* Rᵐᵒᵖ) to a RingInvolution R.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Affine.EndomorphismAlgebra {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : Type u

The endomorphism algebra of an elliptic curve E, defined as End(E) ⊗_ℤ ℚ. This realises Definition 12.2 of Sutherland's Elliptic Curves: End^0(E) := End(E) ⊗_ℤ ℚ.

@[implicit_reducible]

noncomputable instance WeierstrassCurve.Affine.EndomorphismAlgebra.instRing {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : Ring E.EndomorphismAlgebra

The endomorphism algebra End(E) ⊗_ℤ ℚ inherits a ring structure from the tensor product of rings.

@[implicit_reducible]

noncomputable instance WeierstrassCurve.Affine.EndomorphismAlgebra.instAlgebra {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : Algebra ℚ E.EndomorphismAlgebra

The endomorphism algebra End(E) ⊗_ℤ ℚ is naturally a ℚ-algebra via the right tensor factor.

noncomputable def WeierstrassCurve.Affine.EndomorphismAlgebra.ofEndRing {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : EndRing E →+* E.EndomorphismAlgebra

The canonical ring homomorphism End(E) → End(E) ⊗_ℤ ℚ sending an endomorphism α to α ⊗ 1.

@[implicit_reducible]

noncomputable instance WeierstrassCurve.Affine.EndomorphismAlgebra.instAlgebraInt {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : Algebra ℤ E.EndomorphismAlgebra

The endomorphism algebra also inherits a ℤ-algebra structure.

@[implicit_reducible]

noncomputable instance WeierstrassCurve.Affine.EndomorphismAlgebra.instModule {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : Module ℚ E.EndomorphismAlgebra

The endomorphism algebra is a ℚ-module via its ℚ-algebra structure.

noncomputable def WeierstrassCurve.Affine.EndomorphismAlgebra.ofRat {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : ℚ →+* E.EndomorphismAlgebra

The canonical ring homomorphism ℚ → End(E) ⊗_ℤ ℚ, given by the ℚ-algebra map.

@[implicit_reducible]

noncomputable instance WeierstrassCurve.Affine.EndomorphismAlgebra.instAddCommGroup {F : Type u} [Field F] [DecidableEq F] (E : Affine F) : AddCommGroup E.EndomorphismAlgebra

The additive group structure on the endomorphism algebra, inherited from its ring structure.