ModuleFiniteCharacterSheaf.lean
Nyll.EtaleFundamentalGroups.Cohomology.FiniteCharacterSheaf
4 declarations indexed from sourceView source ↗ Module documentation
An actual finite étale sheaf extension constructed from a character
The triangular representation on A × End(A) descends to a short exact sequence of actual étale abelian sheaves. The two end terms have trivial monodromy; the middle term retains the given character. All exactness statements follow from the explicit inclusion and projection.
Declarations
EtaleFundamentalGroups.Cohomology.trivialAdditiveAction
DocumentationThe trivial action on an additive group, with the original additive structure.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
EtaleFundamentalGroups.Cohomology.characterExtension_inclusion_projection_zero
DocumentationThe kernel inclusion followed by the quotient projection is zero.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
EtaleFundamentalGroups.Cohomology.characterExtension_inclusion_projection_shortExact
DocumentationThe original inclusion and projection form a short exact sequence of abelian groups.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
EtaleFundamentalGroups.Cohomology.finiteCharacterSheafSequence
DocumentationThe finite sheaf sequence obtained by descending the explicit triangular representation, together with its proved short exactness. The same local actions and topologies are shared by the construction and its proof.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
{Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
(A : Type u) [AddCommGroup A] [Fintype A] [TopologicalSpace A] [DiscreteTopology A]
(χ : Aut (FiniteEtale.fiber ξ) →ₜ* Multiplicative A)