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
B : Rep k H
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ (resFunctor φ).obj Y✝
⊢ (indResHomEquiv φ X'✝ Y✝).symm (x✝¹ ≫ x✝) = (indFunctor k φ).map x✝¹ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝

Tactic:
ext

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝³ : X'✝ ⟶ X✝
x✝² : X✝ ⟶ (resFunctor φ).obj Y✝
x✝¹ : H
x✝ : ↑X'✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indResHomEquiv φ X'✝ Y✝).symm (x✝³ ≫ x✝²))).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X'✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indFunctor k φ).map x✝³ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝²)).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X'✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
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
g : G
⊢ 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)) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g =
    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:
ext

Goal state after:
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
g : G
x✝² : H
x✝¹ : ↑A
x✝ : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (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)) ∘ₗ
                (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (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))) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝
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:
ext

Goal state after:
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✝¹ : ↑A
x✝ : ↑(res φ B)
⊢ (((A.coinvariantsTensorMk (res φ B)).compr₂
          (ModuleCat.Hom.hom (coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B)))
        x✝¹)
      x✝ =
    (((A.coinvariantsTensorMk (res φ B)).compr₂
          (ModuleCat.Hom.hom (𝟙 (((coinvariantsTensor k G).obj A).obj (res φ B)))))
        x✝¹)
      x✝
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:
ext

Goal state after:
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
x✝² : H
x✝¹ : ↑A
x✝ : ↑X
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk X).compr₂
                  (ModuleCat.Hom.hom
                    (((coinvariantsTensor k H).obj (ind φ A)).map f ≫ (coinvariantsTensorIndIso φ A Y).hom)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk X).compr₂
                  (ModuleCat.Hom.hom
                    ((coinvariantsTensorIndIso φ A X).hom ≫ (resFunctor φ ⋙ (coinvariantsTensor k G).obj A).map f)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝
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:
ext

Goal state after:
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
x✝ : ↑A
⊢ x✝ ∈ A.ρ.invariants ↔ x✝ ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).ker
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:
ext

Goal state after:
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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:
ext

Goal state after:
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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:
ext

Goal state after:
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✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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:
ext

Goal state after:
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✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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:
ext

Goal state after:
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
a✝ : L
⊢ x a✝ = y a✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 0)) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y) =
    (ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g✝ : Fin 0 → G
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 0)) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)
      g✝ =
    (ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) (↑z) g✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ d₀₁ A = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : ↑(ModuleCat.of k ↑A)
x✝ : G
⊢ (ModuleCat.Hom.hom (d₀₁ A)) x✝¹ x✝ = (ModuleCat.Hom.hom 0) x✝¹ x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 1)) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y) =
    (ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) ⇑z

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g✝ : Fin 1 → G
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 1)) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y)
      g✝ =
    (ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) (⇑z) g✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
S : Subgroup G
A✝ : Rep.{?u.12, u, u} k ↥S
P : ProjectiveResolution (Rep.trivial k G k)
A : Rep.{u, u, u} k ↥S
x✝² x✝¹ : ℕ
x✝ : (ComplexShape.up ℕ).Rel x✝² x✝¹
f : ↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x✝²)
⊢ Hom.hom
      ((ModuleCat.Hom.hom
          ((resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝²) A).toModuleIso.hom ≫
            (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).d x✝² x✝¹))
        f) =
    Hom.hom
      ((ModuleCat.Hom.hom
          ((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).d x✝² x✝¹ ≫
            (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝¹) A).toModuleIso.hom))
        f)

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
S : Subgroup G
A✝ : Rep.{?u.12, u, u} k ↥S
P : ProjectiveResolution (Rep.trivial k G k)
A : Rep.{u, u, u} k ↥S
x✝⁴ x✝³ : ℕ
x✝² : (ComplexShape.up ℕ).Rel x✝⁴ x✝³
f : ↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x✝⁴)
x✝¹ : ↑(Opposite.unop (Opposite.op (P.complex.X x✝³)))
x✝ : G
⊢ ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝⁴) A).toModuleIso.hom ≫
                    (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).d x✝⁴ x✝³))
                f)).toLinearMap
          x✝¹)
      x✝ =
    ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).d x✝⁴ x✝³ ≫
                    (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝³) A).toModuleIso.hom))
                f)).toLinearMap
          x✝¹)
      x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
m n : ℕ
h : (ComplexShape.down ℕ).next m = n
f : (Fin m → G) →₀ ↑A
hf : (ConcreteCategory.hom ((inhomogeneousChains A).d m n)) f = 0
⊢ (ConcreteCategory.hom (iCycles A m)) (cyclesMk m n h f hf) = f

Tactic:
by
  exact (inhomogeneousChains A).i_cyclesMk f n h hf

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ d₀₁ A ≫ d₁₂ A = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝¹ : ↑(ModuleCat.of k ↑A)
x✝ : G × G
⊢ (ModuleCat.Hom.hom (d₀₁ A ≫ d₁₂ A)) x✝¹ x✝ = (ModuleCat.Hom.hom 0) x✝¹ x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G → A
hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)
⊢ IsCoboundary₁ f

Tactic:
rcases hf with ⟨a, rfl⟩
  exact ⟨a, fun _ => rfl⟩

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
⊢ f 1 = 1

Tactic:
by
  simpa only [mul_one, one_smul, left_eq_mul] using hf 1 1

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ (inhomogeneousCochains A).d 0 1 = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
i✝ : Fin 0 → G
x✝ : ↑A
g✝ : Fin 1 → G
⊢ (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1) ∘ₗ LinearMap.single k (fun i ↦ ↑A) i✝) x✝ g✝ =
    (ModuleCat.Hom.hom 0 ∘ₗ LinearMap.single k (fun i ↦ ↑A) i✝) x✝ g✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq 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:
ext

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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 i : ℕ
⊢ ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousCochains B).d i (i + 1) =
    (inhomogeneousCochains A).d i (i + 1) ≫
      ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x)

Tactic:
ext

Goal state after:
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 i : ℕ
x✝ : ↑((inhomogeneousCochains A).X i)
g✝ : Fin (i + 1) → G
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x) ≫
          (inhomogeneousCochains B).d i (i + 1)))
      x✝ g✝ =
    (ModuleCat.Hom.hom
        ((inhomogeneousCochains A).d i (i + 1) ≫
          ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x)))
      x✝ g✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq 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:
ext

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ

Tactic:
ext

Goal state after:
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f A)
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq 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:
ext

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq 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:
ext

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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 : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ

Tactic:
ext

Goal state after:
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 : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f A)
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝
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 →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ X.X₃).inv) ↑z) = 0

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]; simp

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

Goal state before:
pp: case e_6
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
x✝ : ↑((inhomogeneousCochains A).X 2)
g : G × G
x : Fin 2
⊢ (fun x ↦ ⇑f ∘ x) ((piFinTwoEquiv fun x ↦ G).symm g) x = (piFinTwoEquiv fun x ↦ H).symm (Prod.map (⇑f) (⇑f) g) x

Tactic:
fin_cases x

Goal state after:
case e_6.«0»
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
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (fun x ↦ ⇑f ∘ x) ((piFinTwoEquiv fun x ↦ G).symm g) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (piFinTwoEquiv fun x ↦ H).symm (Prod.map (⇑f) (⇑f) g) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_6.«1»
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
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (fun x ↦ ⇑f ∘ x) ((piFinTwoEquiv fun x ↦ G).symm g) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (piFinTwoEquiv fun x ↦ H).symm (Prod.map (⇑f) (⇑f) g) ((fun i ↦ i) ⟨1, ⋯⟩)