English
If Q and Q' have the same underlying fixed prime (same base), then arithFrobAt for Q and Q' are conjugate.
Русский
Если у Q и Q' совпадает основание базового простого (одинаковое основание), то arithFrobAt для Q и Q' сопряжены.
LaTeX
$$$ isConj\_arithFrobAt(R,S,G,Q,Q')$, given $Q.under R = Q'.under R$.$$
Lean4
theorem _root_.isConj_arithFrobAt [Q.IsPrime] [Finite (S ⧸ Q)] (Q' : Ideal S) [Q'.IsPrime] [Finite (S ⧸ Q')]
(H : Q.under R = Q'.under R) : IsConj (arithFrobAt R G Q) (arithFrobAt R G Q') :=
by
obtain ⟨P, hP, h₁, h₂⟩ : ∃ P : Ideal R, P.IsPrime ∧ P = Q.under R ∧ P = Q'.under R :=
⟨Q.under R, inferInstance, rfl, H⟩
convert
(exists_primesOver_isConj S G P ⟨⟨Q, ‹_›, ⟨h₁⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose_spec.2 ⟨Q, ‹_›, ⟨h₁⟩⟩ ⟨Q', ‹_›, ⟨h₂⟩⟩
· subst h₁; rfl
· subst h₂; rfl
