Documentation

Atlas.EllipticCurves.code.ComplexMultiplication

The endomorphism ring $\mathrm{End}(L)$ of a complex lattice $L$ is the subring of $\mathbb{C}$ consisting of all $\alpha \in \mathbb{C}$ such that $\alpha L \subseteq L$. Equivalently, an element $\alpha$ lies in $\mathrm{End}(L)$ iff multiplication by $\alpha$ preserves the additive subgroup underlying $L$.

Instances For
    @[simp]

    Characterization of membership in the endomorphism ring: $\alpha \in \mathrm{End}(L)$ iff $\alpha \cdot z \in L$ for every $z \in L$.

    A complex lattice $L$ is a proper $\mathcal{O}$-ideal if its endomorphism ring equals $\mathcal{O}$ exactly (not just contains $\mathcal{O}$). This is the standard notion of proper ideal in the theory of orders in imaginary quadratic fields.

    Instances For

      Two proper $\mathcal{O}$-ideals $L_1$ and $L_2$ are equivalent if there exist nonzero $\alpha, \beta \in \mathcal{O}$ with $\alpha L_1 = \beta L_2$ as subsets of $\mathbb{C}$. This is the equivalence relation whose classes form the ideal class group of $\mathcal{O}$.

      Instances For

        Reflexivity of ideal equivalence: every lattice is equivalent to itself (witnessed by $\alpha = \beta = 1$).

        theorem ComplexLattice.IsEquivalent.symm {𝒪 : Subring } {L₁ L₂ : ComplexLattice} (h : IsEquivalent 𝒪 L₁ L₂) :
        IsEquivalent 𝒪 L₂ L₁

        Symmetry of ideal equivalence: if $\alpha L_1 = \beta L_2$, then $\beta L_2 = \alpha L_1$ (with the roles of $\alpha$ and $\beta$ swapped).

        theorem ComplexLattice.IsEquivalent.trans {𝒪 : Subring } {L₁ L₂ L₃ : ComplexLattice} (h₁₂ : IsEquivalent 𝒪 L₁ L₂) (h₂₃ : IsEquivalent 𝒪 L₂ L₃) :
        IsEquivalent 𝒪 L₁ L₃

        Transitivity of ideal equivalence: if $\alpha_1 L_1 = \beta_1 L_2$ and $\alpha_2 L_2 = \beta_2 L_3$, then $(\alpha_2\alpha_1) L_1 = (\beta_1\beta_2) L_3$.

        The relation IsEquivalent 𝒪 is an equivalence relation on complex lattices.

        theorem ComplexLattice.IsEquivalent.isHomothetic {𝒪 : Subring } {L₁ L₂ : ComplexLattice} (h : IsEquivalent 𝒪 L₁ L₂) :
        L₁.IsHomothetic L₂

        Ideal equivalence implies homothety: if $\alpha L_1 = \beta L_2$, then $L_2 = (\beta^{-1}\alpha) L_1$, so the lattices are homothetic with factor $\beta^{-1}\alpha$.

        The type of proper $\mathcal{O}$-ideals: pairs $(L, \mathrm{proof})$ where $L$ is a complex lattice, $L$ is a proper $\mathcal{O}$-ideal (its endomorphism ring equals $\mathcal{O}$), and $L$ is contained in $\mathcal{O}$ as a subset of $\mathbb{C}$.

        Instances For

          The setoid structure on proper $\mathcal{O}$-ideals induced by ideal equivalence; the quotient is the ideal class group of $\mathcal{O}$.

          Instances For

            The ideal class group $\mathrm{Cl}(\mathcal{O})$ of an order $\mathcal{O}$: the quotient of proper $\mathcal{O}$-ideals by the equivalence relation of being equal up to scaling by nonzero elements of $\mathcal{O}$. It is a finite abelian group whose order is the class number $h(\mathcal{O})$.

            Instances For

              The class of a proper $\mathcal{O}$-ideal in the ideal class group.

              Instances For
                theorem ComplexLattice.IdealClassGroup.mk_eq_mk_iff (𝒪 : Subring ) (L₁ L₂ : ProperIdeal 𝒪) :
                mk 𝒪 L₁ = mk 𝒪 L₂ IsEquivalent 𝒪 L₁ L₂

                Two proper ideals define the same class in $\mathrm{Cl}(\mathcal{O})$ iff they are equivalent as ideals.

                def ComplexLattice.ProperIdeal.mul (𝒪 : Subring ) (𝔞 𝔟 : ProperIdeal 𝒪) :

                The product of two proper $\mathcal{O}$-ideals: given $\mathfrak{a}$ with period pair $(\omega_1, \omega_2)$ and $\mathfrak{b}$ with period pair $(\omega_1', \omega_2')$, the product is the lattice with period pair $(\omega_1\omega_1', \omega_1\omega_2')$. The result is again a proper $\mathcal{O}$-ideal.

                Instances For

                  The subring $\mathcal{O} \subseteq \mathbb{C}$ viewed as a complex lattice, when $\mathcal{O}$ is an order in an imaginary quadratic field. This is the lattice underlying the unit ideal $\mathcal{O}$ itself.

                  Instances For

                    The underlying set of subringAsComplexLattice 𝒪 coincides with the set of elements of $\mathcal{O}$.

                    The endomorphism ring of $\mathcal{O}$ (viewed as a lattice) equals $\mathcal{O}$ itself, so $\mathcal{O}$ is a proper ideal of itself.

                    noncomputable def ComplexLattice.ProperIdeal.one (𝒪 : Subring ) :

                    The unit element of the ideal class group: the proper $\mathcal{O}$-ideal $\mathcal{O}$ itself.

                    Instances For
                      theorem ComplexLattice.conjugateScaledLattice_isProperIdeal (𝒪 : Subring ) (𝔞 : ProperIdeal 𝒪) (Linv : ComplexLattice) (hω₁ : Linv.ω₁ = (starRingEnd ) (↑𝔞).ω₁ / (Complex.normSq (↑𝔞).ω₁)) (hω₂ : Linv.ω₂ = (starRingEnd ) (↑𝔞).ω₂ / (Complex.normSq (↑𝔞).ω₁)) :
                      IsProperIdeal 𝒪 Linv

                      If $L_{\mathrm{inv}}$ has period pair $(\bar\omega_1/N(\omega_1), \bar\omega_2/N(\omega_1))$ for a proper $\mathcal{O}$-ideal $\mathfrak{a}$, then $L_{\mathrm{inv}}$ is again a proper $\mathcal{O}$-ideal. This is the construction of the inverse ideal in the ideal class group.

                      theorem ComplexLattice.conjugateScaledLattice_subset_order (𝒪 : Subring ) (𝔞 : ProperIdeal 𝒪) (Linv : ComplexLattice) (hω₁ : Linv.ω₁ = (starRingEnd ) (↑𝔞).ω₁ / (Complex.normSq (↑𝔞).ω₁)) (hω₂ : Linv.ω₂ = (starRingEnd ) (↑𝔞).ω₂ / (Complex.normSq (↑𝔞).ω₁)) (z : ) :
                      z Linv.toAddSubgroupz 𝒪

                      The conjugate-scaled lattice $L_{\mathrm{inv}}$ is contained in $\mathcal{O}$; together with conjugateScaledLattice_isProperIdeal this shows that it qualifies as a proper $\mathcal{O}$-ideal.

                      noncomputable def ComplexLattice.ProperIdeal.inv (𝒪 : Subring ) (𝔞 : ProperIdeal 𝒪) :

                      The inverse of a proper $\mathcal{O}$-ideal $\mathfrak{a}$ with period pair $(\omega_1, \omega_2)$: the proper $\mathcal{O}$-ideal with period pair $(\bar\omega_1/N(\omega_1), \bar\omega_2/N(\omega_1))$, which represents the inverse class in $\mathrm{Cl}(\mathcal{O})$.

                      Instances For
                        theorem ComplexLattice.ProperIdeal.mul_equiv_snd (𝒪 : Subring ) (a b : ProperIdeal 𝒪) :
                        IsEquivalent 𝒪 (mul 𝒪 a b) b

                        For any proper $\mathcal{O}$-ideals $\mathfrak{a}, \mathfrak{b}$, the product $\mathfrak{a}\mathfrak{b}$ is equivalent to $\mathfrak{b}$ in the ideal class group; this is the homothety $\mathfrak{a}\mathfrak{b} = \omega_1(\mathfrak{a}) \cdot \mathfrak{b}$ underlying the definition.

                        theorem ComplexLattice.ProperIdeal.mul_resp (𝒪 : Subring ) (a₁ a₂ b₁ b₂ : ProperIdeal 𝒪) :
                        (properIdealSetoid 𝒪) a₁ a₂(properIdealSetoid 𝒪) b₁ b₂(properIdealSetoid 𝒪) (mul 𝒪 a₁ b₁) (mul 𝒪 a₂ b₂)

                        Ideal multiplication respects the equivalence relation: if $\mathfrak{a}_1 \sim \mathfrak{a}_2$ and $\mathfrak{b}_1 \sim \mathfrak{b}_2$, then $\mathfrak{a}_1\mathfrak{b}_1 \sim \mathfrak{a}_2\mathfrak{b}_2$. This makes ideal multiplication well-defined on class group elements.

                        theorem ComplexLattice.ProperIdeal.mul_assoc_equiv (𝒪 : Subring ) (a b c : ProperIdeal 𝒪) :
                        (properIdealSetoid 𝒪) (mul 𝒪 (mul 𝒪 a b) c) (mul 𝒪 a (mul 𝒪 b c))

                        Associativity of ideal multiplication up to equivalence: $(\mathfrak{a}\mathfrak{b}) \mathfrak{c} \sim \mathfrak{a}(\mathfrak{b}\mathfrak{c})$.

                        theorem ComplexLattice.ProperIdeal.mul_comm_equiv (𝒪 : Subring ) (a b : ProperIdeal 𝒪) :
                        (properIdealSetoid 𝒪) (mul 𝒪 a b) (mul 𝒪 b a)

                        Commutativity of ideal multiplication up to equivalence: $\mathfrak{a}\mathfrak{b} \sim \mathfrak{b}\mathfrak{a}$.

                        theorem ComplexLattice.ProperIdeal.one_mul_equiv (𝒪 : Subring ) (a : ProperIdeal 𝒪) :
                        (properIdealSetoid 𝒪) (mul 𝒪 (one 𝒪) a) a

                        Left identity for ideal multiplication up to equivalence: $\mathcal{O} \cdot \mathfrak{a} \sim \mathfrak{a}$.

                        theorem ComplexLattice.ProperIdeal.inv_mul_equiv (𝒪 : Subring ) (a : ProperIdeal 𝒪) :
                        (properIdealSetoid 𝒪) (mul 𝒪 (inv 𝒪 a) a) (one 𝒪)

                        Inverse property for ideal multiplication up to equivalence: $\mathfrak{a}^{-1} \cdot \mathfrak{a} \sim \mathcal{O}$.

                        theorem ComplexLattice.ProperIdeal.inv_resp (𝒪 : Subring ) (a₁ a₂ : ProperIdeal 𝒪) :
                        (properIdealSetoid 𝒪) a₁ a₂(properIdealSetoid 𝒪) (inv 𝒪 a₁) (inv 𝒪 a₂)

                        Ideal inversion respects the equivalence relation: equivalent ideals have equivalent inverses. This makes inversion well-defined on class group elements.

                        @[reducible]

                        The commutative group structure on the ideal class group $\mathrm{Cl}(\mathcal{O})$. Multiplication, identity, and inversion are induced from the corresponding operations on proper $\mathcal{O}$-ideals via the quotient by ideal equivalence.

                        Instances For
                          theorem ComplexLattice.ProperIdeal.finite_representatives (𝒪 : Subring ) :
                          ∃ (n : ) (f : Fin nProperIdeal 𝒪), ∀ (x : IdealClassGroup 𝒪), ∃ (i : Fin n), IdealClassGroup.mk 𝒪 (f i) = x

                          Finiteness of the ideal class group: there exist finitely many proper ideal representatives that surject onto $\mathrm{Cl}(\mathcal{O})$. This is the classical finiteness theorem for orders in imaginary quadratic fields.

                          The ideal class group $\mathrm{Cl}(\mathcal{O})$ is a finite type.

                          noncomputable def ComplexLattice.classNumber (𝒪 : Subring ) :

                          The class number $h(\mathcal{O}) = |\mathrm{Cl}(\mathcal{O})|$ of an order $\mathcal{O}$.

                          Instances For

                            A subring $\mathcal{O} \subseteq \mathbb{C}$ is an order in an imaginary quadratic field if it contains some non-integer element $\tau$ that satisfies a monic integer quadratic polynomial $\tau^2 + b\tau + c = 0$ with negative discriminant $b^2 - 4c < 0$.

                            Instances For

                              The setoid structure on proper $\mathcal{O}$-ideals induced by homothety: two proper ideals are identified if one is a complex scalar multiple of the other.

                              Instances For

                                The set of homothety classes of proper $\mathcal{O}$-ideals. When $\mathcal{O}$ is an order in an imaginary quadratic field, this set is in canonical bijection with the ideal class group $\mathrm{Cl}(\mathcal{O})$.

                                Instances For
                                  theorem ComplexLattice.lattice_subset_of_isImagQuadOrder (𝒪 : Subring ) (h𝒪 : IsImagQuadOrder 𝒪) (L : ProperIdeal 𝒪) (z : ) (hz : z (↑L).toAddSubgroup) :
                                  z 𝒪

                                  A proper $\mathcal{O}$-ideal is contained in $\mathcal{O}$: every element of the lattice underlying a proper ideal lies in $\mathcal{O}$.

                                  theorem ComplexLattice.omega1_mem_of_isImagQuadOrder (𝒪 : Subring ) (h𝒪 : IsImagQuadOrder 𝒪) (L : ProperIdeal 𝒪) :
                                  (↑L).ω₁ 𝒪

                                  The first basis vector $\omega_1$ of a proper $\mathcal{O}$-ideal lies in $\mathcal{O}$.

                                  theorem ComplexLattice.lambda_omega1_mem_of_isImagQuadOrder (𝒪 : Subring ) (h𝒪 : IsImagQuadOrder 𝒪) (L₁ L₂ : ProperIdeal 𝒪) (c : ) (hc : c 0) (hL : (PeriodPair.lattice L₂) = c (PeriodPair.lattice L₁)) :
                                  c * (↑L₁).ω₁ 𝒪

                                  If $L_2 = c \cdot L_1$ (homothety) with $c \neq 0$ and both are proper $\mathcal{O}$-ideals, then $c \omega_1(L_1) \in \mathcal{O}$.

                                  theorem ComplexLattice.isEquivalent_of_isHomothetic_properIdeal (𝒪 : Subring ) (h𝒪 : IsImagQuadOrder 𝒪) (L₁ L₂ : ProperIdeal 𝒪) (h : (↑L₁).IsHomothetic L₂) :
                                  IsEquivalent 𝒪 L₁ L₂

                                  For proper ideals of an imaginary-quadratic order, homothety implies ideal equivalence. Combined with the converse IsEquivalent.isHomothetic, this means the two notions of equivalence coincide for proper ideals.

                                  theorem ComplexLattice.isEquivalent_iff_isHomothetic_properIdeal (𝒪 : Subring ) (h𝒪 : IsImagQuadOrder 𝒪) (L₁ L₂ : ProperIdeal 𝒪) :
                                  IsEquivalent 𝒪 L₁ L₂ (↑L₁).IsHomothetic L₂

                                  For proper ideals of an order in an imaginary quadratic field, ideal equivalence and homothety are equivalent notions.

                                  For an order $\mathcal{O}$ in an imaginary quadratic field, the ideal class group is in canonical bijection with the set of homothety classes of proper $\mathcal{O}$-ideals.

                                  Instances For

                                    The endomorphism ring $\mathrm{End}(L)$ of any complex lattice $L$ is commutative, since it is a subring of $\mathbb{C}$.

                                    Classification of endomorphism rings (Theorem 12.17): the endomorphism ring of any complex lattice $L$ is either isomorphic to $\mathbb{Z}$ (constructor isZ), or is an order in an imaginary quadratic field (constructor isOrderInImagQuadField), in which case $L$ embeds into that order via $\alpha \mapsto \alpha\omega_1$.

                                    Instances For

                                      A complex lattice $L$ has complex multiplication iff its endomorphism ring contains some non-integer element (i.e. is strictly larger than $\mathbb{Z}$).

                                      Instances For

                                        Every integer $n \in \mathbb{Z}$ acts on $L$ by multiplication, so $\mathbb{Z} \subseteq \mathrm{End}(L)$ for any complex lattice $L$.

                                        theorem ComplexLattice.endomorphismRing_charPoly (L : ComplexLattice) (τ : ) (hτ_mem : τ L.endomorphismRing) (hτ_not_int : ∀ (n : ), τ n) (a b c d : ) (hab : a * L.ω₁ + b * L.ω₂ = τ * L.ω₁) (hcd : c * L.ω₁ + d * L.ω₂ = τ * L.ω₂) :
                                        τ * τ + ↑(-(a + d)) * τ + ↑(a * d - b * c) = 0

                                        Every $\tau \in \mathrm{End}(L)$ satisfies the characteristic polynomial $\tau^2 - (a+d)\tau + (ad - bc) = 0$ where $\begin{pmatrix}a & b\\c & d\end{pmatrix}$ is the matrix representation of $\tau$ acting on the lattice basis $(\omega_1, \omega_2)$.

                                        theorem ComplexLattice.endomorphismRing_negDisc (L : ComplexLattice) (τ : ) (hτ_mem : τ L.endomorphismRing) (hτ_not_int : ∀ (n : ), τ n) (a b c d : ) (hab : a * L.ω₁ + b * L.ω₂ = τ * L.ω₁) (hcd : c * L.ω₁ + d * L.ω₂ = τ * L.ω₂) :
                                        -(a + d) * -(a + d) - 4 * (a * d - b * c) < 0

                                        The discriminant $(a + d)^2 - 4(ad - bc) = (\mathrm{tr}\,\tau)^2 - 4\det\tau$ of the characteristic polynomial of $\tau \in \mathrm{End}(L) \setminus \mathbb{Z}$ is negative. Hence $\tau$ generates an imaginary quadratic extension of $\mathbb{Q}$.

                                        theorem ComplexLattice.endomorphismRing_order_witness (L : ComplexLattice) (τ : ) (hτ_mem : τ L.endomorphismRing) (hτ_not_int : ∀ (n : ), τ n) :
                                        τ'L.endomorphismRing, (∀ (n : ), τ' n) ∃ (b : ) (c : ), τ' * τ' + b * τ' + c = 0 b * b - 4 * c < 0

                                        Order witness: if $\tau \in \mathrm{End}(L)$ is not an integer, then there exists an element of $\mathrm{End}(L)$ (namely $\tau$ itself) satisfying a monic integer quadratic polynomial with negative discriminant. This shows that $\mathrm{End}(L)$ is an order in an imaginary quadratic field.

                                        Theorem 12.17 (classification of endomorphism rings): for every complex lattice $L$, either $\mathrm{End}(L) \cong \mathbb{Z}$ or $\mathrm{End}(L)$ is an order in an imaginary quadratic field.

                                        Combined statement of Theorem 12.17: $\mathrm{End}(L)$ is commutative and is either $\mathbb{Z}$ or an order in an imaginary quadratic field.

                                        Zero belongs to the lattice multiplier set $\{\alpha \in \mathbb{C} : \alpha L_1 \subseteq L_2\}$.

                                        theorem ComplexLattice.latticeMulSet_add_mem (L₁ L₂ : ComplexLattice) {α β : } ( : α L₁.latticeMulSet L₂) ( : β L₁.latticeMulSet L₂) :
                                        α + β L₁.latticeMulSet L₂

                                        The lattice multiplier set is closed under addition: if $\alpha L_1, \beta L_1 \subseteq L_2$, then $(\alpha + \beta) L_1 \subseteq L_2$.

                                        theorem ComplexLattice.latticeMulSet_neg_mem (L₁ L₂ : ComplexLattice) {α : } ( : α L₁.latticeMulSet L₂) :
                                        -α L₁.latticeMulSet L₂

                                        The lattice multiplier set is closed under negation: if $\alpha L_1 \subseteq L_2$, then $-\alpha \cdot L_1 \subseteq L_2$.

                                        The lattice multiplier set $\{\alpha : \alpha L_1 \subseteq L_2\}$ packaged as an additive subgroup of $\mathbb{C}$.

                                        Instances For
                                          theorem ComplexLattice.inducedMap_add (L₁ L₂ : ComplexLattice) (α β : ) ( : α L₁.latticeMulSet L₂) ( : β L₁.latticeMulSet L₂) (x : L₁.torusQuot) :
                                          (L₁.inducedMap L₂ (α + β) ) x = (L₁.inducedMap L₂ α ) x + (L₁.inducedMap L₂ β ) x

                                          The induced map between complex tori is additive in the multiplier: the map induced by $\alpha + \beta$ equals the sum of the maps induced by $\alpha$ and $\beta$ separately.

                                          theorem ComplexLattice.corollary_16_2_surj (L₁ L₂ : ComplexLattice) (φ : L₁.ComplexTorusHolMap L₂) (hφ0 : φ.toFun 0 = 0) :
                                          ∃ (α : ) ( : α L₁.latticeMulSet L₂), ∀ (z : ), φ.toFun (L₁.proj z) = (L₁.inducedMap L₂ α ) (L₁.proj z)

                                          Corollary 16.2, surjectivity part: every holomorphic map of complex tori sending $0$ to $0$ is induced by some multiplier $\alpha \in \mathbb{C}$ with $\alpha L_1 \subseteq L_2$.

                                          theorem ComplexLattice.corollary_16_2_inj (L₁ L₂ : ComplexLattice) (α γ : ) ( : α L₁.latticeMulSet L₂) ( : γ L₁.latticeMulSet L₂) (heq : ∀ (z : ), (L₁.inducedMap L₂ α ) (L₁.proj z) = (L₁.inducedMap L₂ γ ) (L₁.proj z)) :
                                          α = γ

                                          Corollary 16.2, injectivity part: the multiplier $\alpha$ inducing a given holomorphic map of complex tori is uniquely determined.

                                          theorem ComplexLattice.corollary_16_2 (L₁ L₂ : ComplexLattice) :
                                          (∀ (φ : L₁.ComplexTorusHolMap L₂), φ.toFun 0 = 0∃ (α : ) ( : α L₁.latticeMulSet L₂), ∀ (z : ), φ.toFun (L₁.proj z) = (L₁.inducedMap L₂ α ) (L₁.proj z)) (∀ (α γ : ) ( : α L₁.latticeMulSet L₂) ( : γ L₁.latticeMulSet L₂), (∀ (z : ), (L₁.inducedMap L₂ α ) (L₁.proj z) = (L₁.inducedMap L₂ γ ) (L₁.proj z))α = γ) ∀ (α β : ) ( : α L₁.latticeMulSet L₂) ( : β L₁.latticeMulSet L₂) (x : L₁.torusQuot), (L₁.inducedMap L₂ (α + β) ) x = (L₁.inducedMap L₂ α ) x + (L₁.inducedMap L₂ β ) x

                                          Corollary 16.2 (combined): the set of holomorphic torus maps $L_1 \to L_2$ sending $0$ to $0$ is in additive bijection with the multiplier set $\{\alpha : \alpha L_1 \subseteq L_2\}$.

                                          A function $f : \mathbb{C} \to \mathbb{C}$ is even iff $f(-z) = f(z)$ for all $z$.

                                          Instances For
                                            theorem ComplexLattice.meromorphic_comp_neg {f : } (hf : Meromorphic f) :
                                            Meromorphic fun (z : ) => f (-z)

                                            The composition $z \mapsto f(-z)$ of a meromorphic function with negation is again meromorphic.

                                            theorem ComplexLattice.latticePeriodic_neg_of_latticePeriodic (L : ComplexLattice) {f : } (hper : L.IsLatticePeriodic f) (ω : ) :
                                            ω PeriodPair.lattice L∀ (z : ), f (-(z + ω)) = f (-z)

                                            If $f$ is $L$-periodic, then so is $z \mapsto f(-z)$.

                                            theorem ComplexLattice.even_part_isEllipticFunction (L : ComplexLattice) {f : } (hf : L.IsEllipticFunction f) :
                                            L.IsEllipticFunction fun (z : ) => (f z + f (-z)) / 2

                                            The even part $f_+(z) = \tfrac{1}{2}(f(z) + f(-z))$ of an elliptic function $f$ is again an elliptic function.

                                            theorem ComplexLattice.even_part_isEvenFunction (f : ) :
                                            IsEvenFunction fun (z : ) => (f z + f (-z)) / 2

                                            The even part $f_+ = \tfrac{1}{2}(f + f \circ (-\mathrm{id}))$ is indeed an even function.

                                            The odd-part quotient $\tfrac{f(z) - f(-z)}{2 \wp'(z)}$ is an elliptic function: since both the odd part of $f$ and $\wp'$ are odd elliptic functions, their ratio is an even elliptic function.

                                            The odd-part quotient $\tfrac{f(z) - f(-z)}{2\wp'(z)}$ is an even function.

                                            theorem ComplexLattice.even_holomorphic_elliptic_is_polynomial_in_wp (L : ComplexLattice) (f : ) (hf_ell : L.IsEllipticFunction f) (hf_even : IsEvenFunction f) (hf_holo : z(PeriodPair.lattice L), DifferentiableAt f z) :
                                            ∃ (P : Polynomial ), ∀ (z : ), f z = Polynomial.eval (PeriodPair.weierstrassP L z) P

                                            Even holomorphic elliptic functions are polynomials in $\wp$: if $f$ is an even, $L$-periodic, meromorphic function with no poles outside $L$, then $f(z) = P(\wp(z))$ for some polynomial $P \in \mathbb{C}[X]$.

                                            Even elliptic functions are rational functions in $\wp$: if $f$ is an even elliptic function, then there exist polynomials $P, Q \in \mathbb{C}[X]$ with $Q \neq 0$ such that $Q(\wp(z)) f(z) = P(\wp(z))$, i.e.\ $f = P(\wp)/Q(\wp)$.

                                            At a zero of $\wp'$, the odd part of an elliptic function $f$ vanishes: if $\wp'(z) = 0$ then $f(z) = f(-z)$. This is needed for the rational expression of arbitrary elliptic functions in $\wp$ and $\wp'$.

                                            Assembly lemma for Lemma 16.3(i): given rational expressions for the even part of $f$ (via $P_e, Q_e$) and for the odd-part quotient $\tfrac{f - f(-\cdot)}{2\wp'}$ (via $P_o, Q_o$), one assembles a rational expression $f = (Q_o P_e + Q_e P_o \wp') / (Q_e Q_o)$ in $\wp$ and $\wp'$.

                                            Theorem: the field of elliptic functions for $L$ equals $\mathbb{C}(\wp, \wp')$. Every elliptic function $f$ can be expressed as $f(z) = (P_1(\wp(z)) + P_2(\wp(z)) \wp'(z)) / Q(\wp(z))$ for polynomials $P_1, P_2, Q \in \mathbb{C}[X]$ with $Q \neq 0$.

                                            $\wp_{L_2}(\alpha z)$ is a rational function in $\wp_{L_1}(z)$: there exist polynomials $u, v$ with $v \neq 0$ such that $v(\wp_{L_1}(z)) \wp_{L_2}(\alpha z) = u(\wp_{L_1}(z))$. Condition (2) of Theorem 16.4.

                                            Instances For

                                              The "isogeny" associated to $\alpha$ exists at the level of $\wp$-functions and their derivatives: both $\wp_{L_2}(\alpha z)$ and $\wp'_{L_2}(\alpha z)$ can be expressed rationally in $\wp_{L_1}$ and $\wp'_{L_1}$. Condition (3) of Theorem 16.4.

                                              Instances For
                                                theorem ComplexLattice.theorem_16_4_one_imp_two (L₁ L₂ : ComplexLattice) (α : ) ( : α L₁.latticeMulSet L₂) :

                                                Theorem 16.4: (1) $\Rightarrow$ (2). If $\alpha L_1 \subseteq L_2$, then $\wp_{L_2}(\alpha z)$ is a rational function in $\wp_{L_1}(z)$.

                                                Theorem 16.4: (2) $\Rightarrow$ (3). If $\wp_{L_2}(\alpha z)$ is rational in $\wp_{L_1}$, then both $\wp_{L_2}(\alpha z)$ and $\wp'_{L_2}(\alpha z)$ have the required rational expressions, giving an isogeny.

                                                Theorem 16.4: (3) $\Rightarrow$ (1). Existence of the rational isogeny formulae for $\alpha$ forces $\alpha L_1 \subseteq L_2$.

                                                theorem ComplexLattice.theorem_16_4 (L₁ L₂ : ComplexLattice) (α : ) :

                                                Theorem 16.4. The following are equivalent: (1) $\alpha L_1 \subseteq L_2$; (2) $\wp_{L_2}(\alpha z)$ is a rational function in $\wp_{L_1}(z)$; (3) the unique isogeny induced by $\alpha$ exists (i.e.\ both $\wp_{L_2}(\alpha z)$ and $\wp'_{L_2}(\alpha z)$ admit rational expressions in $\wp_{L_1}$ and $\wp'_{L_1}$).

                                                theorem ComplexLattice.poleOrder_deg_relation (L₁ L₂ : ComplexLattice) (α : ) ( : α L₁.latticeMulSet L₂) (hα0 : α 0) (u v : Polynomial ) (hv : v 0) (h : ∀ (z : ), Polynomial.eval (PeriodPair.weierstrassP L₁ z) v * PeriodPair.weierstrassP L₂ (α * z) = Polynomial.eval (PeriodPair.weierstrassP L₁ z) u) :

                                                Degree relation: if $v(\wp_{L_1}(z)) \wp_{L_2}(\alpha z) = u(\wp_{L_1}(z))$ expresses the isogeny induced by $\alpha$, then $\deg u = \deg v + 1$.

                                                theorem ComplexLattice.normSq_eq_natDegree (L : ComplexLattice) (α : ) ( : α L.latticeMulSet L) (hα0 : α 0) (u v : Polynomial ) (hv : v 0) (h : ∀ (z : ), Polynomial.eval (PeriodPair.weierstrassP L z) v * PeriodPair.weierstrassP L (α * z) = Polynomial.eval (PeriodPair.weierstrassP L z) u) :
                                                α * (starRingEnd ) α = u.natDegree

                                                For an endomorphism $\alpha$ of a single lattice $L$, the norm $\alpha \overline{\alpha}$ equals the degree $\deg u$ of the rational $\wp$-expression of the induced isogeny.

                                                theorem ComplexLattice.latticeMulSet_mul_mem (L : ComplexLattice) {α β : } ( : α L.latticeMulSet L) ( : β L.latticeMulSet L) :
                                                α * β L.latticeMulSet L

                                                The endomorphism multiplier set $\{\alpha : \alpha L \subseteq L\}$ is closed under multiplication, mirroring composition of endomorphisms.

                                                theorem ComplexLattice.inducedMap_mul (L : ComplexLattice) (α β : ) ( : α L.latticeMulSet L) ( : β L.latticeMulSet L) (x : L.torusQuot) :
                                                (L.inducedMap L (α * β) ) x = (L.inducedMap L α ) ((L.inducedMap L β ) x)

                                                Multiplicativity of the induced map: the endomorphism of $\mathbb{C}/L$ attached to $\alpha \beta$ equals the composition of the endomorphisms attached to $\alpha$ and $\beta$.

                                                theorem ComplexLattice.corollary_16_5_ring_iso (L : ComplexLattice) :
                                                (∀ (φ : L.ComplexTorusHolMap L), φ.toFun 0 = 0∃ (α : ) ( : α L.latticeMulSet L), ∀ (z : ), φ.toFun (L.proj z) = (L.inducedMap L α ) (L.proj z)) (∀ (α γ : ) ( : α L.latticeMulSet L) ( : γ L.latticeMulSet L), (∀ (z : ), (L.inducedMap L α ) (L.proj z) = (L.inducedMap L γ ) (L.proj z))α = γ) (∀ (α β : ) ( : α L.latticeMulSet L) ( : β L.latticeMulSet L) (x : L.torusQuot), (L.inducedMap L (α + β) ) x = (L.inducedMap L α ) x + (L.inducedMap L β ) x) ∀ (α β : ) ( : α L.latticeMulSet L) ( : β L.latticeMulSet L) (x : L.torusQuot), (L.inducedMap L (α * β) ) x = (L.inducedMap L α ) ((L.inducedMap L β ) x)

                                                Corollary 16.5 (ring isomorphism). The set $\{\alpha : \alpha L \subseteq L\}$ with addition and multiplication of complex numbers is naturally isomorphic to the ring of holomorphic endomorphisms of $\mathbb{C}/L$: existence and uniqueness from Corollary 16.2 together with additivity and multiplicativity of the induced maps.

                                                theorem ComplexLattice.rosatiInvolution_exists (L : ComplexLattice) (α : ) ( : α L.latticeMulSet L) :
                                                βL.latticeMulSet L, β = (starRingEnd ) α

                                                The Rosati involution on $\mathrm{End}(\mathbb{C}/L)$: for any endomorphism multiplier $\alpha$, the complex conjugate $\overline{\alpha}$ is also an endomorphism multiplier.

                                                noncomputable def ComplexLattice.dualEndomorphism (L : ComplexLattice) (α : ) ( : α L.latticeMulSet L) :

                                                The dual endomorphism (Rosati involution) of $\alpha$: an element of the endomorphism multiplier set realising the complex conjugate $\overline{\alpha}$.

                                                Instances For

                                                  The dual endomorphism is the complex conjugate of the original endomorphism.

                                                  noncomputable def ComplexLattice.traceEndomorphism (L : ComplexLattice) (α : ) ( : α L.latticeMulSet L) :

                                                  The trace of an endomorphism: $\alpha + \overline{\alpha}$, an integer (more precisely, a real-integer) by Theorem 12.21.

                                                  Instances For
                                                    @[simp]

                                                    Corollary 16.5 (involution = conjugation). The Rosati involution on the endomorphism ring of $\mathbb{C}/L$ is exactly complex conjugation.