Comodule over a Hopf algebroid

In mathematics, at the intersection of algebraic topology and algebraic geometry, there is the notion of a Hopf algebroid which encodes the information of a presheaf of groupoids whose object sheaf and arrow sheaf are represented by algebras. Because any such presheaf will have an associated site, we can consider quasi-coherent sheaves on the site, giving a topos-theoretic notion of modules. Duallypg 2, comodules over a Hopf algebroid are the purely algebraic analogue of this construction, giving a purely algebraic description of quasi-coherent sheaves on a stack: this is one of the first motivations behind the theory.
Definition.
Given a commutative Hopf-algebroid formula_1 a left comodule formula_2pg 302 is a left formula_3-module formula_2 together with an formula_3-linear mapformula_6which satisfies the following two properties
A right comodule is defined similarly, buy instead there is a mapformula_9satisfying analogous axioms.
Structure theorems.
Flatness of Γ gives an abelian category.
One of the main structure theorems for comodulespg 303 is if formula_10 is a flat formula_3-module, then the category of comodules formula_12 of the Hopf-algebroid is an Abelian category.
Relation to stacks.
There is a structure theorempg 7 relating comodules of Hopf-algebroids and modules of presheaves of groupoids. If formula_1 is a Hopf-algebroid, there is an equivalence between the category of comodules formula_12 and the category of quasi-coherent sheaves formula_15 for the associated presheaf of groupoidsformula_16to this Hopf-algebroid.
Examples.
From BP-homology.
Associated to the Brown-Peterson spectrum is the Hopf-algebroid formula_17 classifying p-typical formal group laws. Noteformula_18where formula_19 is the localization of formula_20 by the prime ideal formula_21. If we let formula_22 denote the idealformula_23Since formula_24 is a primitive in formula_25, there is an associated Hopf-algebroid formula_1formula_27There is a structure theorem on the Adams-Novikov spectral sequence relating the Ext-groups of comodules on formula_17 to Johnson-Wilson homology, giving a more tractable spectral sequence. This happens through an equivalence of categories of comodules of formula_1 to the category of comodules of formula_30giving the isomorphismformula_31assuming formula_2 and formula_33 satisfy some technical hypothesespg 24.