mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ cocyclesMap f φ 1 ≫ (isoCocycles₁ B).hom = (isoCocycles₁ A).hom ≫ mapCocycles₁ f φ

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
φ : res 1 A ⟶ B
⊢ mapCocycles₁ 1 φ = 0

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ H1π A ≫ map f φ 1 = mapCocycles₁ f φ ≫ H1π B

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
φ : res 1 A ⟶ B
⊢ map 1 φ 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₁ X.X₁).inv) x)) x✝ =
    ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ X.X₂).inv) y)) x✝

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ConcreteCategory.hom (δ hX 2 1 ⋯)) ((ConcreteCategory.hom (H2π X.X₃)) z) = (ConcreteCategory.hom (H1π X.X₁)) ⟨x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ M.tateNorm = ModuleCat.ofHom ((Finsupp.lsum R) fun x ↦ LinearMap.pi fun x ↦ M.ρ.norm)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ Hom.toModuleCatHom M.norm ≫ d₀₁ M = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ M.tateNorm ≫ (inhomogeneousCochains M).d 0 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ d₁₀ M ≫ Hom.toModuleCatHom M.norm = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ (inhomogeneousChains M).d 1 0 ≫ M.tateNorm = 0

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx :
  (ConcreteCategory.hom (H1π (of A.ρ)))
      ((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)))) x) =
    0
y : ↑(ModuleCat.of k ↑(of A.ρ))
hy :
  (ModuleCat.Hom.hom (d₀₁ (of A.ρ))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)))) x)
g✝ : G ⧸ S
g : G
⊢ ↑((ModuleCat.Hom.hom (d₀₁ (A.quotientToInvariants S))) ⟨y, ⋯⟩ ↑g) = ↑(x ↑g)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X Y : Rep R G
φ : X ⟶ Y
⊢ tateComplex X ⟶ tateComplex Y

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
⊢ map 0 = 0

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ Mono (H1InfRes A S).f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
⊢ map (f + g) = map f + map g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X : Rep R G
Y : Rep R G
X✝ Y✝ Z✝ : Rep R G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ tateComplex.map (f ≫ g) = tateComplex.map f ≫ tateComplex.map g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X✝ : Rep R G
Y✝ : Rep R G
X Y : Rep R G
⊢ (tateComplexFunctor R G).map 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
⊢ (S.map (tateComplexFunctor R G)).ShortExact

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝³ : CommRing R
inst✝² : Group G
inst✝¹ : Fintype G
M : Rep R G
X✝ : Rep R G
Y✝ : Rep R G
n : ℕ
inst✝ : NeZero n
X Y : Rep R G
f : X ⟶ Y
⊢ (tateCohomologyFunctor ↑n).map f ≫ ((tateComplexConnectData Y).homologyIsoPos n ↑n ⋯).hom =
    ((tateComplexConnectData X).homologyIsoPos n ↑n ⋯).hom ≫ (groupCohomology.functor R G n).map f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝³ : CommRing R
inst✝² : Group G
inst✝¹ : Fintype G
M : Rep R G
X✝ : Rep R G
Y✝ : Rep R G
m : ℤ
n : ℕ
hmn : m = -(↑n + 1)
inst✝ : NeZero n
X Y : Rep R G
f : X ⟶ Y
⊢ (tateCohomologyFunctor m).map f ≫ ((tateComplexConnectData Y).homologyIsoNeg n m hmn).hom =
    ((tateComplexConnectData X).homologyIsoNeg n m hmn).hom ≫ (groupHomology.functor R G n).map f

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g : G
s : ↥S
⊢ ((MonoidHom.comp A.ρ S.subtype) s) (↑x g - (A.ρ g) y + y) = x (↑s * g) - x ↑s - (A.ρ ↑s) ((A.ρ g) y) + (x ↑s + y)

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g : G
s : ↥S
⊢ x (↑s * g) - x ↑s - (A.ρ ↑s) ((A.ρ g) y) + (x ↑s + y) =
    x (g * (g⁻¹ * ↑s * g)) - (A.ρ g) ((A.ρ (g⁻¹ * ↑s * g)) y - y) - (A.ρ g) y + y

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g : G
s : ↥S
⊢ x (g * (g⁻¹ * ↑s * g)) - (A.ρ g) ((A.ρ (g⁻¹ * ↑s * g)) y - y) - (A.ρ g) y + y = x g - (A.ρ g) y + y

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
⊢ InducedCategory.homMk (↟(X.ρ g)) ≫ InducedCategory.homMk (↟(X.ρ g⁻¹)) = 𝟙 X.V

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
⊢ InducedCategory.homMk (↟(X.ρ g⁻¹)) ≫ InducedCategory.homMk (↟(X.ρ g)) = 𝟙 X.V

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
⊢ ∀ (X Y : FDRep k G),
    Functor.LaxMonoidal.μ (forget k G).toFunctor X Y ≫ (equivApp g (X ⊗ Y)).hom =
      ((equivApp g X).hom ⊗ₘ (equivApp g Y).hom) ≫ Functor.LaxMonoidal.μ (forget k G).toFunctor X Y

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯ = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp (x✝¹ * x✝)) ⋯ ⋯ ⋯ =
    LaxMonoidalFunctor.isoOfComponents (equivApp x✝¹) ⋯ ⋯ ⋯ * LaxMonoidalFunctor.isoOfComponents (equivApp x✝) ⋯ ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
