theorem image_subsingleton_or_surjective {G : Type u} [TopologicalSpace G] [Group G] [IsCompleteVariety G] [IsTopologicalGroup G] [ConnectedSpace G] {f : G → G} (hf : Continuous f) : Function.Surjective f ∨ ∃ (c : G), Set.range f = {c}

A continuous self-map $f \colon G \to G$ of a complete connected topological group is either surjective or has singleton image (a key dichotomy for proper varieties).

theorem semicontinuity_of_image {G : Type u} [TopologicalSpace G] [Group G] [IsCompleteVariety G] [IsTopologicalGroup G] [ConnectedSpace G] {P : Type u} [TopologicalSpace P] [ConnectedSpace P] {H : Type u} [TopologicalSpace H] [Group H] [IsCompleteVariety H] [IsTopologicalGroup H] [ConnectedSpace H] {F : G × P → H} (hF : Continuous F) (hF_const : ∃ (p₀ : P), ∀ (g : G), F (g, p₀) = 1) (p : P) (g : G) : F (g, p) = 1

Semicontinuity in families: if $F \colon G \times P \to H$ is continuous between connected complete varieties / groups and there exists $p_0$ with $F(g, p_0) = 1$ for all $g$, then $F(g, p) = 1$ identically.

theorem rigidity_of_complete_connected_group {G : Type u} [TopologicalSpace G] [Group G] [IsCompleteVariety G] [IsTopologicalGroup G] [ConnectedSpace G] {f : G → G} (hf_cont : Continuous f) (hf_id : f 1 = 1) {y : G} (hy : y ∉ Set.range f) (x : G) : f x = 1

Rigidity lemma: a continuous self-map $f$ of a complete connected topological group that fixes the identity and whose image misses some point must be constantly $1$.

theorem IsAbelianVariety.mul_comm {k : Type u} [Field k] {A : Type u} [TopologicalSpace A] [Group A] [IsAbelianVariety k A] (a b : A) : a * b = b * a

Theorem 23.23: An abelian variety is commutative; equivalently, the group law $a \cdot b$ on an IsAbelianVariety is symmetric. The proof applies the rigidity lemma to the commutator map $g \mapsto b^{-1} g^{-1} b g$.

@[reducible]

def IsAbelianVariety.toCommGroup {k : Type u} [Field k] {A : Type u} [TopologicalSpace A] [Group A] [IsAbelianVariety k A] : CommGroup A

Promotes the Group instance on an abelian variety to a CommGroup instance using the commutativity theorem IsAbelianVariety.mul_comm.

theorem rigidity_lemma_product {G : Type u} [TopologicalSpace G] [Group G] [IsCompleteVariety G] [IsTopologicalGroup G] [ConnectedSpace G] {H : Type u} [TopologicalSpace H] [Group H] [IsCompleteVariety H] [IsTopologicalGroup H] [ConnectedSpace H] {Ψ : G × G → H} (hΨ_cont : Continuous Ψ) (hΨ_fst : ∀ (g : G), Ψ (g, 1) = 1) (_hΨ_snd : ∀ (h : G), Ψ (1, h) = 1) (g h : G) : Ψ (g, h) = 1

Two-variable rigidity: a continuous $\Psi \colon G \times G \to H$ between complete connected topological groups that is identically $1$ on each axis (i.e. $\Psi(g,1) = \Psi(1,h) = 1$) is identically $1$.

theorem morphism_preserving_identity_is_hom {k : Type u} [Field k] {G : Type u} [TopologicalSpace G] [Group G] [IsAbelianVariety k G] {H : Type u} [TopologicalSpace H] [Group H] [IsAbelianVariety k H] (φ : G → H) (hφ_cont : Continuous φ) (hφ_id : φ 1 = 1) (g h : G) : φ (g * h) = φ g * φ h

A continuous map $\varphi$ between abelian varieties that sends $1 \mapsto 1$ is automatically a group homomorphism: $\varphi(gh) = \varphi(g) \varphi(h)$. Proved by applying the two-variable rigidity lemma to $\Psi(g,h) = \varphi(g)\varphi(h)\varphi(gh)^{-1}$.