GoodReductionJacobian.AbelianSchemePropertyBundle.geometricallyIntegral_of_commRing
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_geometricallyIntegral_of_commRing
attribute [-simp] GoodReductionJacobian.RelativeGroupLaw.baseChangePointToBase_ofBase
GoodReductionJacobian.RelativeGroupLaw.baseChangePointToBase_coe
GoodReductionJacobian.RelativeGroupLaw.baseChangePointOfBase_coe
GoodReductionJacobian.RelativeGroupLaw.baseChange_inv
GoodReductionJacobian.RelativeGroupLaw.baseChangePointOfBase_toBase
GoodReductionJacobian.RelativeGroupLaw.baseChange_mul
GoodReductionJacobian.RelativeGroupLaw.baseChange_one
GoodReductionJacobian.RelativeGroupLaw.nsmul_zero
GoodReductionJacobian.RelativeGroupLaw.mem_torsionSubset
GoodReductionJacobian.RelativeGroupLaw.nsmul_succ NeronModelInfra.schemeHomOverComp_id_left
NeronModelInfra.schemeHomOverComp_id_right NeronModelInfra.schemeHomOverId_coe
NeronModelInfra.schemeHomOverComp_coe NeronModelInfra.fibreRestrictAlong_coe_comp_snd
NeronModelInfra.fibreRestrictAlong_coe_comp_fst GoodReductionJacobian.RelativeGroupLaw.fibre_inv
GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase_coe
GoodReductionJacobian.RelativeGroupLaw.fibrePointOfBase_toBase
GoodReductionJacobian.RelativeGroupLaw.fibre_mul
GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase_ofBase
GoodReductionJacobian.RelativeGroupLaw.fibre_one
GoodReductionJacobian.RelativeGroupLaw.fibrePointOfBase_coe AlgebraicGeometry.schemeFibreEndo_snd
AlgebraicGeometry.schemeFibreEndo_fst
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobianLean source · statement
theorem _root_.GoodReductionJacobian.AbelianSchemePropertyBundle.geometricallyIntegral_of_commRing
{R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
(hA : AbelianSchemePropertyBundle R f) : GeometricallyIntegral f