GoodReductionJacobian.abelianSchemePropertyBundle_prodStr
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace abelianSchemePropertyBundle_prodStr
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe uLean source · statement
theorem _root_.GoodReductionJacobian.abelianSchemePropertyBundle_prodStr
{K : Type u} [Field K] {B C : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of K)}
{h : C ⟶ Spec (CommRingCat.of K)} (hB : AbelianSchemePropertyBundle K g)
(hC : AbelianSchemePropertyBundle K h) :
AbelianSchemePropertyBundle K (prodStr g h)