⊢ { toFun := fun f t ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ } = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun f t ↦ f (t * (x✝¹ * x✝)), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun f t ↦ f (t * x✝¹), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun f t ↦ f (t * x✝), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
⊢ { toFun := fun f t ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun f t ↦ f ((x✝¹ * x✝)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun f t ↦ f (x✝¹⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun f t ↦ f (x✝⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Nontrivial k
⊢ Function.Injective ⇑(equivHom k G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∀ (g : G),
    (rightFDRep ⊗ rightFDRep).ρ g ≫ InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) =
      InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) ≫ rightFDRep.ρ g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
this : α (α_inv 1) = 1
⊢ α 1 = 1

Tactic:
by

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ (H1InfRes A S).Exact

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
⊢ (G → k) →ₐ[k] G → k

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
x✝¹ x✝ : G → k
⊢ ∑ s, (x✝¹ + x✝) s • (X.ρ s⁻¹) v = ∑ s, x✝¹ s • (X.ρ s⁻¹) v + ∑ s, x✝ s • (X.ρ s⁻¹) v

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
x✝¹ : k
x✝ : G → k
⊢ ∑ s, (x✝¹ • x✝) s • (X.ρ s⁻¹) v = (RingHom.id k) x✝¹ • ∑ s, x✝ s • (X.ρ s⁻¹) v

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
X : FDRep k G
v : ↑X.V
⊢ ∑ s, single 1 1 s • (X.ρ s⁻¹) v = v

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
⊢ cochainsMap₁ f φ ≫ (shortComplexH2 B).f = (shortComplexH2 A).f ≫ cochainsMap₂ f φ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
t : G
⊢ rightFDRep.ρ t ≫ InducedCategory.homMk (↟(sumSMulInv v)) = InducedCategory.homMk (↟(sumSMulInv v)) ≫ X.ρ t

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
⊢ cochainsMap₂ f φ ≫ (shortComplexH2 B).g = (shortComplexH2 A).g ≫ cochainsMap₃ f φ

Tactic:
by

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

Goal state before:
pp: k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ mapShortComplexH2 (MonoidHom.id H) (𝟙 A) = 𝟙 (shortComplexH2 A)

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ mapCocycles₂ f φ ≫ (shortComplexH2 B).moduleCatLeftHomologyData.i =
    (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ cochainsMap₂ f φ

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ cocyclesMap f φ 2 ≫ (isoCocycles₂ B).hom = (isoCocycles₂ A).hom ≫ mapCocycles₂ f φ

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ H2π A ≫ map f φ 2 = mapCocycles₂ f φ ≫ H2π B

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ n : ℕ
X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ map (MonoidHom.id G) (x✝¹ ≫ x✝) n = map (MonoidHom.id G) x✝¹ n ≫ map (MonoidHom.id G) x✝ n

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ n : ℕ
x✝¹ x✝ : Rep k G
⊢ (functor k G n).map 0 = 0

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ✝ : res f A ⟶ B
n✝ n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ (functor k H n).map φ ≫ map f (𝟙 (res f Y)) n = map f (𝟙 (res f X)) n ≫ (resFunctor f ⋙ functor k G n).map φ

Tactic:
by

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ✝ : res f A ⟶ B
n✝ : ℕ
S : Subgroup G
inst✝ : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ (quotientToInvariantsFunctor k S ⋙ functor k (G ⧸ S) n).map φ ≫
      map (QuotientGroup.mk' S) (ofHom (Y.ρ.quotientToInvariants_lift S)) n =
    map (QuotientGroup.mk' S) (ofHom (X.ρ.quotientToInvariants_lift S)) n ≫ (functor k G n).map φ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
⊢ η₁ = η₂

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
s x✝ : G
⊢ rightFDRep.ρ x✝ ≫ InducedCategory.homMk (↟(leftRegular s)) =
    InducedCategory.homMk (↟(leftRegular s)) ≫ rightFDRep.ρ x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s ↦ (monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s ↦ (monomial s) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ s, (monomial si) 1 ∣ (monomial xi) (coeff xi x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
hs : (evalAlgHom k (fun a ↦ k) 1).comp (algHomOfRightFDRepComp η) = evalAlgHom k (fun i ↦ k) s
u t : G
nat :
  (forget k G).map (leftRegularFDRepHom t⁻¹) ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app rightFDRep ≫ (forget k G).map (leftRegularFDRepHom t⁻¹)
⊢ (Hom.hom (η.hom.hom.app (FDRep.of rightRegular)).hom) ((basisFun k G) u) t =
    (leftRegular t⁻¹) ((ConcreteCategory.hom (η.hom.hom.app rightFDRep).hom) (single u 1)) 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
hs : (evalAlgHom k (fun a ↦ k) 1).comp (algHomOfRightFDRepComp η) = evalAlgHom k (fun i ↦ k) s
u t : G
nat :
  (forget k G).map (leftRegularFDRepHom t⁻¹) ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app rightFDRep ≫ (forget k G).map (leftRegularFDRepHom t⁻¹)
⊢ (evalAlgHom k (fun a ↦ k) s) ((leftRegular t⁻¹) (single u 1)) = (rightRegular s) ((basisFun k G) u) t

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : σ →₀ ℕ
hx : x ∈ ⇑degree ⁻¹' Set.Ici 1
⊢ x.support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
⊢ ∃ s, Hom.hom (η.hom.hom.app rightFDRep).hom = rightRegular s

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
⊢ Function.Surjective ⇑(equivHom k G)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
c : σ →₀ ℕ
hx : c + single i 1 ∈ ⇑degree ⁻¹' Set.Ici 1
hi : i ∈ (c + single i 1).support
⊢ X i ∈ Set.range X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ idealOfVars σ R = restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ idealOfVars σ R ^ n = restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ idealOfVars σ R ^ n = Ideal.span ((fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' {n})

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ p ∈ idealOfVars σ R ^ n ↔ ∀ x ∈ p.support, n ≤ degree x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ p ∈ idealOfVars σ R ^ n ↔ ∀ (x : σ →₀ ℕ), degree x < n → coeff x p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
x : σ →₀ ℕ
r : R
h : r ≠ 0
⊢ (monomial x) r ∈ idealOfVars σ R ^ n ↔ n ≤ degree x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

Tactic:
by

Goal state after: