instance ProjectiveCoverInfra.endFiniteDimensional (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] (X : C) [FiniteDimensional 𝕜 (X ⟶ X)] : FiniteDimensional 𝕜 (CategoryTheory.End X)

The endomorphism algebra of a finite-dimensional hom space is finite-dimensional.

def ProjectiveCoverInfra.postcomp (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] (P : C) {Y Z : C} (f : Y ⟶ Z) : (P ⟶ Y) →ₗ[𝕜] P ⟶ Z

Postcomposition by a fixed morphism f : Y ⟶ Z as a 𝕜-linear map (P ⟶ Y) → (P ⟶ Z).

def ProjectiveCoverInfra.precomp (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] (P : C) (a : P ⟶ P) (X : C) : (P ⟶ X) →ₗ[𝕜] P ⟶ X

Precomposition by a fixed endomorphism a : P ⟶ P as a 𝕜-linear map (P ⟶ X) → (P ⟶ X).

@[simp]

theorem ProjectiveCoverInfra.postcomp_apply (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] (P : C) {Y Z : C} (f : Y ⟶ Z) (h : P ⟶ Y) : (postcomp 𝕜 P f) h = CategoryTheory.CategoryStruct.comp h f

Action of postcomp on a hom is given by postcomposition.

@[simp]

theorem ProjectiveCoverInfra.precomp_apply (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] (P : C) (a : P ⟶ P) (X : C) (h : P ⟶ X) : (precomp 𝕜 P a X) h = CategoryTheory.CategoryStruct.comp a h

Action of precomp on a hom is given by precomposition.

noncomputable def ProjectiveCoverInfra.homScalar (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) (f : P ⟶ S) : 𝕜

When (P ⟶ S) is one-dimensional, the unique scalar c such that f = c • π.

theorem ProjectiveCoverInfra.homScalar_spec (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) (f : P ⟶ S) : f = homScalar 𝕜 hdim π hπ f • π

Defining property of homScalar: f = homScalar f • π.

theorem ProjectiveCoverInfra.smul_π_injective (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (π : P ⟶ S) (hπ : π ≠ 0) {c d : 𝕜} (h : c • π = d • π) : c = d

Scalars acting on a nonzero hom are determined by their action: c • π = d • π implies c = d.

noncomputable def ProjectiveCoverInfra.precompScalar (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) (a : CategoryTheory.End P) : 𝕜

For an endomorphism a : End P, the scalar c such that a ≫ π = c • π.

theorem ProjectiveCoverInfra.precompScalar_spec (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) (a : CategoryTheory.End P) : CategoryTheory.CategoryStruct.comp a π = precompScalar 𝕜 hdim π hπ a • π

Defining property of precompScalar: a ≫ π = precompScalar a • π.

theorem ProjectiveCoverInfra.precompScalar_mul (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) (a b : CategoryTheory.End P) : precompScalar 𝕜 hdim π hπ (a * b) = precompScalar 𝕜 hdim π hπ a * precompScalar 𝕜 hdim π hπ b

precompScalar is multiplicative: precompScalar (a*b) = precompScalar a * precompScalar b.

theorem ProjectiveCoverInfra.precompScalar_add (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) (a b : CategoryTheory.End P) : precompScalar 𝕜 hdim π hπ (a + b) = precompScalar 𝕜 hdim π hπ a + precompScalar 𝕜 hdim π hπ b

precompScalar is additive.

theorem ProjectiveCoverInfra.precompScalar_one (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) : precompScalar 𝕜 hdim π hπ 1 = 1

precompScalar sends the identity endomorphism to 1.

theorem ProjectiveCoverInfra.precompScalar_zero (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) : precompScalar 𝕜 hdim π hπ 0 = 0

precompScalar sends the zero endomorphism to 0.

noncomputable def ProjectiveCoverInfra.augmentationRingHom (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) : CategoryTheory.End P →+* 𝕜

The augmentation End P → 𝕜 packaged as a ring homomorphism, built from precompScalar.

noncomputable def ProjectiveCoverInfra.augmentation (𝕜 : Type w) [Field 𝕜] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear 𝕜 C] {P S : C} (hdim : Module.finrank 𝕜 (P ⟶ S) = 1) (π : P ⟶ S) (hπ : π ≠ 0) : CategoryTheory.End P →ₐ[𝕜] 𝕜

The augmentation End P → 𝕜 upgraded to a 𝕜-algebra homomorphism.