EtaleFundamentalGroups.Cohomology.h1Character_pointedSchemePullback
Actual geometric H¹ pullback corresponds to the map on actual fundamental groups defined by any specified pointed fiber comparison.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable (f : X ⟶ Y) (A : AddCommGrpCat.{u}) [Finite A]
variable {Ω Ω' : Type u} [Field Ω] [IsSepClosed Ω] [Field Ω'] [IsSepClosed Ω']
variable (ξ : Spec (.of Ω) ⟶ X) (η : Spec (.of Ω') ⟶ Y)
variable (t : FiniteEtale.pullback f ⋙ FiniteEtale.fiber ξ ≅ FiniteEtale.fiber η)Lean source · full declaration
theorem h1Character_pointedSchemePullback
(a : Sheaf.H.{u} ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A) 1) :
let : TopologicalSpace (Multiplicative A) := ⊥
(h1Character A η a).comp (autHomOfCompIso (FiniteEtale.pullback f) t) =
h1Character A ξ (constantCohomologyPullback f A 1 a) := by
let : TopologicalSpace (Multiplicative A) := ⊥
let c := FiniteEtale.pullbackFiberIso f ξ
let τ := c.symm ≪≫ t
have ht : c ≪≫ τ = t := by
change c ≪≫ (c.symm ≪≫ t) = t
rw [← Iso.trans_assoc, Iso.self_symm_id, Iso.refl_trans]
have hg (g : Aut (FiniteEtale.fiber ξ)) :
autHomOfCompIso (FiniteEtale.pullback f) t g =
continuousConjAut τ (FiniteEtale.fundamentalGroupHom f ξ g) := by
let b := ((Functor.whiskeringLeft _ _ FintypeCat).obj
(FiniteEtale.pullback f)).mapAut (FiniteEtale.fiber ξ) g
change t.conjAut b = τ.conjAut (c.conjAut b)
exact (congrArg (fun e => e.conjAut b) ht.symm).trans
(Iso.trans_conjAut c τ b)
apply ContinuousMonoidHom.ext
intro g
change h1Character A η a (autHomOfCompIso (FiniteEtale.pullback f) t g) = _
rw [hg]
have hb := congrArg
(fun χ : Aut (FiniteEtale.fiber (ξ ≫ f)) →ₜ* Multiplicative A =>
χ (FiniteEtale.fundamentalGroupHom f ξ g))
(h1Character_basePoint A (ξ ≫ f) η τ a)
have hp := congrArg
(fun χ : Aut (FiniteEtale.fiber ξ) →ₜ* Multiplicative A => χ g)
(h1Character_schemePullback f A ξ a)
exact hb.trans hp