Nonnegatively graded quasicoherent algebras

A nonnegatively graded algebra on a scheme X is a commutative monoid object in the symmetric monoidal category of ℕ-graded 𝒪_X-modules. Requiring every homogeneous component to be quasicoherent gives the category GradedQuasicoherentAlgebra X. Its morphisms are genuine graded algebra morphisms, since they are morphisms of commutative monoid objects in graded modules.

The functor GradedQuasicoherentAlgebra.degree extracts any homogeneous component as a quasicoherent sheaf. In particular, degreeOne is the coefficient object from which freely generated graded algebras and their associated linear schemes are recovered. The unit GradedQuasicoherentAlgebra.one and the homogeneous multiplications GradedQuasicoherentAlgebra.mul are morphisms of quasicoherent sheaves between these components, satisfying the unit, associativity and commutativity laws and preserved by morphisms of graded algebras. These are the data transported along monoidal functors out of quasicoherent sheaves, such as pullback.

Conversely, GradedQuasicoherentAlgebra.ofHomogeneous builds a graded quasicoherent algebra from its homogeneous components, unit and homogeneous multiplications, and GradedQuasicoherentAlgebra.homMk builds morphisms from componentwise maps. These are the constructors through which graded algebras that are described degree by degree, such as symmetric algebras of quasicoherent sheaves, enter this category.

Main declarations

• TauCeti.AlgebraicGeometry.isGradedQuasicoherentAlgebra: componentwise quasicoherence for a commutative algebra object in nonnegatively graded modules;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra: the full category cut out by that property;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toGradedModules: the underlying graded module functor;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.hom_ext_of_epi_mul: morphisms out of a graded quasicoherent algebra generated in degree one are determined in degree one;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.degree: extraction of a homogeneous component as a quasicoherent sheaf;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.degreeOne: the degree-one functor;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one and TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul: the unit and homogeneous multiplications as morphisms of quasicoherent sheaves, with their laws one_mul, mul_one, mul_assoc, mul_comm, one_map and map_mul;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ofHomogeneous: conversely, the graded quasicoherent algebra with given quasicoherent components, unit and homogeneous multiplications satisfying these laws;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMk: the morphism of graded quasicoherent algebras given by componentwise maps preserving the unit and the homogeneous multiplications;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMkOfEq: the same, for componentwise maps between families identified with the homogeneous components;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.isoMkOfEq: the isomorphism given by componentwise isomorphisms between such families.

def TauCeti.AlgebraicGeometry.isGradedQuasicoherentAlgebra (X : AlgebraicGeometry.Scheme) : CategoryTheory.ObjectProperty (CategoryTheory.CommMon (CategoryTheory.GradedObject ℕ X.Modules))

A commutative algebra object in nonnegatively graded 𝒪_X-modules is graded quasicoherent when each of its homogeneous components is a quasicoherent 𝒪_X-module.

theorem TauCeti.AlgebraicGeometry.isGradedQuasicoherentAlgebra_iff {X : AlgebraicGeometry.Scheme} (A : CategoryTheory.CommMon (CategoryTheory.GradedObject ℕ X.Modules)) : isGradedQuasicoherentAlgebra X A ↔ ∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)

A commutative algebra object in graded modules is graded quasicoherent exactly when each of its homogeneous components is quasicoherent.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The category of commutative nonnegatively graded quasicoherent 𝒪_X-algebras. Its morphisms are morphisms of commutative monoid objects in graded modules, hence preserve the unit, multiplication, and degree.

instance TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.instIsQuasicoherentOpensCarrierCarrierCommRingCatXGradedObjectNatModulesObjCommMonIsGradedQuasicoherentAlgebra {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) : SheafOfModules.IsQuasicoherent (A.obj.X n)

Every homogeneous component of a graded quasicoherent algebra is quasicoherent.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toGradedModules {X : AlgebraicGeometry.Scheme} : CategoryTheory.Functor (GradedQuasicoherentAlgebra X) (CategoryTheory.GradedObject ℕ X.Modules)

The faithful functor forgetting the algebra structure while retaining the grading.

instance TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.instFaithfulGradedObjectNatModulesToGradedModules {X : AlgebraicGeometry.Scheme} : toGradedModules.Faithful

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toGradedModules_obj {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : toGradedModules.obj A = A.obj.X

Forgetting a graded quasicoherent algebra gives its underlying graded module.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toGradedModules_map {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f : A ⟶ B) : toGradedModules.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f.hom.hom.hom (CategoryTheory.eqToHom ⋯))

Forgetting a graded algebra morphism gives its underlying morphism of graded modules.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.hom_ext {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f g : A ⟶ B) (h : ∀ (n : ℕ), f.hom.hom.hom n = g.hom.hom.hom n) : f = g

Two morphisms of graded quasicoherent algebras agree when they agree in every degree.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.hom_ext_iff {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} {f g : A ⟶ B} : f = g ↔ ∀ (n : ℕ), f.hom.hom.hom n = g.hom.hom.hom n

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.hom_ext_of_epi_mul {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} [CategoryTheory.Epi A.obj.toMon.one] [∀ (n : ℕ), CategoryTheory.Epi (A.obj.toMon.mul n 1)] {f g : A ⟶ B} (h : f.hom.hom.hom 1 = g.hom.hom.hom 1) : f = g

Morphisms out of a graded quasicoherent algebra A generated in degree one are determined by their degree-one components. Here generation in degree one means that the unit 𝒪_X ⟶ A₀ and the multiplications Aₙ ⊗ A₁ ⟶ Aₙ₊₁ are epimorphisms, as for symmetric algebras.

def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.degree {X : AlgebraicGeometry.Scheme} (n : ℕ) : CategoryTheory.Functor (GradedQuasicoherentAlgebra X) (QuasicoherentSheaf X)

Extract the degree-n component of a graded quasicoherent algebra as a quasicoherent sheaf. On morphisms this is the degree-n component of the underlying graded algebra morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.degree_obj_obj {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) : ((degree n).obj A).obj = A.obj.X n

The underlying module of the degree-n component is the corresponding component of the underlying graded module.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.degree_map_hom {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f : A ⟶ B) (n : ℕ) : ((degree n).map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (f.hom.hom.hom n) (CategoryTheory.eqToHom ⋯))

The degree functor acts on a graded algebra morphism by its component in that degree.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.epi_hom_hom_of_epi_degree_map {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f : A ⟶ B) (n : ℕ) (h : CategoryTheory.Epi ((degree n).map f).hom) : CategoryTheory.Epi (f.hom.hom.hom n)

A morphism of graded quasicoherent algebras is an epimorphism in degree n when its image under the degree-n functor is an epimorphism of the underlying modules.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.degreeOne {X : AlgebraicGeometry.Scheme} : CategoryTheory.Functor (GradedQuasicoherentAlgebra X) (QuasicoherentSheaf X)

Extract the degree-one component of a graded quasicoherent algebra. This is the component that generates a free graded algebra and therefore the coefficient sheaf of a linear scheme.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (QuasicoherentSheaf X) ⟶ (degree 0).obj A

The unit 𝒪_X ⟶ A₀ of a graded quasicoherent algebra, as a morphism of quasicoherent sheaves into its degree-zero component.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((degree i).obj A) ((degree j).obj A) ⟶ (degree (i + j)).obj A

The homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ of a graded quasicoherent algebra, as a morphism of quasicoherent sheaves between its homogeneous components.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_hom {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : A.one.hom = CategoryTheory.CategoryStruct.comp A.obj.toMon.one (CategoryTheory.eqToHom ⋯)

The unit of A, as a morphism of quasicoherent sheaves, is the unit of the underlying graded algebra on modules, up to the identification degree_obj_obj.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_hom {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) : (A.mul i j).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (A.obj.toMon.mul i j) (CategoryTheory.eqToHom ⋯))

The homogeneous multiplication of A, as a morphism of quasicoherent sheaves, is that of the underlying graded algebra on modules, up to the identifications degree_obj_obj.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_mul {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.one ((degree n).obj A)) (A.mul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((degree n).obj A)).hom (CategoryTheory.eqToHom ⋯)

