English
The exactness of the inflation-restriction sequence is preserved under simp simplifications.
Русский
Точность инфляции-ограничения сохраняется при упрощениях simp.
LaTeX
$$$\text{H1InfRes}_{\text{exact}}$$$
Lean4
/-- Given a `G`-representation `A` and a normal subgroup `S ≤ G`, the short complex
`H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A)` is exact. -/
theorem H1InfRes_exact : (H1InfRes A S).Exact :=
by
rw [moduleCat_exact_iff_ker_sub_range]
intro x hx
induction x using H1_induction_on with
| @h
x =>
simp_all only [H1InfRes_X₂, H1InfRes_X₃, H1InfRes_g, H1InfRes_X₁, LinearMap.mem_ker, H1π_comp_map_apply S.subtype,
H1InfRes_f]
rcases (H1π_eq_zero_iff _).1 hx with ⟨(y : A), hy⟩
have h1 := (mem_cocycles₁_iff x).1 x.2
have h2 : ∀ s ∈ S, x s = A.ρ s y - y := fun s hs => funext_iff.1 hy.symm ⟨s, hs⟩
refine ⟨H1π _ ⟨fun g => Quotient.liftOn' g (fun g => ⟨x.1 g - A.ρ g y + y, ?_⟩) ?_, ?_⟩, ?_⟩
· intro s
calc
_ = x (s * g) - x s - A.ρ s (A.ρ g y) + (x s + y) := by
simp [add_eq_of_eq_sub (h2 s s.2), sub_eq_of_eq_add (h1 s g)]
_ = x (g * (g⁻¹ * s * g)) - A.ρ g (A.ρ (g⁻¹ * s * g) y - y) - A.ρ g y + y :=
by
simp only [mul_assoc, mul_inv_cancel_left, map_mul, Module.End.mul_apply, map_sub,
Representation.self_inv_apply]
abel
_ = x g - A.ρ g y + y := by
simp [eq_sub_of_add_eq' (h1 g (g⁻¹ * s * g)).symm, h2 (g⁻¹ * s * g) (Subgroup.Normal.conj_mem' ‹_› _ s.2 _)]
· intro g h hgh
have := congr(A.ρ g $(h2 (g⁻¹ * h) <| QuotientGroup.leftRel_apply.1 hgh))
simp_all [← sub_eq_add_neg, sub_eq_sub_iff_sub_eq_sub]
· rw [mem_cocycles₁_iff]
intro g h
induction g using QuotientGroup.induction_on with
| @H g =>
induction h using QuotientGroup.induction_on with
| @H h =>
apply Subtype.ext
simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]
· symm
simp only [H1π_comp_map_apply, H1π_eq_iff (A := A)]
use y
ext g
simp [coe_mapCocycles₁ (QuotientGroup.mk' S), cocycles₁.coe_mk (A := A.quotientToInvariants S), ← sub_sub]
