English
There is a natural action of automorphisms Aut_K(L) on the set of primes of B lying over p, given by σ ↦ primesOver.mk p (map galRestrict σ Q). This turns the set of primes over p into a MulAction by AlgEquiv_K(L).
Русский
Существовано естественное действие автоморфизмов Aut_K(L) на множество простых над p в B, задаваемое σ ↦ primesOver.mk p (map galRestrict σ Q). Это превращает множество primes over p в действие по умножению.
LaTeX
$$$\\text{MulAction} (\\mathrm{AlgEquiv}\\ K L L)\\; (p.primesOver\\ B).\\!\\mathrm{Elem}$$$
Lean4
noncomputable instance : MulAction (L ≃ₐ[K] L) (primesOver p B)
where
smul σ Q := primesOver.mk p (map (galRestrict A K L B σ) Q.1)
one_smul
Q := by
apply Subtype.val_inj.mp
change map _ Q.1 = Q.1
simpa only [map_one] using map_id Q.1
mul_smul σ τ
Q := by
apply Subtype.val_inj.mp
change map _ Q.1 = map _ (map _ Q.1)
rw [map_mul]
exact (Q.1.map_map ((galRestrict A K L B) τ).toRingHom ((galRestrict A K L B) σ).toRingHom).symm
