AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_curveChange_iso_of_closedCover.GTExists.isClosedImmersion_curveChange
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_curveChange_iso_of_closedCover
attribute [-instance]
PresheafOfModules.instMonoidalClosed
instModuleCarrierObjOppositeCommRingCatSubtypePiFamilyMemAddSubgroupNaturalFamilies
instModuleCarrierObjOppositeRingCatCompCommRingCatForget₂RingHomCarrierCarrierAbPresheaf
instSMulCarrierObjOppositeCommRingCatSubtypePiFamilyMemAddSubgroupNaturalFamilies
AlgebraicGeometry.Scheme.PresheafOfModules.symmetricCategory
SheafOfModules.instFaithfulRingSheafPModToPMod
SheafOfModules.symmetricCategory
AlgebraicGeometry.Scheme.PresheafOfModules.monoidalCategory
AlgebraicGeometry.Scheme.PresheafOfModules.monoidalClosed
SheafOfModules.instFullRingSheafPModToPMod
SheafOfModules.monoidalCategory
AlgebraicGeometry.Scheme.Modules.symmetricCategory
SheafOfModules.monoidalClosed
SheafOfModules.instIsLocalizationPModRingSheafSheafifyFunctorPresheafW
SheafOfModules.sheafifyFunctor_monoidal
AlgebraicGeometry.Scheme.Modules.monoidalClosed
AlgebraicGeometry.instMonoidalPresheafOfModulesModulesSheafify
AlgebraicGeometry.Scheme.Modules.monoidalCategory
pullback_monoidal
isIso_δ
PresheafOfModules.pushforward_laxMonoidal
isIso_η
PresheafOfModules.free_monoidal
PresheafOfModules.restrictScalars_laxMonoidal
isIso_δ_gS
PresheafOfModules.pullback_oplaxMonoidal
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
PresheafOfModules.pullback_monoidal'
AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
AlgebraicGeometry.Scheme.Modules.pullback_monoidal
AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
AlgebraicGeometry.Scheme.Modules.map_unitSection
AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
PresheafOfModules.InternalHom.presheaf_map_apply PresheafOfModules.InternalHom.curryFamily_app
PresheafOfModules.InternalHom.add_app PresheafOfModules.InternalHom.smul_app
PresheafOfModules.InternalHom.zero_app PresheafOfModules.ihomObj_map_val
PresheafOfModules.ihomFunctor_map PresheafOfModules.InternalHom.restrict_app
PresheafOfModules.InternalHom.postcomp_app PresheafOfModules.InternalHom.neg_app
PresheafOfModules.curry'_app_val PresheafOfModules.InternalHom.presheaf_obj
PresheafOfModules.ihomFunctor_obj PresheafOfModules.ihomObj_obj
PresheafOfModules.InternalHom.sub_app PresheafOfModules.ihomMap_app_val
SheafOfModules.tensorUnit_eq AlgebraicGeometry.Scheme.Modules.tensorUnit_eq
AlgebraicGeometry.Scheme.Modules.tensorPow_zero AlgebraicGeometry.Scheme.Modules.tensorPow_succ
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add PresheafOfModules.freeεIso_hom_app
PresheafOfModules.freeμIso_hom_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
AlgebraicGeometry.RelPicard
namespace GTExistsLean source · statement
theorem isClosedImmersion_curveChange {R : Type u} [CommRing R] {C C' T : Scheme.{u}}
{c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)} (f : C' ⟶ C) (hf : f ≫ c
= c')
(t : T ⟶ Spec (CommRingCat.of R)) [IsClosedImmersion f] : IsClosedImmersion (curveChange f hf
t)