Definitions bundle OAIQ031A174 of the split of OpenAI, An explicit counterexample to the Auslander-Reiten conjecture (result family 199)
DefinitionOAIQ031A174A definitions bundle of the split of OpenAI's proof of OAI.ArExplicit.Statement.main, carved from OpenAI's openai/math development (OpenAI, An explicit counterexample to the Auslander-Reiten conjecture (result family 199), OpenAI Math Release, September 23, 2026, result family 199, github.com/openai/math at commit adc7f12, Apache License 2.0) and ported to Lean 4.33.1 and Mathlib 0df444a. The declarations and their proofs are OpenAI's.
Contents. It holds 1 declaration of OpenAI's Lean: 1 theorem.
Sources. They come from these modules of lean/OAI/Algebra, in whole or in part: AuslanderReiten_Coordinates_ConcreteMainCriterion.
Imports. It imports the bundles OAIQ031A163 and OAIQ031A167 of this split.
Imported by (directly, in this split): the bundle OAIQ031A189.
import Mathlib
import Definitions.Def_OAIQ031A163
import Definitions.Def_OAIQ031A167
section
-- module Solutions.OAIQ031_AR.AuslanderReiten_Coordinates_ConcreteMainCriterion
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
namespace OAI
noncomputable section
open CategoryTheory CochainComplex.HomComplex
open scoped ModuleCat.Algebra
namespace ArExplicit.T
universe u
variable {k : Type u} [Field k] [CharP k 2] (q : k) (H₁ H₂ : kˣ)
variable [HasDerivedCategory (ModuleCat.{u} (ArExplicit.T k q))]
variable [HasDerivedCategory (ModuleCat.{u} (ArExplicit.A k q))]
attribute [local instance] moduleCatBaseModule moduleCatBaseTower
local instance instProjectiveMulOppositeAEnvelopingBimoduleCarrierTensorProductFiniteFiber_1 : Module.Projective (A k q)ᵐᵒᵖ
(EnvelopingBimodule k (A k q) (finiteFiber q H₁ H₂).carrier) := by
simpa only [explicitBimodule, BimoduleFiber.bimodule, BimoduleFiber.finiteModule, finiteFiber]
using (explicitBimodule_right q H₁ H₂).2
end ArExplicit.T
end
end OAI
end