The unit of a graded quasicoherent algebra is a left identity for homogeneous multiplication, up to the identification of the degrees 0 + n and n.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_mul_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) {Z : QuasicoherentSheaf X} (h : (degree (0 + n)).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.one ((degree n).obj A)) (CategoryTheory.CategoryStruct.comp (A.mul 0 n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((degree n).obj A)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The unit of a graded quasicoherent algebra is a left identity for homogeneous multiplication, up to the identification of the degrees 0 + n and n.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_one {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((degree n).obj A) A.one) (A.mul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((degree n).obj A)).hom (CategoryTheory.eqToHom ⋯)

The unit of a graded quasicoherent algebra is a right identity for homogeneous multiplication, up to the identification of the degrees n + 0 and n.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_one_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) {Z : QuasicoherentSheaf X} (h : (degree (n + 0)).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((degree n).obj A) A.one) (CategoryTheory.CategoryStruct.comp (A.mul n 0) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((degree n).obj A)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The unit of a graded quasicoherent algebra is a right identity for homogeneous multiplication, up to the identification of the degrees n + 0 and n.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (A.mul i j) ((degree k).obj A)) (A.mul (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((degree i).obj A) ((degree j).obj A) ((degree k).obj A)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((degree i).obj A) (A.mul j k)) (CategoryTheory.CategoryStruct.comp (A.mul i (j + k)) (CategoryTheory.eqToHom ⋯)))

Homogeneous multiplication of a graded quasicoherent algebra is associative, up to the identification of the degrees i + j + k and i + (j + k).

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_assoc_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j k : ℕ) {Z : QuasicoherentSheaf X} (h : (degree (i + j + k)).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (A.mul i j) ((degree k).obj A)) (CategoryTheory.CategoryStruct.comp (A.mul (i + j) k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((degree i).obj A) ((degree j).obj A) ((degree k).obj A)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((degree i).obj A) (A.mul j k)) (CategoryTheory.CategoryStruct.comp (A.mul i (j + k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)))

Homogeneous multiplication of a graded quasicoherent algebra is associative, up to the identification of the degrees i + j + k and i + (j + k).

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_comm {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (β_ ((degree i).obj A) ((degree j).obj A)).hom (A.mul j i) = CategoryTheory.CategoryStruct.comp (A.mul i j) (CategoryTheory.eqToHom ⋯)

Homogeneous multiplication of a graded quasicoherent algebra is commutative, up to the identification of the degrees i + j and j + i.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_comm_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) {Z : QuasicoherentSheaf X} (h : (degree (j + i)).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (β_ ((degree i).obj A) ((degree j).obj A)).hom (A.mul j i)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (A.mul i j) (CategoryTheory.eqToHom ⋯)) h

Homogeneous multiplication of a graded quasicoherent algebra is commutative, up to the identification of the degrees i + j and j + i.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_map {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp A.one ((degree 0).map g) = B.one

A morphism of graded quasicoherent algebras preserves the unit in degree zero.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_map_assoc {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (g : A ⟶ B) {Z : QuasicoherentSheaf X} (h : (degree 0).obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp A.one (CategoryTheory.CategoryStruct.comp ((degree 0).map g) h) = CategoryTheory.CategoryStruct.comp B.one h

A morphism of graded quasicoherent algebras preserves the unit in degree zero.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.map_mul {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (g : A ⟶ B) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((degree i).map g) ((degree j).map g)) (B.mul i j) = CategoryTheory.CategoryStruct.comp (A.mul i j) ((degree (i + j)).map g)

A morphism of graded quasicoherent algebras commutes with homogeneous multiplication.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.map_mul_assoc {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (g : A ⟶ B) (i j : ℕ) {Z : QuasicoherentSheaf X} (h : (degree (i + j)).obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((degree i).map g) ((degree j).map g)) (CategoryTheory.CategoryStruct.comp (B.mul i j) h) = CategoryTheory.CategoryStruct.comp (A.mul i j) (CategoryTheory.CategoryStruct.comp ((degree (i + j)).map g) h)

A morphism of graded quasicoherent algebras commutes with homogeneous multiplication.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ofHomogeneous {X : AlgebraicGeometry.Scheme} (M : ℕ → X.Modules) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (M n)] (one : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0) (mul : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)) (one_mul : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one (M n)) (mul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_one : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M n) one) (mul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_assoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mul i j) (M k)) (mul (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (M i) (M j) (M k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M i) (mul j k)) (CategoryTheory.CategoryStruct.comp (mul i (j + k)) (CategoryTheory.eqToHom ⋯)))) (mul_comm : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (β_ (M i) (M j)).hom (mul j i) = CategoryTheory.CategoryStruct.comp (mul i j) (CategoryTheory.eqToHom ⋯)) : GradedQuasicoherentAlgebra X

