CyclotomicCrossingBoundary.lean

1 import PaperX.CyclotomicCrossingCore
2 import Mathlib.Analysis.Complex.Polynomial.Basic
3 
4 /-!
5 # A field-level boundary for the restriction-order hypothesis
6 
7 Complex conjugation over the reals is nontrivial but restricts trivially to
8 the bottom intermediate field. Its fixed field and that auxiliary field fail
9 to generate the complex numbers. This is not an arithmetic distribution example.
10 -/
11 
12 set_option autoImplicit false
13 
14 noncomputable section
15 
16 namespace PaperX.CyclotomicCrossingBoundary
17 
18 open IntermediateField
19 
20 /-- The test extension is genuinely a finite Galois extension. -/
21 theorem real_complex_finite_galois :
22     FiniteDimensional ℝ ℂ ∧ IsGalois ℝ ℂ := by
23   let : Algebra.IsQuadraticExtension ℝ ℂ := ⟨Complex.finrank_real_complex⟩
24   exact ⟨inferInstance, inferInstance⟩
25 
26 /-- Conjugation is nontrivial on the actual complex field. -/
27 theorem conjugation_ne_one : Complex.conjAe ≠ 1 := by
28   intro h
29   have heq := congrArg (fun f : ℂ ≃ₐ[ℝ] ℂ => (f Complex.I).im) h
30   norm_num at heq
31 
32 /-- Its order is two. -/
33 theorem conjugation_order : orderOf Complex.conjAe = 2 := by
34   apply orderOf_eq_prime
35   · ext z
36     simp [pow_two, AlgEquiv.mul_apply]
37   · exact conjugation_ne_one
38 
39 /-- The auxiliary bottom field sees only the identity restriction. -/
40 theorem conjugation_restrict_bottom :
41     AlgEquiv.restrictNormalHom (⊥ : IntermediateField ℝ ℂ) Complex.conjAe = 1 := by
42   apply MonoidHom.mem_ker.mp
43   rw [IntermediateField.restrictNormalHom_ker, fixingSubgroup_bot]
44   exact Subgroup.mem_top _
45 
46 /-- In particular, restriction does not preserve the order. -/
47 theorem conjugation_restriction_order_mismatch :
48     orderOf (AlgEquiv.restrictNormalHom (⊥ : IntermediateField ℝ ℂ) Complex.conjAe) ≠
49       orderOf Complex.conjAe := by
50   rw [conjugation_restrict_bottom, orderOf_one, conjugation_order]
51   norm_num
52 
53 /-- Omitting the restriction-order hypothesis makes the crossing identity false,
54 even for the concrete finite Galois extension `ℂ/ℝ`. -/
55 theorem fixed_conjugation_sup_bottom_ne_top :
56     fixedField (Subgroup.zpowers Complex.conjAe) ⊔ (⊥ : IntermediateField ℝ ℂ) ≠ ⊤ := by
57   rw [sup_bot_eq]
58   intro h
59   have hI : Complex.I ∈ fixedField (Subgroup.zpowers Complex.conjAe) := by
60     rw [h]
61     exact mem_top
62   have heq := (mem_fixedField_iff (Subgroup.zpowers Complex.conjAe) Complex.I).mp hI Complex.conjAe
63     (Subgroup.mem_zpowers Complex.conjAe)
64   have him := congrArg Complex.im heq
65   norm_num at him
66 
67 end PaperX.CyclotomicCrossingBoundary

Back to source controls