mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x✝ : H
⊢ TensorProduct.lift
        (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
          (TensorProduct.lift
            (((lift
                  (↑A →ₗ[k] ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                  k H)
                fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
              ↑(MonoidAlgebra.coeffLinearEquiv k)))
          ⋯) ∘ₗ
      (((MonoidalCategory.curriedTensor (Rep k H)).obj (ind φ A)).obj B).ρ x✝ =
    TensorProduct.lift
      (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (TensorProduct.lift
          (((lift (↑A →ₗ[k] ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                k H)
              fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
            ↑(MonoidAlgebra.coeffLinearEquiv k)))
        ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
inst✝² : CommRing k
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
x : ↑A
y : ↑B
⊢ (ConcreteCategory.hom (coinvariantsTensorIndHom φ A B))
      ((((ind φ A).coinvariantsTensorMk B) ((IndV.mk φ A.ρ h) x)) y) =
    ((A.coinvariantsTensorMk (res φ B)) x) ((B.ρ h) y)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
x : ↑A
y : ↑B
⊢ (((Representation.ind φ A.ρ).tprod B.ρ) (φ s)) ((IndV.mk φ A.ρ 1) x ⊗ₜ[k] y) - (IndV.mk φ A.ρ 1) x ⊗ₜ[k] y =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] (A.ρ s) x) ⊗ₜ[k]
        (B.ρ (φ s)) y -
      (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] x) ⊗ₜ[k]
        y

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ s =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)

Tactic:
simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, tprod_apply,
      MonoidHom.coe_comp, Function.comp_apply]
    ext x y
    simpa [Coinvariants.mk_eq_iff, coinvariantsTensorMk] using
      Coinvariants.mem_ker_of_eq (φ s) (IndV.mk φ A.ρ (1 : H) x ⊗ₜ[k] y) _ <| by
      simp [← Coinvariants.mk_inv_tmul]

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ s =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
inst✝² : CommRing k
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x : ↑A
y : ↑B
⊢ (ConcreteCategory.hom (coinvariantsTensorIndInv φ A B)) ((Coinvariants.mk (A.ρ.tprod (res φ B).ρ)) (x ⊗ₜ[k] y)) =
    (((ind φ A).coinvariantsTensorMk B) ((IndV.mk φ A.ρ 1) x)) y

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
a : ↑A
b : ↑B
⊢ (((Representation.ind φ A.ρ).tprod B.ρ) h) ((IndV.mk φ A.ρ h) a ⊗ₜ[k] b) - (IndV.mk φ A.ρ h) a ⊗ₜ[k] b =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] a) ⊗ₜ[k]
        (B.ρ h) b -
      (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single h 1 ⊗ₜ[k] a) ⊗ₜ[k]
        b

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
⊢ coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B = 𝟙 (((coinvariantsTensor k H).obj (ind φ A)).obj B)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
⊢ coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B = 𝟙 (((coinvariantsTensor k G).obj A).obj (res φ B))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X Y : Rep k H
f : X ⟶ Y
⊢ ((coinvariantsTensor k H).obj (ind φ A)).map f ≫ (coinvariantsTensorIndIso φ A Y).hom =
    (coinvariantsTensorIndIso φ A X).hom ≫ (resFunctor φ ⋙ (coinvariantsTensor k G).obj A).map f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ ∀ (i j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i j =
        ((resolution k g hg).complex.linearYonedaObj k A).d i j ≫ A.leftRegularHomEquiv.toModuleIso.hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ A.ρ.invariants = (Hom.hom (A.applyAsHom g - 𝟙 A)).ker

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ∀ (i j : ℕ), (ComplexShape.up ℕ).Rel i j → Odd (i + j)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.up ℕ).Rel i ((ComplexShape.up ℕ).next i)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ (Hom.hom A.norm).range

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) x =
      (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Hom.hom A.norm).range

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ ∀ (i j : ℕ), (ComplexShape.up ℕ).Rel i j → Odd (i + j)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ (ComplexShape.up ℕ).Rel i ((ComplexShape.up ℕ).next i)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) x =
      (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
x y : Gal(L/K)
h : (fun f ↦ ↑f) x = (fun f ↦ ↑f) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
⊢ aux f z = ∑ h, ↑(f h) * h z

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
⊢ IsMulCoboundary₁ f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : ↑(H1 (Rep.ofAlgebraAutOnUnits K L))
x : ↥(cocycles₁ (Rep.ofAlgebraAutOnUnits K L))
⊢ ⇑x ∈ coboundaries₁ (Rep.ofAlgebraAutOnUnits K L)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
⊢ (cechNerveTerminalFrom (Action.ofMulAction G G)).map f ≫
      (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom =
    (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫ (classifyingSpaceUniversalCover G).map f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : Lˣ
⊢ ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul x))))) =
    (algebraMap K L) ((Algebra.norm K) ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ cechNerveTerminalFrom G ≅ classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (↾fun x ↦ 1) ≫ (Arrow.mk (terminal.from G)).hom = 𝟙 (Arrow.mk (terminal.from G)).right

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
⊢ (Algebra.norm K) x⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (𝟭 (SimplicialObject (Type u))).map (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G).hom ≫
      (compForgetAugmented G).hom =
    (Arrow.mk (terminal.from G)).augmentedCechNerve.hom ≫
      (SimplicialObject.const (Type u)).map (Iso.refl (Arrow.mk (terminal.from G)).augmentedCechNerve.right).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (compForgetAugmented G).ExtraDegeneracy

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
⊢ (d k G n) (MonoidAlgebra.single c 1) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) ((-1) ^ ↑p)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (MonoidAlgebra.single c r) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r * (-1) ^ ↑p)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
n : ℕ
⊢ Projective ((standardComplex k G).X n)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)).toLinearMap = d k G (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
⊢ ∃ y, ↑y / g ↑y = x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)) f = (d k G (n + 1)) f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x✝¹ : G
x✝ : Fin 1 → G
⊢ ((((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
          (Representation.ofMulAction k G (Fin 1 → G)) x✝¹) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    (((Representation.trivial k G k) x✝¹ ∘ₗ (linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 = (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (standardComplex k G).d 1 0 ≫ ε k G = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (trivial k G k) =
    (forget₂ToModuleCatHomotopyEquiv k G).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
⊢ Odd 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ QuasiIso (εToSingle₀ k G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
⊢ toAdditive.symm (ofMul xu) ∈ (Hom.hom (ofAlgebraAutOnUnits K L).norm).ker

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
x : Fin (n + 1) → G
⊢ (Hom.hom (d k G n)) (single x (MonoidAlgebra.single 1 1)) =
    single (fun i ↦ x i.succ) (MonoidAlgebra.single (x 0) 1) +
      ∑ j, single (j.contractNth (fun x1 x2 ↦ x1 * x2) x) (MonoidAlgebra.single 1 ((-1) ^ (↑j + 1)))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
⊢ MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1

Tactic:
by

Goal state after: