AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_inertiaDeg_smul.restrictSmulValuationSubringEquiv
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_inertiaDeg_smul
open AlgebraicCurve AlgebraicCurve.SemilinearAut
open scoped Pointwise
noncomputable sectionLean source · full declaration
def restrictSmulValuationSubringEquiv {K F F' : Type*} [Field K] [Field F] [Field F']
[Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] {g :
SemilinearAut K F} {g' : SemilinearAut K F'} (hgg' : IntertwinesAlong (algebraMap F F') g g')
(w : Place K F') :
(w.restrict F).toValuationSubring ≃+* ((g' • w).restrict F).toValuationSubring where
toFun x := ⟨g • (x : F), by
change algebraMap F F' (g • (x : F)) ∈ (g' • w).toValuationSubring
rw [← hgg' (x : F), smul_toValuationSubring]
exact ValuationSubring.smul_mem_pointwise_smul g' _ _ x.2⟩
invFun y := ⟨g⁻¹ • (y : F), by
change algebraMap F F' (g⁻¹ • (y : F)) ∈ w.toValuationSubring
rw [← hgg'.inv (y : F)]
have hy : algebraMap F F' (y : F) ∈ (g' • w).toValuationSubring := y.2
rw [smul_toValuationSubring,
ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem] at hy
exact hy⟩
left_inv x := by ext; exact inv_smul_smul g (x : F)
right_inv y := by ext; exact smul_inv_smul g (y : F)
map_mul' x y := by ext; exact smul_mul' g (x : F) (y : F)
map_add' x y := by ext; exact smul_add g (x : F) (y : F)