AlgebraicCurves.Places.Proofs.Place_ramificationIndex_eq_of_restrict_eq.AlgebraicCurve.Place.intertwinesAlong_one_ofAlgAut
Source context 15 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ramificationIndex_eq_of_restrict_eq
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F' M : Type*} [Field K] [Field F'] [Field M] [Algebra K F'] [Algebra K M]
[Algebra F' M] [IsScalarTower K F' M]Lean source · statement
theorem intertwinesAlong_one_ofAlgAut (σ : M ≃ₐ[F'] M) :
SemilinearAut.IntertwinesAlong (algebraMap F' M) (1 : SemilinearAut K F')
(SemilinearAut.ofAlgAut (σ.restrictScalars K))