baseChange_mul_fst
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianNoetherianDescent
attribute [-instance] IsDirectLimit.Module.instDirectLimitCoeLinearMapIdOfOfNonempty
AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
AlgebraicGeometry.SubalgebraStages.compactSpace_obj
AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
AlgebraicGeometry.SubalgebraStages.isCofiltered_op AlgebraicGeometry.ChowDatum.hι_closed
AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
AlgebraicGeometry.OModulePresheaf.isScalarTower
AlgebraicGeometry.Scheme.OrderedAffineCover.instLinearOrder
AlgebraicGeometry.OModulePresheaf.module AlgebraicGeometry.Scheme.OrderedAffineCover.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCover.instFintypeIdx
AlgebraicGeometry.OModulePresheaf.addCommGroup
AlgebraicGeometry.Scheme.OrderedAffineCover.instDecidableEqIdx
AlgebraicGeometry.OModulePresheaf.moduleSections TwoChartCech.Sections.M0_moduleA
TwoChartCech.Sections.M1_module TwoChartCech.Cover.A01_algebra TwoChartCech.Cover.A0_algebra
TwoChartCech.Cover.A1_commRing TwoChartCech.Cover.A1_algebra TwoChartCech.Sections.M01_module
TwoChartCech.Sections.M0_addCommGroup TwoChartCech.Sections.M0_tower
TwoChartCech.Sections.M01_addCommGroup TwoChartCech.Cover.A0_commRing
attribute [-instance] TwoChartCech.Sections.M1_tower TwoChartCech.Sections.M01_moduleA
TwoChartCech.Sections.M0_module TwoChartCech.Sections.M1_moduleA
TwoChartCech.Sections.M1_addCommGroup TwoChartCech.Cover.A01_commRing
TwoChartCech.Sections.M01_tower CoherentBaseChange.TwoTermComplex.C0_module
CoherentBaseChange.TwoTermComplex.C0_addCommGroup CoherentBaseChange.TwoTermComplex.C1_module
CoherentBaseChange.TwoTermComplex.C1_addCommGroup CoherentBaseChange.TwoTermComplex.C0_free
CoherentBaseChange.TwoTermComplex.C1_finite CoherentBaseChange.TwoTermComplex.C0_finite
CoherentBaseChange.TwoTermComplex.C1_free
AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.biC_abGrp
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_smul
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_smul
AlgebraicGeometry.OModulePresheaf.Leray.biC_module
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx DoubleComplex.instModuleE₂I
DoubleComplex.Bounded.modR DoubleComplex.instModuleE₂II DoubleComplex.instAddCommGroupE₂II
DoubleComplex.Bounded.abGrp DoubleComplex.instAddCommGroupE₂I ProjSpaceCech.GradedModule.H.module
ProjSpaceCech.GradedModule.H.addCommGroup ProjSpaceCech.GradedModule.sec.instAdd
ProjSpaceCech.GradedModule.sec.instNeg ProjSpaceCech.GradedModule.acg
attribute [-instance] ProjSpaceCech.GradedModule.Frac.setoid ProjSpaceCech.GradedModule.modR
ProjSpaceCech.GradedModule.sec.instModule ProjSpaceCech.GradedModule.sec.instAddCommGroup
ProjSpaceCech.GradedModule.sec.instZero ProjSpaceCech.GradedModule.Presentation.fJ
ProjSpaceCech.GradedModule.sec.instSMul ProjSpaceCech.Twist.H.module
ProjSpaceCech.Idx.instFintype ProjSpaceCech.Twist.H.addCommGroup
ProjSpaceCech.Idx.instDecidableEq ProjSpaceCech.Twist.Mon.instDecidableEq
ProjSpaceCech.Twist.cochain.instAddCommGroup ProjSpaceCech.Twist.cochain.instModule
attribute [-simp] IsDirectLimit.Module.linearEquiv_symm_apply IsDirectLimit.linearEquiv_symm_apply
IsDirectLimit.lift_of IsDirectLimit.Module.linearEquiv_apply IsDirectLimit.Module.lift_of
IsDirectLimit.Equiv_apply AlgebraicGeometry.SubalgebraStages.specCone_π_app
AlgebraicGeometry.SubalgebraStages.specLeg_specHom
AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
AlgebraicGeometry.SubalgebraStages.specTrans_specHom
AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
AlgebraicGeometry.SubalgebraStages.specDiagram_map
AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
AlgebraicGeometry.SubalgebraStages.leg_trans AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
AlgebraicGeometry.ChowDatum.mk.injEq AlgebraicGeometry.Scheme.OrderedAffineCover.mk.injEq
AlgebraicGeometry.OModulePresheaf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCover.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.mk.injEq AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0 TwoChartCech.Sections.mk.injEq
TwoChartCech.Cover.mk.injEq TwoChartCech.GrothendieckComplex.mk.injEq
TwoChartCech.Sections.mk.sizeOf_spec
attribute [-simp] TwoChartCech.Cover.mk.sizeOf_spec TwoChartCech.Cover.lineBundle_r0_apply
TwoChartCech.GrothendieckComplex.mk.sizeOf_spec TwoChartCech.Cover.lineBundle_r1_apply
CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec CoherentBaseChange.TwoTermComplex.mk.injEq
AlgebraicGeometry.OModulePresheaf.prod_obj AlgebraicGeometry.OModulePresheaf.restrOpen_obj
AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.injEq
AlgebraicGeometry.OModulePresheaf.pushforward_obj AlgebraicGeometry.OModulePresheaf.im_obj
AlgebraicGeometry.OModulePresheaf.pow_obj AlgebraicGeometry.OModulePresheaf.fstHom_app
AlgebraicGeometry.OModulePresheaf.ker_obj AlgebraicGeometry.OModulePresheaf.coker_obj
AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_U
AlgebraicGeometry.OModulePresheaf.sndHom_app AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
AlgebraicGeometry.OModulePresheaf.Hom.id_app
AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
AlgebraicGeometry.OModulePresheaf.AffHom.id_app
AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
AlgebraicGeometry.OModulePresheaf.Leray.restrictToPreimage_U
AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U DoubleComplex.Bounded.mk.injEq
attribute [-simp] DoubleComplex.Bounded.mk.sizeOf_spec DoubleComplex.Convergence.mk.injEq
DoubleComplex.Convergence.mk.sizeOf_spec DoubleComplex.SubQuot.mk.sizeOf_spec
DoubleComplex.SubQuot.mk.injEq ProjSpaceCech.GradedModule.mk.injEq
ProjSpaceCech.GradedModule.mk.sizeOf_spec ProjSpaceCech.GradedModule.Frac.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Presentation.mk.injEq ProjSpaceCech.GradedModule.Frac.mk.injEq
ProjSpaceCech.GradedModule.Presentation.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.shift_toLinearMap ProjSpaceCech.GradedModule.Hom.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.mk.injEq
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace GoodReductionJacobian
namespace RelativeGroupLaw
namespace FgAbelianDescent
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobiantheorem baseChange_mul_fst {S S' : Type u} [CommRing S] [CommRing S']
(u : Spec (CommRingCat.of S') ⟶ Spec (CommRingCat.of S))
{A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of S)} (G : RelativeGroupLaw S f)
{T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of S')) (x y : SchemeHomOver t' (pullback.snd f
u)) :
((G.baseChange u).mul t' x y).1 ≫ pullback.fst f u =
(G.mul (t' ≫ u)
⟨x.1 ≫ pullback.fst f u, by rw [Category.assoc, pullback.condition, ← Category.assoc, x.2]⟩
⟨y.1 ≫ pullback.fst f u,
by rw [Category.assoc, pullback.condition, ← Category.assoc, y.2]⟩).1 := by
have h := congrArg Subtype.val (RelativeGroupLaw.baseChangePointToBase_mul u G t' x y)
rw [RelativeGroupLaw.baseChangePointToBase_coe] at h
exact h