The graded quasicoherent algebra with quasicoherent homogeneous components M n, unit one : 𝒪_X ⟶ M 0 and homogeneous multiplications mul i j : M i ⊗ M j ⟶ M (i + j), which are required to be unital, associative and commutative up to the identifications of degrees.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ofHomogeneous_obj_X {X : AlgebraicGeometry.Scheme} (M : ℕ → X.Modules) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (M n)] (one : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0) (mul : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)) (one_mul : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one (M n)) (mul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_one : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M n) one) (mul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_assoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mul i j) (M k)) (mul (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (M i) (M j) (M k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M i) (mul j k)) (CategoryTheory.CategoryStruct.comp (mul i (j + k)) (CategoryTheory.eqToHom ⋯)))) (mul_comm : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (β_ (M i) (M j)).hom (mul j i) = CategoryTheory.CategoryStruct.comp (mul i j) (CategoryTheory.eqToHom ⋯)) : (ofHomogeneous M one mul one_mul mul_one mul_assoc mul_comm).obj.X = M

The underlying graded module of ofHomogeneous is the given family of components.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_ofHomogeneous {X : AlgebraicGeometry.Scheme} (M : ℕ → X.Modules) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (M n)] (one : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0) (mul : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)) (one_mul : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one (M n)) (mul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_one : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M n) one) (mul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_assoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mul i j) (M k)) (mul (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (M i) (M j) (M k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M i) (mul j k)) (CategoryTheory.CategoryStruct.comp (mul i (j + k)) (CategoryTheory.eqToHom ⋯)))) (mul_comm : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (β_ (M i) (M j)).hom (mul j i) = CategoryTheory.CategoryStruct.comp (mul i j) (CategoryTheory.eqToHom ⋯)) (i j : ℕ) : (ofHomogeneous M one mul one_mul mul_one mul_assoc mul_comm).obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mul i j) (CategoryTheory.eqToHom ⋯))

The homogeneous multiplication of ofHomogeneous is the given one, up to the identification ofHomogeneous_obj_X of its components with M.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_ofHomogeneous {X : AlgebraicGeometry.Scheme} (M : ℕ → X.Modules) [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (M n)] (one : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0) (mul : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)) (one_mul : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one (M n)) (mul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_one : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M n) one) (mul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (mul_assoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mul i j) (M k)) (mul (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (M i) (M j) (M k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M i) (mul j k)) (CategoryTheory.CategoryStruct.comp (mul i (j + k)) (CategoryTheory.eqToHom ⋯)))) (mul_comm : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (β_ (M i) (M j)).hom (mul j i) = CategoryTheory.CategoryStruct.comp (mul i j) (CategoryTheory.eqToHom ⋯)) : (ofHomogeneous M one mul one_mul mul_one mul_assoc mul_comm).obj.toMon.one = CategoryTheory.CategoryStruct.comp one (CategoryTheory.eqToHom ⋯)

The unit of ofHomogeneous is the given one, up to the identification ofHomogeneous_obj_X of its degree-zero component with M 0.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMk {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f : (n : ℕ) → A.obj.X n ⟶ B.obj.X n) (one_f : CategoryTheory.CategoryStruct.comp A.obj.toMon.one (f 0) = B.obj.toMon.one) (mul_f : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i) (f j)) (B.obj.toMon.mul i j) = CategoryTheory.CategoryStruct.comp (A.obj.toMon.mul i j) (f (i + j))) : A ⟶ B

A family of morphisms between the homogeneous components of two graded quasicoherent algebras which preserves the unit and the homogeneous multiplications is a morphism of graded quasicoherent algebras.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMk_hom_hom_hom {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f : (n : ℕ) → A.obj.X n ⟶ B.obj.X n) (one_f : CategoryTheory.CategoryStruct.comp A.obj.toMon.one (f 0) = B.obj.toMon.one) (mul_f : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i) (f j)) (B.obj.toMon.mul i j) = CategoryTheory.CategoryStruct.comp (A.obj.toMon.mul i j) (f (i + j))) : (homMk f one_f mul_f).hom.hom.hom = f

The components of homMk f are the given morphisms.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMkOfEq {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} {M N : ℕ → X.Modules} (hA : A.obj.X = M) (hB : B.obj.X = N) {oneM : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0} {oneN : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ N 0} {mulM : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} {mulN : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (N i) (N j) ⟶ N (i + j)} (hoA : A.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneM (CategoryTheory.eqToHom ⋯)) (hoB : B.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneN (CategoryTheory.eqToHom ⋯)) (hmA : ∀ (i j : ℕ), A.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulM i j) (CategoryTheory.eqToHom ⋯))) (hmB : ∀ (i j : ℕ), B.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulN i j) (CategoryTheory.eqToHom ⋯))) (f : (n : ℕ) → M n ⟶ N n) (one_f : CategoryTheory.CategoryStruct.comp oneM (f 0) = oneN) (mul_f : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i) (f j)) (mulN i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (f (i + j))) : A ⟶ B

A morphism of graded quasicoherent algebras whose homogeneous components are identified with families M and N carrying units and multiplications, given by componentwise maps M n ⟶ N n preserving those units and multiplications. This transports homMk along identifications of components such as those provided by ofHomogeneous_obj_X.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMkOfEq_hom_hom_hom {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} {M N : ℕ → X.Modules} (hA : A.obj.X = M) (hB : B.obj.X = N) {oneM : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0} {oneN : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ N 0} {mulM : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} {mulN : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (N i) (N j) ⟶ N (i + j)} (hoA : A.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneM (CategoryTheory.eqToHom ⋯)) (hoB : B.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneN (CategoryTheory.eqToHom ⋯)) (hmA : ∀ (i j : ℕ), A.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulM i j) (CategoryTheory.eqToHom ⋯))) (hmB : ∀ (i j : ℕ), B.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulN i j) (CategoryTheory.eqToHom ⋯))) (f : (n : ℕ) → M n ⟶ N n) (one_f : CategoryTheory.CategoryStruct.comp oneM (f 0) = oneN) (mul_f : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i) (f j)) (mulN i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (f (i + j))) (n : ℕ) : (homMkOfEq hA hB hoA hoB hmA hmB f one_f mul_f).hom.hom.hom n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (f n) (CategoryTheory.eqToHom ⋯))

The components of homMkOfEq are the given morphisms, transported along the identifications of the homogeneous components.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMkOfEq_id {X : AlgebraicGeometry.Scheme} {A : GradedQuasicoherentAlgebra X} {M : ℕ → X.Modules} (hA : A.obj.X = M) {oneM : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0} {mulM : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} (hoA : A.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneM (CategoryTheory.eqToHom ⋯)) (hmA : ∀ (i j : ℕ), A.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulM i j) (CategoryTheory.eqToHom ⋯))) (f : (n : ℕ) → M n ⟶ M n) (one_f : CategoryTheory.CategoryStruct.comp oneM (f 0) = oneM) (mul_f : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i) (f j)) (mulM i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (f (i + j))) (hf : ∀ (n : ℕ), f n = CategoryTheory.CategoryStruct.id (M n)) : homMkOfEq hA hA hoA hoA hmA hmA f one_f mul_f = CategoryTheory.CategoryStruct.id A

homMkOfEq sends a family of identities to the identity.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.homMkOfEq_comp {X : AlgebraicGeometry.Scheme} {A B C : GradedQuasicoherentAlgebra X} {M N P : ℕ → X.Modules} (hA : A.obj.X = M) (hB : B.obj.X = N) (hC : C.obj.X = P) {oneM : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0} {oneN : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ N 0} {oneP : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ P 0} {mulM : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} {mulN : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (N i) (N j) ⟶ N (i + j)} {mulP : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (P i) (P j) ⟶ P (i + j)} (hoA : A.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneM (CategoryTheory.eqToHom ⋯)) (hoB : B.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneN (CategoryTheory.eqToHom ⋯)) (hoC : C.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneP (CategoryTheory.eqToHom ⋯)) (hmA : ∀ (i j : ℕ), A.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulM i j) (CategoryTheory.eqToHom ⋯))) (hmB : ∀ (i j : ℕ), B.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulN i j) (CategoryTheory.eqToHom ⋯))) (hmC : ∀ (i j : ℕ), C.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulP i j) (CategoryTheory.eqToHom ⋯))) (f : (n : ℕ) → M n ⟶ N n) (one_f : CategoryTheory.CategoryStruct.comp oneM (f 0) = oneN) (mul_f : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f i) (f j)) (mulN i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (f (i + j))) (g : (n : ℕ) → N n ⟶ P n) (one_g : CategoryTheory.CategoryStruct.comp oneN (g 0) = oneP) (mul_g : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (g i) (g j)) (mulP i j) = CategoryTheory.CategoryStruct.comp (mulN i j) (g (i + j))) (h : (n : ℕ) → M n ⟶ P n) (one_h : CategoryTheory.CategoryStruct.comp oneM (h 0) = oneP) (mul_h : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (h i) (h j)) (mulP i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (h (i + j))) (hfg : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (f n) (g n) = h n) : homMkOfEq hA hC hoA hoC hmA hmC h one_h mul_h = CategoryTheory.CategoryStruct.comp (homMkOfEq hA hB hoA hoB hmA hmB f one_f mul_f) (homMkOfEq hB hC hoB hoC hmB hmC g one_g mul_g)

homMkOfEq sends componentwise composites to composites.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.isoMkOfEq {X : AlgebraicGeometry.Scheme} {P Q : GradedQuasicoherentAlgebra X} {M N : ℕ → X.Modules} (hP : P.obj.X = M) (hQ : Q.obj.X = N) {oneM : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0} {oneN : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ N 0} {mulM : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} {mulN : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (N i) (N j) ⟶ N (i + j)} (hoP : P.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneM (CategoryTheory.eqToHom ⋯)) (hoQ : Q.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneN (CategoryTheory.eqToHom ⋯)) (hmP : ∀ (i j : ℕ), P.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulM i j) (CategoryTheory.eqToHom ⋯))) (hmQ : ∀ (i j : ℕ), Q.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulN i j) (CategoryTheory.eqToHom ⋯))) (e : (n : ℕ) → M n ≅ N n) (one_e : CategoryTheory.CategoryStruct.comp oneM (e 0).hom = oneN) (mul_e : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e i).hom (e j).hom) (mulN i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (e (i + j)).hom) : P ≅ Q

An isomorphism of graded quasicoherent algebras whose homogeneous components are identified with families M and N carrying units and multiplications, given by componentwise isomorphisms M n ≅ N n preserving those units and multiplications. Both directions are built by homMkOfEq.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.isoMkOfEq_hom_hom_hom_hom {X : AlgebraicGeometry.Scheme} {P Q : GradedQuasicoherentAlgebra X} {M N : ℕ → X.Modules} (hP : P.obj.X = M) (hQ : Q.obj.X = N) {oneM : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0} {oneN : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ N 0} {mulM : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} {mulN : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (N i) (N j) ⟶ N (i + j)} (hoP : P.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneM (CategoryTheory.eqToHom ⋯)) (hoQ : Q.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneN (CategoryTheory.eqToHom ⋯)) (hmP : ∀ (i j : ℕ), P.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulM i j) (CategoryTheory.eqToHom ⋯))) (hmQ : ∀ (i j : ℕ), Q.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulN i j) (CategoryTheory.eqToHom ⋯))) (e : (n : ℕ) → M n ≅ N n) (one_e : CategoryTheory.CategoryStruct.comp oneM (e 0).hom = oneN) (mul_e : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e i).hom (e j).hom) (mulN i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (e (i + j)).hom) (n : ℕ) : (isoMkOfEq hP hQ hoP hoQ hmP hmQ e one_e mul_e).hom.hom.hom.hom n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e n).hom (CategoryTheory.eqToHom ⋯))

The components of isoMkOfEq are the given isomorphisms, transported along the identifications of the homogeneous components.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.isoMkOfEq_inv_hom_hom_hom {X : AlgebraicGeometry.Scheme} {P Q : GradedQuasicoherentAlgebra X} {M N : ℕ → X.Modules} (hP : P.obj.X = M) (hQ : Q.obj.X = N) {oneM : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ M 0} {oneN : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ N 0} {mulM : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} {mulN : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (N i) (N j) ⟶ N (i + j)} (hoP : P.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneM (CategoryTheory.eqToHom ⋯)) (hoQ : Q.obj.toMon.one = CategoryTheory.CategoryStruct.comp oneN (CategoryTheory.eqToHom ⋯)) (hmP : ∀ (i j : ℕ), P.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulM i j) (CategoryTheory.eqToHom ⋯))) (hmQ : ∀ (i j : ℕ), Q.obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mulN i j) (CategoryTheory.eqToHom ⋯))) (e : (n : ℕ) → M n ≅ N n) (one_e : CategoryTheory.CategoryStruct.comp oneM (e 0).hom = oneN) (mul_e : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e i).hom (e j).hom) (mulN i j) = CategoryTheory.CategoryStruct.comp (mulM i j) (e (i + j)).hom) (n : ℕ) : (isoMkOfEq hP hQ hoP hoQ hmP hmQ e one_e mul_e).inv.hom.hom.hom n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e n).inv (CategoryTheory.eqToHom ⋯))

The components of the inverse of isoMkOfEq are the inverses of the given isomorphisms, transported along the identifications of the homogeneous components.