instIsPretransitiveAlgEquivElemPrimesOverOfIsGalois

English

Under IsGalois(K,L), the action of AlgEquiv K L L on the set of primes over p in B is pretransitive: given any two primes P,Q lying over p, there exists σ in the automorphism group such that map σ P = Q.

Русский

При IsGalois(K,L) действия AlgEquiv K L L на множество простых над p над B являются предтрaнзитивными: для любых P,Q над p существует σ так, что map σ P = Q.

LaTeX

$$IsGalois K L ⇒ MulAction.IsPretransitive (AlgEquiv K L L) (p.primesOver B).Elem$$

Lean4

instance [IsGalois K L] : MulAction.IsPretransitive (L ≃ₐ[K] L) (primesOver p B) where
  exists_smul_eq := by
    intro ⟨P, _, _⟩ ⟨Q, _, _⟩
    rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩
    exact
      ⟨(galRestrict A K L B).symm σ,
        Subtype.val_inj.mp <| (congrFun (congrArg map ((galRestrict A K L B).apply_symm_apply σ)) P).trans hs⟩

Похожие утверждения