AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Exists_canonicalDivisor_genus_riemannRoch.S18RR.finite_and_isSeparable_of_ratFuncAlgHom
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Exists_canonicalDivisor_genus_riemannRoch
attribute [-instance] AlgebraicCurve.instHasLocalResidue_of_hasCanonicalLocalResidueK
AlgebraicCurve.instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
AlgebraicCurve.Place.kw_ffgc_finiteDimensional_adicCompletion
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersIntegersCompletion
ModularCurve.KwF4gRRTate.instAlgebraKAdicCompletionIntegers
AlgebraicCurve.Place.kw_ffgc_continuousSMul_adicCompletionComap
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersCompletionCompletion
instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal
AlgebraicCurve.instHasCanonicalLocalResidueK
AlgebraicCurve.Place.instAlgebra_restrictResidueField
AlgebraicCurve.Place.instIsScalarTower_restrictResidueField AlgebraicCurve.instHasLocalResidue
AlgebraicCurve.HasSeparableResidue.of_perfectField_of_isCurveOver
AlgebraicCurve.HasSeparableResidue.of_perfectField
AlgebraicCurve.Place.instIsLocalHom_restrictSubringHom
AlgebraicCurve.instHasCanonicalLocalResidueKStar ModularCurve.KwNo6Pin.isLocalRing_completion
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsPrimeCenter AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.sizeOf_spec
AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.injEq AlgebraicCurve.adeleSingle_coe
AlgebraicCurve.kaehlerResidueTermKFam_apply AlgebraicCurve.Place.LocalResidueData.mk.injEq
AlgebraicCurve.Place.LocalResidueData.mk.sizeOf_spec AlgebraicCurve.Divisor.mapRestrict_single
AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers_coe
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.sizeOf_spec
AlgebraicCurve.Place.mem_simplePoleSubmodule AlgebraicCurve.Place.coe_uniformizerSubring
ModularCurve.Lg37.Lg37CompletionSection.mk.injEq
AlgebraicCurve.Place.CoefficientFieldSection.mk.injEq
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.injEq
ModularCurve.Lg37.Lg37CompletionSection.mk.sizeOf_spec
AlgebraicCurve.Place.CoefficientFieldSection.mk.sizeOf_spec
AlgebraicCurve.Place.poleSubmodule_one AlgebraicCurve.Place.mem_poleSubmodule
AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
universe u v
open IntermediateField Polynomial
namespace S18RR
variable {K F : Type*} [Field K] [Field F] [Algebra K F]Lean source · full declaration
theorem finite_and_isSeparable_of_ratFuncAlgHom (t : F)
(hfd : FiniteDimensional K⟮t⟯ F) (hsep : Algebra.IsSeparable K⟮t⟯ F)
(φ : RatFunc K →ₐ[K] F) (hφ : φ RatFunc.X = t) :
letI := φ.toRingHom.toAlgebra
Module.Finite (RatFunc K) F ∧ Algebra.IsSeparable (RatFunc K) F := by
let : Algebra (RatFunc K) F := φ.toRingHom.toAlgebra
let E : IntermediateField K F := φ.fieldRange
have htE : t ∈ E := ⟨RatFunc.X, hφ⟩
have hle : K⟮t⟯ ≤ E := adjoin_simple_le_iff.mpr htE
let : Algebra K⟮t⟯ E := (IntermediateField.inclusion hle).toAlgebra
have : IsScalarTower K⟮t⟯ E F := IsScalarTower.of_algebraMap_eq (fun x => rfl)
have : Module.Finite E F := Module.Finite.of_restrictScalars_finite K⟮t⟯ E F
have : Algebra.IsSeparable E F := Algebra.isSeparable_tower_top_of_isSeparable K⟮t⟯ E F
let e : RatFunc K ≃ₐ[K] E := AlgEquiv.ofInjectiveField φ
have key : ∀ x : E, φ (e.symm x) = (x : F) := fun x => by
have h2 : ((e (e.symm x) : E) : F) = φ (e.symm x) := AlgEquiv.ofInjective_apply _ _ _
rw [e.apply_symm_apply] at h2
exact h2.symm
have he : (algebraMap (RatFunc K) F).comp (e.symm.toRingEquiv : E ≃+* RatFunc K).toRingHom
= (RingEquiv.refl F).toRingHom.comp (algebraMap E F) := by
refine RingHom.ext fun x => ?_
simp only [RingHom.comp_apply, RingHom.algebraMap_toAlgebra]
exact key x
refine ⟨?_, ?_⟩
· exact Module.Finite.of_equiv_equiv (e.symm.toRingEquiv : E ≃+* RatFunc K) (RingEquiv.refl F) he
· exact Algebra.IsSeparable.of_equiv_equiv (e.symm.toRingEquiv : E ≃+* RatFunc K)
(RingEquiv.refl F) he