NYLL
Module

GroupOfMatching.lean

Nyll.AlgebraicCurves.Geometry.Descent.GroupOfMatching
7 declarations indexed from sourceView source ↗

Module documentation

Commutative group laws on effective descents

Matching local elements form a subgroup. The actual matching equivalence transports its operations to relative points of the descended scheme.

Imports4
Imported by3

Declarations

def

matchingSubgroup

L31 ↗
AlgebraicGeometry.DescentAction.matchingSubgroup
Documentation

The subgroup of local elements satisfying the descent matching condition.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ CommGrpCat.{u + 1})
Lean source · full declaration
def matchingSubgroup (T : Over S) :
    Subgroup (G.obj (op ((Over.map s).obj ((Over.pullback s).obj T)))) where
  carrier := {z | Matching s (G ⋙ forget CommGrpCat) T z}
  one_mem' := by
    intro W g₁ g₂ _
    change (G.map g₁.op) 1 = (G.map g₂.op) 1
    rw [map_one, map_one]
  mul_mem' := by
    intro x y hx hy W g₁ g₂ hg
    change (G.map g₁.op) (x * y) = (G.map g₂.op) (x * y)
    rw [map_mul, map_mul]
    exact congrArg₂ (· * ·) (hx g₁ g₂ hg) (hy g₁ g₂ hg)
  inv_mem' := by
    intro x hx W g₁ g₂ hg
    change (G.map g₁.op) x⁻¹ = (G.map g₂.op) x⁻¹
    rw [map_inv, map_inv]
    exact congrArg Inv.inv (hx g₁ g₂ hg)
theorem

localPoint_comp

L56 ↗
AlgebraicGeometry.DescentAction.localPoint_comp
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ CommGrpCat.{u + 1})
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
Lean source · statement
theorem localPoint_comp {T U : Over S} (φ : U ⟶ T) (m : T ⟶ Over.mk f) :
    localPoint s (G ⋙ forget CommGrpCat) x' hX' f e he (φ ≫ m) =
      G.map ((Over.map s).map ((Over.pullback s).map φ)).op
        (localPoint s (G ⋙ forget CommGrpCat) x' hX' f e he m)
def

matchingPointEquiv

L80 ↗
AlgebraicGeometry.DescentAction.matchingPointEquiv
Documentation

Relative scheme points identified with the subgroup of matching local elements.

Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ CommGrpCat.{u + 1})
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
section affineBase
variable {R : Type u} [CommRing R]
  {S' : Scheme.{u}} (s : S' ⟶ Spec (CommRingCat.of R))
  (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ CommGrpCat.{u + 1})
  {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
  [∀ T : Over (Spec (CommRingCat.of R)), EffectiveEpi (pullback.fst T.hom s)]
Lean source · statement
def matchingPointEquiv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    SchemeHomOver t f ≃ matchingSubgroup s G (Over.mk t)
theorem

matchingPointEquiv_apply_val

L85 ↗
AlgebraicGeometry.DescentAction.matchingPointEquiv_apply_val
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ CommGrpCat.{u + 1})
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
section affineBase
variable {R : Type u} [CommRing R]
  {S' : Scheme.{u}} (s : S' ⟶ Spec (CommRingCat.of R))
  (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ CommGrpCat.{u + 1})
  {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
  [∀ T : Over (Spec (CommRingCat.of R)), EffectiveEpi (pullback.fst T.hom s)]
Lean source · statement
theorem matchingPointEquiv_apply_val {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x : SchemeHomOver t f) :
    (matchingPointEquiv s G x' hX' f e he hcompat t x).1 =
      localPoint s (G ⋙ forget CommGrpCat) x' hX' f e he (schemeHomOverToOverHom x)
theorem

matchingPointEquiv_comp

L90 ↗
AlgebraicGeometry.DescentAction.matchingPointEquiv_comp
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ CommGrpCat.{u + 1})
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
section affineBase
variable {R : Type u} [CommRing R]
  {S' : Scheme.{u}} (s : S' ⟶ Spec (CommRingCat.of R))
  (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ CommGrpCat.{u + 1})
  {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
  [∀ T : Over (Spec (CommRingCat.of R)), EffectiveEpi (pullback.fst T.hom s)]
Lean source · statement
theorem matchingPointEquiv_comp {T T' : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (t' : T' ⟶ Spec (CommRingCat.of R))
    (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (x : SchemeHomOver t f) :
    (matchingPointEquiv s G x' hX' f e he hcompat t'
      (schemeHomOverComp ψ hψ x)).1 =
      G.map ((Over.map s).map ((Over.pullback s).map (Over.homMk ψ hψ : Over.mk t' ⟶ Over.mk t))).op
        (matchingPointEquiv s G x' hX' f e he hcompat t x).1
def

relativeGroupLawOfMatching

L108 ↗
AlgebraicGeometry.DescentAction.relativeGroupLawOfMatching
Documentation

The relative group law obtained by effective descent of a group-valued presheaf.

Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ CommGrpCat.{u + 1})
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
section affineBase
variable {R : Type u} [CommRing R]
  {S' : Scheme.{u}} (s : S' ⟶ Spec (CommRingCat.of R))
  (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ CommGrpCat.{u + 1})
  {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
  [∀ T : Over (Spec (CommRingCat.of R)), EffectiveEpi (pullback.fst T.hom s)]
Lean source · full declaration
def relativeGroupLawOfMatching : RelativeGroupLaw R f where
  mul t x y :=
    (matchingPointEquiv s G x' hX' f e he hcompat t).symm
      (matchingPointEquiv s G x' hX' f e he hcompat t x *
        matchingPointEquiv s G x' hX' f e he hcompat t y)
  one t := (matchingPointEquiv s G x' hX' f e he hcompat t).symm 1
  inv t x :=
    (matchingPointEquiv s G x' hX' f e he hcompat t).symm
      (matchingPointEquiv s G x' hX' f e he hcompat t x)⁻¹
  mul_assoc t x y z := by
    apply (matchingPointEquiv s G x' hX' f e he hcompat t).injective
    simp only [Equiv.apply_symm_apply, mul_assoc]
  one_mul t x := by
    apply (matchingPointEquiv s G x' hX' f e he hcompat t).injective
    simp only [Equiv.apply_symm_apply, one_mul]
  mul_one t x := by
    apply (matchingPointEquiv s G x' hX' f e he hcompat t).injective
    simp only [Equiv.apply_symm_apply, mul_one]
  inv_mul_cancel t x := by
    apply (matchingPointEquiv s G x' hX' f e he hcompat t).injective
    simp only [Equiv.apply_symm_apply, inv_mul_cancel]
  mul_natural t t' ψ hψ x y := by
    apply (matchingPointEquiv s G x' hX' f e he hcompat t').injective
    apply Subtype.ext
    rw [matchingPointEquiv_comp]
    simp only [Equiv.apply_symm_apply, Subgroup.coe_mul, map_mul]
    rw [matchingPointEquiv_comp, matchingPointEquiv_comp]
theorem

relativeGroupLawOfMatching_commutative

L136 ↗
AlgebraicGeometry.DescentAction.relativeGroupLawOfMatching_commutative
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ CommGrpCat.{u + 1})
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
section affineBase
variable {R : Type u} [CommRing R]
  {S' : Scheme.{u}} (s : S' ⟶ Spec (CommRingCat.of R))
  (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ CommGrpCat.{u + 1})
  {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hcompat : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
  [∀ T : Over (Spec (CommRingCat.of R)), EffectiveEpi (pullback.fst T.hom s)]
Lean source · statement
theorem relativeGroupLawOfMatching_commutative :
    (relativeGroupLawOfMatching s G x' hX' f e he hcompat).IsCommutative

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