Constructs the permutation action on a finite fiber power and records symmetric power properties.
The fiber product of r copies of C over the given field.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)abbrev finFibrePow : Scheme.{u}The projection from the finite fiber power to its l-th factor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowabbrev proj (l : Fin r) : finFibrePow c r ⟶ CThe structure morphism from the finite fiber power to the field spectrum.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowabbrev toBase : finFibrePow c r ⟶ Spec (CommRingCat.of k)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem proj_comp (l : Fin r) : proj c r l ≫ c = toBase c rThe endomorphism that permutes the factors by the inverse permutation.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowdef permHom (σ : Equiv.Perm (Fin r)) : finFibrePow c r ⟶ finFibrePow c rSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permHom_proj (σ : Equiv.Perm (Fin r)) (j : Fin r) :
permHom c r σ ≫ proj c r j = proj c r (σ⁻¹ j)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permHom_toBase (σ : Equiv.Perm (Fin r)) : permHom c r σ ≫ toBase c r = toBase c rSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permHom_one : permHom c r 1 = 𝟙 _Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permHom_mul (σ τ : Equiv.Perm (Fin r)) :
permHom c r (σ * τ) = permHom c r τ ≫ permHom c r σThe automorphism of the fiber power induced by a permutation of its factors.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowdef permAut (σ : Equiv.Perm (Fin r)) : Aut (finFibrePow c r) where
hom := permHom c r σ
inv := permHom c r σ⁻¹
hom_inv_id := by rw [← permHom_mul, inv_mul_cancel, permHom_one]
inv_hom_id := by rw [← permHom_mul, mul_inv_cancel, permHom_one]The symmetric group action on the finite fiber power.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowdef permAct : Equiv.Perm (Fin r) →* Aut (finFibrePow c r)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permAct_hom (σ : Equiv.Perm (Fin r)) : (permAct c r σ).hom = permHom c r σSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permAct_inv (σ : Equiv.Perm (Fin r)) : (permAct c r σ).inv = permHom c r σ⁻¹Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permAct_hom_proj (σ : Equiv.Perm (Fin r)) (i : Fin r) :
(permAct c r σ).hom ≫ proj c r (σ i) = proj c r iSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
namespace finFibrePowtheorem permAct_hom_toBase (σ : Equiv.Perm (Fin r)) :
(permAct c r σ).hom ≫ toBase c r = toBase c rSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)theorem le_preimage_of_comp_eq {X Y : Scheme.{u}} (g : X ⟶ X) (q : X ⟶ Y) (h : g ≫ q = q)
(V : Y.Opens) : q ⁻¹ᵁ V ≤ g ⁻¹ᵁ (q ⁻¹ᵁ V)A symmetric power with quotient, affine chart, and geometric property data.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicCurve
open AlgebraicGeometrystructure SymmetricPowerPackage {k : Type u} [Field k] {C : Scheme.{u}}
(c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ) where
/-- The scheme representing the symmetric power. -/
Csym : Scheme.{u}
/-- The structure morphism of the symmetric power over the field. -/
csym : Csym ⟶ Spec (CommRingCat.of k)
/-- The quotient morphism from the finite fiber power. -/
π : finFibrePow c r ⟶ Csym
/-- The quotient morphism preserves the structure morphism to the field. -/
π_comp_csym : π ≫ csym = finFibrePow.toBase c r
/-- The quotient morphism is invariant under permutation of the factors. -/
permAct_comp_π : ∀ σ : Equiv.Perm (Fin r), (finFibrePow.permAct c r σ).hom ≫ π = π
/-- The quotient morphism is finite. -/
isFinite_π : IsFinite π
/-- The quotient morphism is surjective on points. -/
surjective_π : Surjective π
/-- Two points have the same quotient image exactly when a permutation relates them. -/
π_apply_eq_iff : ∀ x x' : ↥(finFibrePow c r),
π.base x = π.base x' ↔ ∃ σ : Equiv.Perm (Fin r), (finFibrePow.permAct c r σ).hom.base x = x'
/-- The quotient induces an injective map on sections over each open set. -/
app_injective : ∀ V : Csym.Opens, Function.Injective (π.app V)
/-- The image on sections consists exactly of the permutation-invariant sections. -/
range_app : ∀ V : Csym.Opens, Set.range (π.app V) =
{s | ∀ σ : Equiv.Perm (Fin r), (finFibrePow.permAct c r σ).hom.appLE (π ⁻¹ᵁ V) (π ⁻¹ᵁ V)
(le_preimage_of_comp_eq _ _ (permAct_comp_π σ) V) s = s}
/-- An affine open of the curve gives an affine chart on the symmetric power. -/
exists_affine_chart : ∀ U : C.Opens, IsAffineOpen U →
∃ V : Csym.Opens, IsAffineOpen V ∧ π ⁻¹ᵁ V = ⨅ l : Fin r, (finFibrePow.proj c r l) ⁻¹ᵁ U
/-- The symmetric power scheme is integral. -/
integral : IsIntegral Csym
/-- The symmetric power is proper over the field. -/
proper : IsProper csym
/-- The symmetric power is smooth of relative dimension r over the field. -/
smooth : SmoothOfRelativeDimension r csym