Contravariance of Hom cocycles in a presentation #
A commutative square between presenting arrows induces precomposition on Hom
cocycles modulo coboundaries. These maps reverse composition of squares and
commute with postcomposition in the coefficient module. They provide the
presentation variable of the cocycle model of Ext¹.
theorem
LinearMap.homCocyclePrecomp_mem
{k : Type u_1}
{A : Type u_2}
{P₀ : Type u_3}
{P₁ : Type u_4}
{Q₀ : Type u_5}
{Q₁ : Type u_6}
{N : Type u_7}
[CommRing k]
[Ring A]
[Algebra k A]
[AddCommGroup P₀]
[Module A P₀]
[AddCommGroup P₁]
[Module A P₁]
[AddCommGroup Q₀]
[Module A Q₀]
[AddCommGroup Q₁]
[Module A Q₁]
[AddCommGroup N]
[Module A N]
[Module k N]
[IsScalarTower k A N]
{p : P₁ →ₗ[A] P₀}
{q : Q₁ →ₗ[A] Q₀}
(f₀ : P₀ →ₗ[A] Q₀)
(f₁ : P₁ →ₗ[A] Q₁)
(hf : f₀ ∘ₗ p = q ∘ₗ f₁)
(h : ↥(lcomp k N q.ker.subtype).ker)
:
Precomposition by a presentation square preserves the Hom cocycle condition.
def
LinearMap.homCocycleQuotientPrecomp
{k : Type u_1}
{A : Type u_2}
{P₀ : Type u_3}
{P₁ : Type u_4}
{Q₀ : Type u_5}
{Q₁ : Type u_6}
{N : Type u_7}
[CommRing k]
[Ring A]
[Algebra k A]
[AddCommGroup P₀]
[Module A P₀]
[AddCommGroup P₁]
[Module A P₁]
[AddCommGroup Q₀]
[Module A Q₀]
[AddCommGroup Q₁]
[Module A Q₁]
[AddCommGroup N]
[Module A N]
[Module k N]
[IsScalarTower k A N]
{p : P₁ →ₗ[A] P₀}
{q : Q₁ →ₗ[A] Q₀}
(f₀ : P₀ →ₗ[A] Q₀)
(f₁ : P₁ →ₗ[A] Q₁)
(hf : f₀ ∘ₗ p = q ∘ₗ f₁)
:
Precomposition by a presentation square on Hom cocycles modulo coboundaries.
Instances For
@[simp]
theorem
LinearMap.homCocycleQuotientPrecomp_mk
{k : Type u_1}
{A : Type u_2}
{P₀ : Type u_3}
{P₁ : Type u_4}
{Q₀ : Type u_5}
{Q₁ : Type u_6}
{N : Type u_7}
[CommRing k]
[Ring A]
[Algebra k A]
[AddCommGroup P₀]
[Module A P₀]
[AddCommGroup P₁]
[Module A P₁]
[AddCommGroup Q₀]
[Module A Q₀]
[AddCommGroup Q₁]
[Module A Q₁]
[AddCommGroup N]
[Module A N]
[Module k N]
[IsScalarTower k A N]
{p : P₁ →ₗ[A] P₀}
{q : Q₁ →ₗ[A] Q₀}
(f₀ : P₀ →ₗ[A] Q₀)
(f₁ : P₁ →ₗ[A] Q₁)
(hf : f₀ ∘ₗ p = q ∘ₗ f₁)
(h : ↥(lcomp k N q.ker.subtype).ker)
:
(homCocycleQuotientPrecomp f₀ f₁ hf) (Submodule.Quotient.mk h) = Submodule.Quotient.mk ⟨↑h ∘ₗ f₁, ⋯⟩
Precomposition sends a cocycle class to the class of the composite.
@[simp]
theorem
LinearMap.homCocycleQuotientPrecomp_id
{k : Type u_1}
{A : Type u_2}
{P₀ : Type u_3}
{P₁ : Type u_4}
{N : Type u_7}
[CommRing k]
[Ring A]
[Algebra k A]
[AddCommGroup P₀]
[Module A P₀]
[AddCommGroup P₁]
[Module A P₁]
[AddCommGroup N]
[Module A N]
[Module k N]
[IsScalarTower k A N]
{p : P₁ →ₗ[A] P₀}
:
The identity square preserves Hom cocycle classes.
@[simp]
theorem
LinearMap.homCocycleQuotientPrecomp_comp_precomp
{k : Type u_1}
{A : Type u_2}
{P₀ : Type u_3}
{P₁ : Type u_4}
{Q₀ : Type u_5}
{Q₁ : Type u_6}
{N : Type u_7}
[CommRing k]
[Ring A]
[Algebra k A]
[AddCommGroup P₀]
[Module A P₀]
[AddCommGroup P₁]
[Module A P₁]
[AddCommGroup Q₀]
[Module A Q₀]
[AddCommGroup Q₁]
[Module A Q₁]
[AddCommGroup N]
[Module A N]
[Module k N]
[IsScalarTower k A N]
{p : P₁ →ₗ[A] P₀}
{q : Q₁ →ₗ[A] Q₀}
{R₀ : Type u_8}
{R₁ : Type u_9}
[AddCommGroup R₀]
[Module A R₀]
[AddCommGroup R₁]
[Module A R₁]
{r : R₁ →ₗ[A] R₀}
(f₀ : P₀ →ₗ[A] Q₀)
(f₁ : P₁ →ₗ[A] Q₁)
(hf : f₀ ∘ₗ p = q ∘ₗ f₁)
(g₀ : Q₀ →ₗ[A] R₀)
(g₁ : Q₁ →ₗ[A] R₁)
(hg : g₀ ∘ₗ q = r ∘ₗ g₁)
:
homCocycleQuotientPrecomp f₀ f₁ hf ∘ₗ homCocycleQuotientPrecomp g₀ g₁ hg = homCocycleQuotientPrecomp (g₀ ∘ₗ f₀) (g₁ ∘ₗ f₁) ⋯
Precomposition reverses composition of presentation squares.
@[simp]
theorem
LinearMap.homCocycleQuotientPrecomp_map
{k : Type u_1}
{A : Type u_2}
{P₀ : Type u_3}
{P₁ : Type u_4}
{Q₀ : Type u_5}
{Q₁ : Type u_6}
{N : Type u_7}
[CommRing k]
[Ring A]
[Algebra k A]
[AddCommGroup P₀]
[Module A P₀]
[AddCommGroup P₁]
[Module A P₁]
[AddCommGroup Q₀]
[Module A Q₀]
[AddCommGroup Q₁]
[Module A Q₁]
[AddCommGroup N]
[Module A N]
[Module k N]
[IsScalarTower k A N]
{p : P₁ →ₗ[A] P₀}
{q : Q₁ →ₗ[A] Q₀}
{N' : Type u_8}
[AddCommGroup N']
[Module A N']
[Module k N']
[IsScalarTower k A N']
(f₀ : P₀ →ₗ[A] Q₀)
(f₁ : P₁ →ₗ[A] Q₁)
(hf : f₀ ∘ₗ p = q ∘ₗ f₁)
(g : N →ₗ[A] N')
(x : q.HomCocycleQuotient N)
:
(homCocycleQuotientPrecomp f₀ f₁ hf) ((q.homCocycleQuotientMap g) x) = (p.homCocycleQuotientMap g) ((homCocycleQuotientPrecomp f₀ f₁ hf) x)
Precomposition in a presentation commutes with postcomposition in the coefficients.