NYLL
Module

CurveModel_exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField
2 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists curve Model hom pullback pullback germ eq of ring Equiv function Field

Imports3
Imported by1

Declarations

theorem

nonempty_preimage_of_isIso

L63 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField.CMTransport.nonempty_preimage_of_isIso
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField
attribute [-instance]
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] 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.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one AlgebraicCurve.mulAdele_apply
  AlgebraicCurve.residuePairing_apply_coe AlgebraicCurve.mem_adeleBdd AlgebraicCurve.weilSmul_one
  AlgebraicCurve.diagonalHom_apply AlgebraicCurve.weilSmul_apply AlgebraicCurve.adeleSpaceMul_coe
  AlgebraicCurve.mulAdele_one AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
namespace CMTransport
Lean source · statement
theorem nonempty_preimage_of_isIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] (U : Y.Opens)
    [h : Nonempty (Scheme.Opens.toScheme U)] : Nonempty (Scheme.Opens.toScheme (f ⁻¹ᵁ U))
theorem

exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField

L86 ↗
AlgebraicCurve.CurveModel.exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurve.CurveModel
open _root_.AlgebraicCurves.Models.Proofs in
open CurveModel_exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve in
open _root_.AlgebraicGeometry.SmoothProperCurve in
Lean source · statement
theorem exists_curveModel_hom_pullback_pullback_germ_eq_of_ringEquiv_functionField
    {R₀ : Type} [CommRing R₀] {X : Scheme.{0}} (πX : X ⟶ Spec (CommRingCat.of R₀))
    [IsProper πX] [SmoothOfRelativeDimension 1 πX] [GeometricallyIntegral πX]
    {O : Type} [CommRing O] (j : R₀ →+* O) (k : Type) [Field k] [IsAlgClosed k] (i : O →+* k)
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R₀))
    (hs : Spec.map (CommRingCat.ofHom i) ≫ Spec.map (CommRingCat.ofHom j) = s)
    [AlgebraicGeometry.IsIntegral ↑(pullback πX s)]
    {L : Type} [Field L] [Algebra k L] (eL : L ≃+* ↥((pullback πX s).functionField))
    (heL : ∀ z : k, eL (algebraMap k L z) = baseToFunctionField (pullback.snd πX s) z) :
    ∃ (𝔐 : AlgebraicCurve.CurveModel k L)
      (e : 𝔐.C ⟶ pullback (pullback.snd πX (Spec.map (CommRingCat.ofHom j))) (Spec.map
        (CommRingCat.ofHom i)))
      (_ : IsIso e),
      e ≫ pullback.snd (pullback.snd πX (Spec.map (CommRingCat.ofHom j))) (Spec.map
        (CommRingCat.ofHom i)) = 𝔐.toBase ∧
      ∀ (U : X.Opens) [Nonempty (Scheme.Opens.toScheme U)]
        [Nonempty (Scheme.Opens.toScheme ((pullback.fst πX s) ⁻¹ᵁ U))]
        [Nonempty (Scheme.Opens.toScheme ((e ≫ pullback.fst (pullback.snd πX (Spec.map
          (CommRingCat.ofHom j))) (Spec.map (CommRingCat.ofHom i)) ≫
          pullback.fst πX (Spec.map (CommRingCat.ofHom j))) ⁻¹ᵁ U))]
        (t : Γ(X, U)),
        𝔐.ffEquiv.symm (𝔐.C.germToFunctionField
          ((e ≫ pullback.fst (pullback.snd πX (Spec.map (CommRingCat.ofHom j))) (Spec.map
            (CommRingCat.ofHom i)) ≫
            pullback.fst πX (Spec.map (CommRingCat.ofHom j))) ⁻¹ᵁ U)
          (((e ≫ pullback.fst (pullback.snd πX (Spec.map (CommRingCat.ofHom j))) (Spec.map
            (CommRingCat.ofHom i)) ≫
            pullback.fst πX (Spec.map (CommRingCat.ofHom j))).app U).hom t)) =
        eL.symm ((pullback πX s).germToFunctionField ((pullback.fst πX s) ⁻¹ᵁ U) (((pullback.fst πX
          s).app U).hom t))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.