def AlgebraicGeometry.Scheme.diagMonFunctor (S : Scheme) : CategoryTheory.Functor AddCommMonCatᵒᵖ (CategoryTheory.Mon (CategoryTheory.Over S))

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Scheme.Diag (S : Scheme) (M : Type u) [AddCommMonoid M] : Scheme

The spectrum of a monoid algebra over an arbitrary base scheme S.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.Diag.canonicallyOver {S : Scheme} {M : Type u} [AddCommMonoid M] : (S.Diag M).CanonicallyOver S

Equations

• AlgebraicGeometry.Scheme.Diag.canonicallyOver = id inferInstance

theorem AlgebraicGeometry.Scheme.Diag.canonicallyOver_over {S : Scheme} {M : Type u} [AddCommMonoid M] : S.Diag M ↘ S = CategoryTheory.Limits.pullback.snd (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing }) (specULiftZIsTerminal.from S)

instance AlgebraicGeometry.Scheme.Diag.monObjAsOver {S : Scheme} {M : Type u} [AddCommMonoid M] : CategoryTheory.MonObj ((S.Diag M).asOver S)

Equations

• AlgebraicGeometry.Scheme.Diag.monObjAsOver = id inferInstance

theorem AlgebraicGeometry.Scheme.Diag.monObjAsOver_mul_left {S : Scheme} {M : Type u} [AddCommMonoid M] : CategoryTheory.MonObj.mul.left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback (specULiftZIsTerminal.from S)) (CategoryTheory.Over.mk (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (CategoryTheory.Over.mk (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing }))).left (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing }) (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (specULiftZIsTerminal.from S)) CategoryTheory.MonObj.mul.left) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing }) (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (specULiftZIsTerminal.from S)) ⋯)

theorem AlgebraicGeometry.Scheme.Diag.monObjAsOver_one_left {S : Scheme} {M : Type u} [AddCommMonoid M] : CategoryTheory.MonObj.one.left = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id (Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (specULiftZIsTerminal.from S))) (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.id (Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (specULiftZIsTerminal.from S)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (algSpec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })).left (Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom (ULift.{u, 0} ℤ) (MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative M))))))) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id (Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing })) (specULiftZIsTerminal.from S)) ⋯)

instance AlgebraicGeometry.Scheme.Diag.grpObjAsOver {S : Scheme} {G : Type u} [AddCommGroup G] : CategoryTheory.GrpObj ((S.Diag G).asOver S)

Equations

• AlgebraicGeometry.Scheme.Diag.grpObjAsOver = id inferInstance

theorem AlgebraicGeometry.Scheme.Diag.grpObjAsOver_inv_left {S : Scheme} {G : Type u} [AddCommGroup G] : CategoryTheory.GrpObj.inv.left = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative G), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing }) (specULiftZIsTerminal.from S)) CategoryTheory.GrpObj.inv.left) (CategoryTheory.Limits.pullback.snd (Spec { carrier := MonoidAlgebra (ULift.{u, 0} ℤ) (Multiplicative G), commRing := MonoidAlgebra.commRing } ↘ Spec { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing }) (specULiftZIsTerminal.from S)) ⋯

instance AlgebraicGeometry.Scheme.Diag.isCommMonObj_asOver {S : Scheme} {M : Type u} [AddCommMonoid M] : CategoryTheory.IsCommMonObj ((S.Diag M).asOver S)

@[simp]

theorem AlgebraicGeometry.Scheme.diagMonFunctor_obj {S : Scheme} (M : AddCommMonCatᵒᵖ) : S.diagMonFunctor.obj M = { X := (S.Diag ↑(Opposite.unop M)).asOver S, mon := Diag.monObjAsOver }

def AlgebraicGeometry.Scheme.Diag.map (S : Scheme) {M N : Type u} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) : S.Diag N ⟶ S.Diag M

A monoid hom M → N induces a monoid morphism Diag S N ⟶ Diag S M.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.Diag.isOver_map {S : Scheme} {M N : Type u} [AddCommMonoid M] [AddCommMonoid N] {f : M →+ N} : Hom.IsOver (map S f) S

instance AlgebraicGeometry.Scheme.Diag.isMonHom_map {S : Scheme} {M N : Type u} [AddCommMonoid M] [AddCommMonoid N] {f : M →+ N} : CategoryTheory.IsMonHom (Hom.asOver (map S f) S)

@[simp]

theorem AlgebraicGeometry.Scheme.diagMonFunctor_map {S : Scheme} {M N : AddCommMonCatᵒᵖ} (f : M ⟶ N) : S.diagMonFunctor.map f = { hom := Hom.asOver (Diag.map S (AddCommMonCat.Hom.hom f.unop)) S, isMonHom_hom := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Diag.map_id (S : Scheme) (M : Type u) [AddCommMonoid M] : map S (AddMonoidHom.id M) = CategoryTheory.CategoryStruct.id (S.Diag M)

@[simp]

theorem AlgebraicGeometry.Scheme.Diag.map_comp (S : Scheme) {M N O : Type u} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O] (f : N →+ O) (g : M →+ N) : map S (f.comp g) = CategoryTheory.CategoryStruct.comp (map S f) (map S g)

def AlgebraicGeometry.Scheme.Diag.mapIso (S : Scheme) {M N : Type u} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) : S.Diag M ≅ S.Diag N

A monoid iso M ≃ N induces a monoid isomorphism Diag S M ≅ Diag S N.

Equations

• AlgebraicGeometry.Scheme.Diag.mapIso S f = { hom := AlgebraicGeometry.Scheme.Diag.map S ↑f.symm, inv := AlgebraicGeometry.Scheme.Diag.map S ↑f, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Diag.mapIso_inv (S : Scheme) {M N : Type u} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) : (mapIso S f).inv = map S ↑f

@[simp]

theorem AlgebraicGeometry.Scheme.Diag.mapIso_hom (S : Scheme) {M N : Type u} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) : (mapIso S f).hom = map S ↑f.symm

def AlgebraicGeometry.Scheme.diagSpecIso (R : CommRingCat) (M : Type u) [AddCommMonoid M] : (Spec R).Diag M ≅ Spec { carrier := MonoidAlgebra (↑R) (Multiplicative M), commRing := MonoidAlgebra.commRing }

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.isOver_diagSpecIso_hom {R : CommRingCat} {M : Type u} [AddCommMonoid M] : Hom.IsOver (diagSpecIso R M).hom (Spec R)

instance AlgebraicGeometry.Scheme.isOver_diagSpecIso_inv {R : CommRingCat} {M : Type u} [AddCommMonoid M] : Hom.IsOver (diagSpecIso R M).inv (Spec R)

instance AlgebraicGeometry.Scheme.instIsMonHomOverSpecAsOverHomDiagSpecIso {R : CommRingCat} {M : Type u} [AddCommMonoid M] : CategoryTheory.IsMonHom (Hom.asOver (diagSpecIso R M).hom (Spec R))

instance AlgebraicGeometry.Scheme.instIsMonHomOverSpecAsOverInvDiagSpecIso {R : CommRingCat} {M : Type u} [AddCommMonoid M] : CategoryTheory.IsMonHom (Hom.asOver (diagSpecIso R M).inv (Spec R))

def AlgebraicGeometry.Scheme.diagPullbackIso {S T : Scheme} {M : Type u} [AddCommMonoid M] (f : T ⟶ S) : CategoryTheory.Limits.pullback f (S.Diag M ↘ S) ≅ T.Diag M

Diag is invariant under pullback.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.diagPullbackIso_hom_over {S T : Scheme} {M : Type u} [AddCommMonoid M] (f : T ⟶ S) : CategoryTheory.CategoryStruct.comp (diagPullbackIso f).hom (T.Diag M ↘ T) = CategoryTheory.Limits.pullback.fst f (S.Diag M ↘ S)

@[simp]

theorem AlgebraicGeometry.Scheme.diagPullbackIso_hom_over_assoc {S T : Scheme} {M : Type u} [AddCommMonoid M] (f : T ⟶ S) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (diagPullbackIso f).hom (CategoryTheory.CategoryStruct.comp (T.Diag M ↘ T) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (S.Diag M ↘ S)) h

@[simp]

theorem AlgebraicGeometry.Scheme.diagPullbackIso_inv_fst {S T : Scheme} {M : Type u} [AddCommMonoid M] (f : T ⟶ S) : CategoryTheory.CategoryStruct.comp (diagPullbackIso f).inv (CategoryTheory.Limits.pullback.fst f (S.Diag M ↘ S)) = T.Diag M ↘ T

@[simp]

theorem AlgebraicGeometry.Scheme.diagPullbackIso_inv_fst_assoc {S T : Scheme} {M : Type u} [AddCommMonoid M] (f : T ⟶ S) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (diagPullbackIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (S.Diag M ↘ S)) h) = CategoryTheory.CategoryStruct.comp (T.Diag M ↘ T) h

instance AlgebraicGeometry.Scheme.locallyOfFiniteType_diag {S : Scheme} {M : Type u} [AddCommMonoid M] [AddMonoid.FG M] : LocallyOfFiniteType (S.Diag M ↘ S)

@[simp]

theorem AlgebraicGeometry.Scheme.locallyOfFiniteType_diag_iff {S : Scheme} {M : Type u} [AddCommMonoid M] [hS : Nonempty ↥S] : LocallyOfFiniteType (S.Diag M ↘ S) ↔ AddMonoid.FG M

def AlgebraicGeometry.Scheme.diagFunctor (S : Scheme) : CategoryTheory.Functor AddCommGrpCatᵒᵖ (CategoryTheory.Grp (CategoryTheory.Over S))

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.diagFunctor_obj {S : Scheme} (M : AddCommGrpCatᵒᵖ) : S.diagFunctor.obj M = { X := (S.Diag ↑(Opposite.unop M)).asOver S, grp := Diag.grpObjAsOver }

@[simp]

theorem AlgebraicGeometry.Scheme.diagFunctor_map {S : Scheme} {M N : AddCommGrpCatᵒᵖ} (f : M ⟶ N) : S.diagFunctor.map f = { hom := Hom.asOver (Diag.map S (AddCommGrpCat.Hom.hom f.unop)) S, isMonHom_hom := ⋯ }

instance AlgebraicGeometry.Scheme.instIsCommMonObjOverXObjOppositeAddCommMonCatMonDiagMonFunctor {S : Scheme} (M : AddCommMonCatᵒᵖ) : CategoryTheory.IsCommMonObj (S.diagMonFunctor.obj M).X

instance AlgebraicGeometry.Scheme.instIsCommMonObjOverXObjOppositeAddCommGrpCatGrpDiagFunctor {S : Scheme} (M : AddCommGrpCatᵒᵖ) : CategoryTheory.IsCommMonObj (S.diagFunctor.obj M).X

@[simp]

theorem AlgebraicGeometry.Scheme.commHopfAlgCatEquivCogrpCommAlgCat_functor_map_ofHom_mul {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [HopfAlgebra R S] [HopfAlgebra R T] [Coalgebra.IsCocomm R S] (f g : S →ₐc[R] T) : (commHopfAlgCatEquivCogrpCommAlgCat R).functor.map (CommHopfAlgCat.ofHom (f * g)) = (((commHopfAlgCatEquivCogrpCommAlgCat R).functor.map (CommHopfAlgCat.ofHom f)).unop * ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.map (CommHopfAlgCat.ofHom g)).unop).op

theorem AlgebraicGeometry.Scheme.diagFunctor_map_add {S : Scheme} {M N : Type u} [AddCommGroup M] [AddCommGroup N] (f g : M →+ N) : S.diagFunctor.map (AddCommGrpCat.ofHom (f + g)).op = S.diagFunctor.map (AddCommGrpCat.ofHom f).op * S.diagFunctor.map (AddCommGrpCat.ofHom g).op

def AlgebraicGeometry.Scheme.diagMonFunctorIso (R : CommRingCat) : (Spec R).diagMonFunctor ≅ AddCommMonCat.equivalence.functor.op.comp ((commMonAlg ↑R).op.comp (bialgSpec R))

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.diagMonFunctorIso_app {R : CommRingCat} (M : AddCommMonCatᵒᵖ) : ((diagMonFunctorIso R).app M).hom.hom.left = (diagSpecIso R ↑(Opposite.unop M)).hom

def AlgebraicGeometry.Scheme.diagFunctorIso (R : CommRingCat) : (Spec R).diagFunctor ≅ commGroupAddCommGroupEquivalence.inverse.op.comp ((commGrpAlg ↑R).op.comp (hopfSpec R))

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.diagFunctorIso_app {R : CommRingCat} (M : AddCommGrpCatᵒᵖ) : ((diagFunctorIso R).app M).hom.hom.left = (diagSpecIso R ↑(Opposite.unop M)).hom

instance AlgebraicGeometry.Scheme.faithful_diagFunctor {R : Type u_1} [CommRing R] [Nontrivial R] : (Spec { carrier := R, commRing := inst✝ }).diagFunctor.Faithful

instance AlgebraicGeometry.Scheme.full_diagFunctor {R : Type u_1} [CommRing R] [IsDomain R] : (Spec { carrier := R, commRing := inst✝ }).diagFunctor.Full

def AlgebraicGeometry.Scheme.HomGrp (G G' S : Scheme) [G.Over S] [G'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] : Type u

Equations

• G.HomGrp G' S = Additive ({ X := G.asOver S, grp := inst✝¹ } ⟶ { X := G'.asOver S, grp := inst✝ })

instance AlgebraicGeometry.Scheme.instAddCommGroupHomGrpOfIsCommMonObjOverAsOver {G G' S : Scheme} [G.Over S] [G'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.IsCommMonObj (G'.asOver S)] : AddCommGroup (G.HomGrp G' S)

Equations

• AlgebraicGeometry.Scheme.instAddCommGroupHomGrpOfIsCommMonObjOverAsOver = id inferInstance

def AlgebraicGeometry.Scheme.HomGrp.ofHom {G G' S : Scheme} [G.Over S] [G'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] (f : G ⟶ G') [Hom.IsOver f S] [CategoryTheory.IsMonHom (Hom.asOver f S)] : G.HomGrp G' S

Equations

• AlgebraicGeometry.Scheme.HomGrp.ofHom f = Additive.ofMul (CategoryTheory.Grp.homMk (AlgebraicGeometry.Scheme.Hom.asOver f S))

def AlgebraicGeometry.Scheme.HomGrp.hom {G G' S : Scheme} [G.Over S] [G'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] (f : G.HomGrp G' S) : G ⟶ G'

Equations

• f.hom = (Additive.toMul f).hom.left

@[simp]

theorem AlgebraicGeometry.Scheme.HomGrp.hom_ofHom {G G' S : Scheme} [G.Over S] [G'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] (f : G ⟶ G') [Hom.IsOver f S] [CategoryTheory.IsMonHom (Hom.asOver f S)] : (ofHom f).hom = f

theorem AlgebraicGeometry.Scheme.HomGrp.toHom_injective {G G' S : Scheme} [G.Over S] [G'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] : Function.Injective hom

theorem AlgebraicGeometry.Scheme.HomGrp.toHom_injective_iff {G G' S : Scheme} [G.Over S] [G'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] {a₁ a₂ : G.HomGrp G' S} : a₁ = a₂ ↔ a₁.hom = a₂.hom

def AlgebraicGeometry.Scheme.HomGrp.comp {G G' G'' S : Scheme} [G.Over S] [G'.Over S] [G''.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.GrpObj (G''.asOver S)] (f : G.HomGrp G' S) (g : G'.HomGrp G'' S) : G.HomGrp G'' S

Equations

• f.comp g = Additive.ofMul (CategoryTheory.CategoryStruct.comp (Additive.toMul f) (Additive.toMul g))

@[simp]

theorem AlgebraicGeometry.Scheme.HomGrp.hom_comp {G G' G'' S : Scheme} [G.Over S] [G'.Over S] [G''.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.GrpObj (G''.asOver S)] (f : G.HomGrp G' S) (g : G'.HomGrp G'' S) : (f.comp g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

theorem AlgebraicGeometry.Scheme.HomGrp.comp_add {G G' G'' S : Scheme} [G.Over S] [G'.Over S] [G''.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.GrpObj (G''.asOver S)] [CategoryTheory.IsCommMonObj (G'.asOver S)] [CategoryTheory.IsCommMonObj (G''.asOver S)] (f f' : G.HomGrp G' S) (g : G'.HomGrp G'' S) : (f + f').comp g = f.comp g + f'.comp g

@[simp]

theorem AlgebraicGeometry.Scheme.HomGrp.comp_zero {G G' G'' S : Scheme} [G.Over S] [G'.Over S] [G''.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.GrpObj (G''.asOver S)] [CategoryTheory.IsCommMonObj (G''.asOver S)] (f : G.HomGrp G' S) : f.comp 0 = 0

@[simp]

theorem AlgebraicGeometry.Scheme.HomGrp.zero_comp {G G' G'' S : Scheme} [G.Over S] [G'.Over S] [G''.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.GrpObj (G''.asOver S)] [CategoryTheory.IsCommMonObj (G'.asOver S)] [CategoryTheory.IsCommMonObj (G''.asOver S)] (f : G'.HomGrp G'' S) : comp 0 f = 0

theorem AlgebraicGeometry.Scheme.HomGrp.add_comp {G G' G'' S : Scheme} [G.Over S] [G'.Over S] [G''.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.GrpObj (G''.asOver S)] [CategoryTheory.IsCommMonObj (G''.asOver S)] (f : G.HomGrp G' S) (g g' : G'.HomGrp G'' S) : f.comp (g + g') = f.comp g + f.comp g'

instance AlgebraicGeometry.Scheme.instIsOverInvOfHom_toric {X Y S : Scheme} [X.Over S] [Y.Over S] (e : X ≅ Y) [Hom.IsOver e.hom S] : Hom.IsOver e.inv S

instance AlgebraicGeometry.Scheme.instIsMonHomOverAsOverInvOfHom_toric {X Y S : Scheme} [X.Over S] [Y.Over S] [CategoryTheory.MonObj (X.asOver S)] [CategoryTheory.MonObj (Y.asOver S)] (e : X ≅ Y) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : CategoryTheory.IsMonHom (Hom.asOver e.inv S)

instance AlgebraicGeometry.Scheme.instIsOverHomSymm_toric {X Y S : Scheme} [X.Over S] [Y.Over S] (e : X ≅ Y) [Hom.IsOver e.hom S] : Hom.IsOver e.symm.hom S

instance AlgebraicGeometry.Scheme.instIsMonHomOverAsOverHomSymm_toric {X Y S : Scheme} [X.Over S] [Y.Over S] [CategoryTheory.MonObj (X.asOver S)] [CategoryTheory.MonObj (Y.asOver S)] (e : X ≅ Y) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : CategoryTheory.IsMonHom (Hom.asOver e.symm.hom S)

instance AlgebraicGeometry.Scheme.instIsOverHomRefl_toric {X S : Scheme} [X.Over S] : Hom.IsOver (CategoryTheory.Iso.refl X).hom S

instance AlgebraicGeometry.Scheme.instIsMonHomOverAsOverHomRefl_toric {X S : Scheme} [X.Over S] [CategoryTheory.MonObj (X.asOver S)] : CategoryTheory.IsMonHom (Hom.asOver (CategoryTheory.Iso.refl X).hom S)

def AlgebraicGeometry.Scheme.HomGrp.congr {G G' H H' S : Scheme} [G.Over S] [G'.Over S] [H.Over S] [H'.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (G'.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] [CategoryTheory.GrpObj (H'.asOver S)] (e₁ : G ≅ G') (e₂ : H ≅ H') [CategoryTheory.IsCommMonObj (H.asOver S)] [CategoryTheory.IsCommMonObj (H'.asOver S)] [Hom.IsOver e₁.hom S] [CategoryTheory.IsMonHom (Hom.asOver e₁.hom S)] [Hom.IsOver e₂.hom S] [CategoryTheory.IsMonHom (Hom.asOver e₂.hom S)] : G.HomGrp H S ≃+ G'.HomGrp H' S

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Scheme.diagHomGrp (S : Scheme) {M N : Type u} [AddCommGroup M] [AddCommGroup N] (f : M →+ N) : (S.Diag N).HomGrp (S.Diag M) S

Equations

• S.diagHomGrp f = Additive.ofMul (have this := S.diagFunctor.map (AddCommGrpCat.ofHom f).op; this)

theorem AlgebraicGeometry.Scheme.diagHomGrp_comp {S : Scheme} {M N O : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup O] (f : M →+ N) (g : N →+ O) : (S.diagHomGrp g).comp (S.diagHomGrp f) = S.diagHomGrp (g.comp f)

theorem AlgebraicGeometry.Scheme.diagHomGrp_add {S : Scheme} {M N : Type u} [AddCommGroup M] [AddCommGroup N] (f g : M →+ N) : S.diagHomGrp (f + g) = S.diagHomGrp f + S.diagHomGrp g

def AlgebraicGeometry.Scheme.diagHomEquiv {R M N : Type u} [CommRing R] [IsDomain R] [AddCommGroup M] [AddCommGroup N] : (N →+ M) ≃+ ((Spec { carrier := R, commRing := inst✝ }).Diag M).HomGrp ((Spec { carrier := R, commRing := inst✝ }).Diag N) (Spec { carrier := R, commRing := inst✝ })

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.diagHomEquiv_apply {R M N : Type u} [CommRing R] [IsDomain R] [AddCommGroup M] [AddCommGroup N] (f : N →+ M) : diagHomEquiv f = (Spec { carrier := R, commRing := inst✝ }).diagHomGrp f

class AlgebraicGeometry.Scheme.IsDiagonalisable (S G : Scheme) [G.Over S] [CategoryTheory.GrpObj (G.asOver S)] : Prop

• existsIso : ∃ (A : Type u) (x : AddCommGroup A) (e : G ≅ S.Diag A) (x_1 : Hom.IsOver e.hom S), CategoryTheory.IsMonHom (Hom.asOver e.hom S)

theorem AlgebraicGeometry.Scheme.isDiagonalisable_iff (S G : Scheme) [G.Over S] [CategoryTheory.GrpObj (G.asOver S)] : S.IsDiagonalisable G ↔ ∃ (A : Type u) (x : AddCommGroup A) (e : G ≅ S.Diag A) (x_1 : Hom.IsOver e.hom S), CategoryTheory.IsMonHom (Hom.asOver e.hom S)

instance AlgebraicGeometry.Scheme.instIsDiagonalisableDiag {S : Scheme} {A : Type u} [AddCommGroup A] : S.IsDiagonalisable (S.Diag A)

theorem AlgebraicGeometry.Scheme.IsDiagonalisable.of_iso {S G H : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] [S.IsDiagonalisable H] (e : G ≅ H) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : S.IsDiagonalisable G

theorem AlgebraicGeometry.Scheme.IsDiagonalisable.of_isIso {S G H : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] [S.IsDiagonalisable H] (f : G ⟶ H) [CategoryTheory.IsIso f] [Hom.IsOver f S] [CategoryTheory.IsMonHom (Hom.asOver f S)] : S.IsDiagonalisable G

instance AlgebraicGeometry.Scheme.instIsDiagonalisableSpecOfAddMonoidAlgebraCarrier {R : CommRingCat} {A : Type u} [AddCommGroup A] : (Spec R).IsDiagonalisable (Spec { carrier := AddMonoidAlgebra (↑R) A, commRing := AddMonoidAlgebra.commRing })

theorem AlgebraicGeometry.Scheme.isDiagonalisable_iff_span_isGroupLikeElem_eq_top {R : CommRingCat} {G : Scheme} [G.Over (Spec R)] [CategoryTheory.GrpObj (G.asOver (Spec R))] [IsDomain ↑R] [IsAffine G] : (Spec R).IsDiagonalisable G ↔ Submodule.span ↑R {a : ↑(G.presheaf.obj (Opposite.op ⊤)) | IsGroupLikeElem (↑R) a} = ⊤

An affine algebraic group G over a domain R is diagonalisable iff it is affine and Γ(G) is R-spanned by its group-like elements.

Note that this is more generally true over arbitrary commutative rings, but we do not prove that. See SGA III, Exposé VIII for more info.

Note that more generally a not necessarily affine algebraic group G over a field K is diagonalisable iff it is affine and Γ(G) is K-spanned by its group-like elements, but we do not prove that.