structure
L35 ↗FiniteMapData
AlgebraicGeometry.SmoothProperCurve.FiniteMapData
Finite coordinate maps on complementary affine charts of a curve with a section.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits NeronModelInfra
namespace AlgebraicGeometry.SmoothProperCurveLean source · full declaration
structure FiniteMapData {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) where
/-- The affine chart complementary to the image of the chosen section. -/
U : C.Opens
/-- The second affine chart, which contains the image of the chosen section. -/
V : C.Opens
/-- The coordinate on the chart complementary to the section. -/
f : Γ(C, U)
/-- The coordinate on the second affine chart. -/
g : Γ(C, V)
/-- The common rank of the finite free coordinate level sets. -/
m : ℕ
/-- The chart complementary to the section is affine. -/
isAffineOpen_U : IsAffineOpen U
/-- The second chart is affine. -/
isAffineOpen_V : IsAffineOpen V
/-- The two affine charts cover the curve. -/
sup_eq_top : U ⊔ V = ⊤
/-- A point belongs to the first chart exactly when it is outside the section image. -/
mem_U_iff : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base
/-- The chart intersection is the basic open where the first coordinate is invertible. -/
inf_eq_basicOpen : U ⊓ V = C.basicOpen f
/-- The chart intersection is also the basic open where the second coordinate is invertible. -/
inf_eq_basicOpen_g : U ⊓ V = C.basicOpen g
/-- The restrictions of the two coordinates to the intersection multiply to one. -/
res_f_mul_res_g : (C.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op).hom f *
(C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op).hom g = 1
/-- The polynomial coordinate map on the first chart is finite. -/
finite_f : letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
(Polynomial.aeval f : Polynomial R →ₐ[R] Γ(C, U)).toRingHom.Finite
/-- The polynomial coordinate map on the second chart is finite. -/
finite_g : letI := Scheme.TwoAffineOpenCover.algebraOfHom c V
(Polynomial.aeval g : Polynomial R →ₐ[R] Γ(C, V)).toRingHom.Finite
/-- Over every local base algebra, each first-coordinate level set is finite free of rank m. -/
levelSet_free : ∀ (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] (s : S),
letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
Module.Finite S (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))}) ∧
Module.Free S (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))}) ∧
Module.finrank S (S ⊗[R] Γ(C, U) ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : Γ(C, U))}) = m