GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_appTop_fibre_of_isPullback
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_bijective_appTop_fibre_of_isPullback
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
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe uLean source · statement
theorem
_root_.GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_appTop_fibre_of_isPullback
{T : Type u} [CommRing T] {A₀ : Scheme.{u}} {f₀ : A₀ ⟶ Spec (CommRingCat.of T)}
(h₀ : AbelianSchemePropertyBundle T f₀)
{k : Type u} [Field k] (ρ : T →+* k)
{Ak : Scheme.{u}} (fk : Ak ⟶ Spec (CommRingCat.of k)) (i₀ : Ak ⟶ A₀)
(hi₀ : IsPullback i₀ fk f₀ (Spec.map (CommRingCat.ofHom ρ))) :
Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fk.appTop).hom